Compiling FO(TC) formulas to nondeterministic counter code

A formula over the canonical ordered language with transitive-closure operators is compiled, at a polarity s, to nondeterministic counter code that reaches a target label when the formula has truth value s and otherwise rejects. First-order subformulas reuse the deterministic ordered checker, shifted above the choice register. Conjunction and universal quantification at polarity true (dually disjunction and existential quantification at false) run sequentially; existential quantification and disjunction at polarity true guess. A closure at polarity true becomes the bounded path loop tcCode around the compiled code of its body. A closure at polarity false becomes the inductive-counting block countCode, whose tests countTestCode run the body code at polarity true (walks and edges) and at polarity false (non-edges).

The correctness contract Correct states soundness and completeness of the compiled code of a formula at each polarity, with every register at most B.

Main definitions

• Cslib.Logic.FO.Ordered.TCModelChecker.compile: the polarity-indexed compiler.
• Cslib.Logic.FO.Ordered.TCModelChecker.tcCode: the bounded closure loop.
• Cslib.Logic.FO.Ordered.TCModelChecker.countTestCode, Cslib.Logic.FO.Ordered.TCModelChecker.countCode: one test and the counting block of inductive counting.
• Cslib.Logic.FO.Ordered.TCModelChecker.Env, Cslib.Logic.FO.Ordered.TCModelChecker.Correct: the hypotheses and statement of compiler correctness.

The register-machine kernel shared with the FO(DTC) compiler (term expressions, the loop test, digit decoding and loading the source tuple) is in Cslib.Logic.FO.Ordered.ClosureKernel; the effect of a block on the registers is Turing.CounterProgram.Kept.

Main results

• Cslib.Logic.FO.Ordered.TCModelChecker.correct_ofFO, correct_neg, correct_conj, correct_ex: correctness for the first-order constructors.

References

• N. Immerman, Languages That Capture Complexity Classes, Theorem 3.1

def Cslib.Logic.FO.Ordered.TCModelChecker.scratch {L : FirstOrder.Language} {Γ : List ℕ} {α : Type w} : Operator.Formula (language L) TC.shape Γ α → ℕ

The scratch registers used by the compiled code of a formula, above its free variables.

def Cslib.Logic.FO.Ordered.TCModelChecker.assignChain (b r k : ℕ) (e : ℕ → Turing.CounterProgram.Expr) : List Turing.CounterProgram.Instr

Straight-line assignments of e i to register r + i above the choice, for i < k.

theorem Cslib.Logic.FO.Ordered.TCModelChecker.length_assignChain (b r k : ℕ) (e : ℕ → Turing.CounterProgram.Expr) : (assignChain b r k e).length = k

theorem Cslib.Logic.FO.Ordered.TCModelChecker.assignChain_eq (b r k : ℕ) (e : ℕ → Turing.CounterProgram.Expr) : assignChain b r k e = List.map Turing.CounterProgram.Instr.shift (Turing.CounterProgram.assignsCode b r k e)

assignChain is the shifted block of assignments.

def Cslib.Logic.FO.Ordered.TCModelChecker.distE (x y : ℕ) : Turing.CounterProgram.Expr

|x - y| for registers x and y: positive exactly when they differ.

def Cslib.Logic.FO.Ordered.TCModelChecker.tcCode (b base k : ℕ) (src dst : Fin k → Turing.CounterProgram.Expr) (M : Turing.CounterProgram.Expr) (body : List Turing.CounterProgram.Instr) (T R : ℕ) : List Turing.CounterProgram.Instr

The closure loop around compiled body code body, placed at b. The source tuple is copied to registers base + i, the guessed successor is decoded into registers base + k + i, register base + 2 * k holds the guess and base + 2 * k + 1 the step counter. The loop reaches T once the current tuple is dst and rejects at R after M steps.

theorem Cslib.Logic.FO.Ordered.TCModelChecker.length_tcCode (b base k : ℕ) (src dst : Fin k → Turing.CounterProgram.Expr) (M : Turing.CounterProgram.Expr) (body : List Turing.CounterProgram.Instr) (T R : ℕ) : (tcCode b base k src dst M body T R).length = 3 * k + 8 + body.length

def Cslib.Logic.FO.Ordered.TCModelChecker.codeE (k : ℕ) (z : Fin k → Turing.CounterProgram.Expr) : Turing.CounterProgram.Expr

The code of a tuple: ∑ i, z i * n ^ i, inverse to digitE.

def Cslib.Logic.FO.Ordered.TCModelChecker.countTestCode (b base k : ℕ) (src : Fin k → Turing.CounterProgram.Expr) (wb et ef : List Turing.CounterProgram.Instr) (T R : ℕ) : List Turing.CounterProgram.Instr

