Shared first-order counter-program control

Compile Mathlib first-order formulas using one counter per bound variable. Equality compares compiled term expressions; relation atoms execute a single supplied branch/read instruction. Implication and universal quantification use the existing fixed-control model-checking recursion. The atomic-handler correctness hypothesis is discharged by each concrete model checker.

This factors the control proof of the original order-free model checker without changing its code lengths, quantifier order or empty-universe behavior.

Main definitions

• Cslib.Logic.FO.boundDepth: the register depth of a bounded formula.
• Cslib.Logic.Vocabulary.ModelChecker.AtomicCompiler: term and relation handlers.
• Cslib.Logic.Vocabulary.ModelChecker.formulaCodeWith: shared formula compilation.

Main results

• Cslib.Logic.Vocabulary.ModelChecker.reaches_formulaCodeWith: semantic correctness and register preservation, from the actual atomic-handler proofs.
• Cslib.Logic.FO.boundDepth_eq_add_quantifierRank: the register depth is the number of bound variables in scope plus the quantifier rank.

References

• N. Immerman, Descriptive Complexity, Theorem 3.1.

def Cslib.Logic.FO.boundDepth {L : FirstOrder.Language} {α : Type u_1} {k : ℕ} : L.BoundedFormula α k → ℕ

The number of bound variables in scope at the deepest point of a formula: the nesting depth of its quantifiers, plus the number of bound variables in scope at the formula itself.

theorem Cslib.Logic.FO.le_boundDepth {L : FirstOrder.Language} {α : Type u_1} {k : ℕ} (φ : L.BoundedFormula α k) : k ≤ boundDepth φ

theorem Cslib.Logic.FO.boundDepth_eq_add_quantifierRank {L : FirstOrder.Language} {α : Type u_1} {k : ℕ} (φ : L.BoundedFormula α k) : boundDepth φ = k + quantifierRank φ

The register depth of a formula is the number of bound variables in scope plus its quantifier rank.

structure Cslib.Logic.Vocabulary.ModelChecker.AtomicCompiler (L : FirstOrder.Language) (α : Type u_1) : Type (max (max u u_1) v)

Compile terms to arithmetic expressions and relations to one branch/read instruction. The handlers do not change registers. Their semantics are proved by AtomicCompiler.Correct.

• term {k : ℕ} : L.Term (α ⊕ Fin k) → Turing.CounterProgram.Expr

  The expression computing a term, for every number of bound variables.

• rel {k r : ℕ} : L.Relations r → (Fin r → L.Term (α ⊕ Fin k)) → ℕ → ℕ → Turing.CounterProgram.Instr

  The instruction branching on a relation atom.

structure Cslib.Logic.Vocabulary.ModelChecker.AtomicCompiler.Correct {L : FirstOrder.Language} {α : Type u_1} (C : AtomicCompiler L α) {n : ℕ} [L.Structure (Fin n)] (w : List Bool) (fv : α → ℕ) (base : ℕ) (val : α → Fin n) : Prop

The atomic handlers realize terms and relations in a concrete input structure, without changing the assignment registers. This is an internal compiler specification, not a hypothesis of the concrete query-language membership theorems.

• term {k : ℕ} (regs : List ℕ) (xs : Fin k → Fin n) : regs.getD 0 0 = n → (∀ (x : α), regs.getD (fv x) 0 = ↑(val x)) → (∀ (i : Fin k), regs.getD (base + ↑i) 0 = ↑(xs i)) → ∀ (t : L.Term (α ⊕ Fin k)), Turing.CounterProgram.Expr.eval regs (C.term t) = ↑(FirstOrder.Language.Term.realize (Sum.elim val xs) t)

  Term expressions compute the canonical natural index.

• rel {k r : ℕ} (R : L.Relations r) (ts : Fin r → L.Term (α ⊕ Fin k)) (P : Turing.CounterProgram) (b T F B : ℕ) (regs : List ℕ) (xs : Fin k → Fin n) : regs.getD 0 0 = n → (∀ (x : α), regs.getD (fv x) 0 = ↑(val x)) → (∀ (i : Fin k), regs.getD (base + ↑i) 0 = ↑(xs i)) → (∀ x ∈ regs, x ≤ B) → P.instr b = C.rel R ts T F → ∃ (res : Bool), (res = true ↔ FirstOrder.Language.Structure.RelMap R fun (i : Fin r) => FirstOrder.Language.Term.realize (Sum.elim val xs) (ts i)) ∧ P.Reaches w (P.Running B) (b, regs) (if res = true then T else F, regs)

  A relation instruction selects exactly its semantic branch.

def Cslib.Logic.Vocabulary.ModelChecker.codeLength {L : FirstOrder.Language} {α : Type u_1} {k : ℕ} : L.BoundedFormula α k → ℕ

The number of instructions compiled from a formula (Cslib.Logic.Vocabulary.ModelChecker.formulaCodeWith).

def Cslib.Logic.Vocabulary.ModelChecker.formulaCodeWith {L : FirstOrder.Language} {α : Type u_1} (C : AtomicCompiler L α) (base : ℕ) {k : ℕ} : L.BoundedFormula α k → ℕ → ℕ → ℕ → List Turing.CounterProgram.Instr

The code evaluating a formula with free variables α and k bound variables, placed at the label b: with the cardinality in register 0, the values expected by the atomic handlers, and the bound variable i in register base + i, it goes to T if the formula holds and to F otherwise. A quantifier over the bound variable k loops over the values of register base + k below the cardinality; equality compares two compiled expressions, and a relation uses its supplied branch instruction.

theorem Cslib.Logic.Vocabulary.ModelChecker.length_formulaCodeWith {L : FirstOrder.Language} {α : Type u_1} (C : AtomicCompiler L α) (base : ℕ) {k : ℕ} (φ : L.BoundedFormula α k) (b T F : ℕ) : (formulaCodeWith C base φ b T F).length = codeLength φ

theorem Cslib.Logic.Vocabulary.ModelChecker.reaches_formulaCodeWith {L : FirstOrder.Language} {P : Turing.CounterProgram} {w : List Bool} {n B : ℕ} [L.Structure (Fin n)] (hnB : n ≤ B) {α : Type u_1} (fv : α → ℕ) (base : ℕ) (hbase : 0 < base) (hfv : ∀ (x : α), fv x < base) (val : α → Fin n) (C : AtomicCompiler L α) (hC : C.Correct w fv base val) {k : ℕ} (φ : L.BoundedFormula α k) (b T F : ℕ) (regs : List ℕ) (xs : Fin k → Fin n) : P.CodeAt b (formulaCodeWith C base φ b T F) → base + FO.boundDepth φ ≤ regs.length → regs.getD 0 0 = n → (∀ r ∈ regs, r ≤ B) → (∀ (x : α), regs.getD (fv x) 0 = ↑(val x)) → (∀ (i : Fin k), regs.getD (base + ↑i) 0 = ↑(xs i)) → ∃ (res : Bool) (regs' : List ℕ), (res = true ↔ φ.Realize val xs) ∧ P.Reaches w (P.Running B) (b, regs) (if res = true then T else F, regs') ∧ Turing.CounterProgram.Kept B (base + k) regs regs'

Compiled first-order control evaluates the formula and preserves the registers below the current bound-variable scope. Only the atomic handlers depend on the input vocabulary/model.