One test of inductive counting, placed at b, with registers I, C, Y, X, S, H at base + 0, 1, 3, 4, 5, 6, the decoded pair at base + 7, and the walk at base + 7 + 2 * k. Given the size C of round I, it scans every x < n ^ k, guesses whether x is in round I, certifies selected x by a walk of at most I steps from src (walk body wb), and guesses and certifies whether x reaches y (the value of Y) in at most one step (edge codes et, ef). It goes to T with H = 1 exactly when y is in round I + 1, after checking that C elements were selected; otherwise it rejects at R.

theorem Cslib.Logic.FO.Ordered.TCModelChecker.length_countTestCode (b base k : ℕ) (src : Fin k → Turing.CounterProgram.Expr) (wb et ef : List Turing.CounterProgram.Instr) (T R : ℕ) : (countTestCode b base k src wb et ef T R).length = 5 * k + 25 + wb.length + et.length + ef.length

def Cslib.Logic.FO.Ordered.TCModelChecker.countCode (b base k : ℕ) (dst : Fin k → Turing.CounterProgram.Expr) (t₁ t₂ : List Turing.CounterProgram.Instr) (T R : ℕ) : List Turing.CounterProgram.Instr

The inductive-counting block for a negated closure, placed at b: rounds I < n ^ k - 1 compute the size D of round I + 1 from the size C of round I by one test per candidate y (first test code t₁), and a final test (code t₂) of the target code at round n ^ k - 1 goes to T exactly when the target is not reached.

theorem Cslib.Logic.FO.Ordered.TCModelChecker.length_countCode (b base k : ℕ) (dst : Fin k → Turing.CounterProgram.Expr) (t₁ t₂ : List Turing.CounterProgram.Instr) (T R : ℕ) : (countCode b base k dst t₁ t₂ T R).length = t₁.length + t₂.length + 12

def Cslib.Logic.FO.Ordered.TCModelChecker.len {L : FirstOrder.Language} {Γ : List ℕ} {α : Type w} : Operator.Formula (language L) TC.shape Γ α → Bool → ℕ

The number of instructions compiled from a formula at a polarity.

def Cslib.Logic.FO.Ordered.TCModelChecker.compile {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) {Γ : List ℕ} {α : Type w} : (α → ℕ) → ℕ → Operator.Formula (language L) TC.shape Γ α → Bool → ℕ → ℕ → ℕ → List Turing.CounterProgram.Instr

The code for a formula at a polarity s, placed at b: registers above the choice; the free variable x in register fv x, scratch registers from base. It goes to T when the formula has truth value s and otherwise rejects at R.

theorem Cslib.Logic.FO.Ordered.TCModelChecker.length_compile {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) {Γ : List ℕ} {α : Type w} (fv : α → ℕ) (base : ℕ) (φ : Operator.Formula (language L) TC.shape Γ α) (s : Bool) (b T R : ℕ) : (compile v fv base φ s b T R).length = len φ s

theorem Cslib.Logic.FO.Ordered.TCModelChecker.reaches_assignChain {P : Turing.CounterProgram} {w : List Bool} {B b r : ℕ} {e : ℕ → Turing.CounterProgram.Expr} {k : ℕ} (hP : P.CodeAt b (assignChain b r k e)) {regs : List ℕ} (hlen : r + k ≤ regs.length) (he : ∀ i < k, ∀ (regs' : List ℕ), (∀ (j : ℕ), j < r ∨ r + k ≤ j → regs'.getD j 0 = regs.getD j 0) → Turing.CounterProgram.Expr.eval regs' (e i) = Turing.CounterProgram.Expr.eval regs (e i)) (hB : ∀ x ∈ regs, x ≤ B) (heB : ∀ i < k, Turing.CounterProgram.Expr.eval regs (e i) ≤ B) : ∃ (regs' : List ℕ), P.Reaches w (P.Oblivious B) (b, 0 :: regs) (b + k, 0 :: regs') ∧ regs'.length = regs.length ∧ (∀ (j : ℕ), j < r ∨ r + k ≤ j → regs'.getD j 0 = regs.getD j 0) ∧ (∀ i < k, regs'.getD (r + i) 0 = Turing.CounterProgram.Expr.eval regs (e i)) ∧ ∀ x ∈ regs', x ≤ B

Straight-line assignments, when each expression ignores the registers assigned.

def Cslib.Logic.FO.Ordered.TCModelChecker.Sat (s : Bool) (p : Prop) : Prop

A proposition with the truth value s.

structure Cslib.Logic.FO.Ordered.TCModelChecker.Env {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) (a : EncodedStructure) [L.Structure (Fin a.1)] [Fact (2 ≤ a.1)] (P : Turing.CounterProgram) (B : ℕ) (Post : Turing.CounterProgram.Config → Prop) (R : ℕ) : Prop

The hypotheses of the compiler correctness proof.

• atomic {β : Type} (fv : β → ℕ) (base : ℕ) (val : β → Fin a.1) : (ModelChecker.atomicCompiler v fv base).Correct (encStructure a) fv base val
• one_le : 1 ≤ B
• card_le : a.1 ≤ B
• halts : (P.instr R).halts = true
• post (s : Turing.CounterProgram.Config) : s.1 = R → Post s

def Cslib.Logic.FO.Ordered.TCModelChecker.Correct {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) (a : EncodedStructure) [L.Structure (Fin a.1)] [Fact (2 ≤ a.1)] (P : Turing.CounterProgram) (B : ℕ) (Post : Turing.CounterProgram.Config → Prop) (R : ℕ) {Γ : List ℕ} {α : Type} (φ : Operator.Formula (language L) TC.shape Γ α) : Prop

The compiled code of φ is correct at every polarity.

theorem Cslib.Logic.FO.Ordered.TCModelChecker.eval_termE {L : FirstOrder.Language} [L.IsRelational] {v : Vocabulary L} {a : EncodedStructure} [L.Structure (Fin a.1)] [Fact (2 ≤ a.1)] {P : Turing.CounterProgram} {B : ℕ} {Post : Turing.CounterProgram.Config → Prop} {R : ℕ} (hE : Env v a P B Post R) {α : Type} (fv : α → ℕ) (val : α → Fin a.1) {regs : List ℕ} (h0 : regs.getD 0 0 = a.1) (hv : ∀ (x : α), regs.getD (fv x) 0 = ↑(val x)) (t : (language L).Term α) : Turing.CounterProgram.Expr.eval regs (ClosureKernel.termE fv t) = ↑(FirstOrder.Language.Term.realize val t)

theorem Cslib.Logic.FO.Ordered.TCModelChecker.correct_ofFO {L : FirstOrder.Language} [L.IsRelational] {v : Vocabulary L} {a : EncodedStructure} [L.Structure (Fin a.1)] [Fact (2 ≤ a.1)] {P : Turing.CounterProgram} {B : ℕ} {Post : Turing.CounterProgram.Config → Prop} {R : ℕ} (hE : Env v a P B Post R) {Γ : List ℕ} {α : Type} (φ : (language L).Formula α) : Correct v a P B Post R (Operator.Formula.ofFO φ)

theorem Cslib.Logic.FO.Ordered.TCModelChecker.correct_neg {L : FirstOrder.Language} [L.IsRelational] {v : Vocabulary L} {a : EncodedStructure} [L.Structure (Fin a.1)] [Fact (2 ≤ a.1)] {P : Turing.CounterProgram} {B : ℕ} {Post : Turing.CounterProgram.Config → Prop} {R : ℕ} {Γ : List ℕ} {α : Type} {φ : Operator.Formula (language L) TC.shape Γ α} (ih : Correct v a P B Post R φ) : Correct v a P B Post R φ.neg

theorem Cslib.Logic.FO.Ordered.TCModelChecker.correct_conj {L : FirstOrder.Language} [L.IsRelational] {v : Vocabulary L} {a : EncodedStructure} [L.Structure (Fin a.1)] [Fact (2 ≤ a.1)] {P : Turing.CounterProgram} {B : ℕ} {Post : Turing.CounterProgram.Config → Prop} {R : ℕ} (hE : Env v a P B Post R) {Γ : List ℕ} {α : Type} {φ ψ : Operator.Formula (language L) TC.shape Γ α} (ihφ : Correct v a P B Post R φ) (ihψ : Correct v a P B Post R ψ) : Correct v a P B Post R (φ.conj ψ)

@[simp]

theorem Cslib.Logic.FO.Ordered.TCModelChecker.sat_true (p : Prop) : Sat true p ↔ p

@[simp]

theorem Cslib.Logic.FO.Ordered.TCModelChecker.sat_false (p : Prop) : Sat false p ↔ ¬p

theorem Cslib.Logic.FO.Ordered.TCModelChecker.correct_ex {L : FirstOrder.Language} [L.IsRelational] {v : Vocabulary L} {a : EncodedStructure} [L.Structure (Fin a.1)] [Fact (2 ≤ a.1)] {P : Turing.CounterProgram} {B : ℕ} {Post : Turing.CounterProgram.Config → Prop} {R : ℕ} (hE : Env v a P B Post R) {Γ : List ℕ} {α : Type} {φ : Operator.Formula (language L) TC.shape Γ (Option α)} (ih : Correct v a P B Post R φ) : Correct v a P B Post R φ.ex