First-order model checking in logarithmic space

For every finite relational vocabulary and every first-order sentence φ, the inputs encoding the finite structures satisfying φ, with malformed inputs rejected, form a problem in L (Cslib.Logic.Vocabulary.queryLanguage_mem_L); so does the query language of every first-order definable class of finite structures (Cslib.Logic.FO.Definable.queryLanguage_mem_L) Immerman, Theorem 3.1. The sentences are those of Mathlib's first-order logic over the relational language: atomic formulas are equalities and relation symbols applied to variables. Immerman's logic FO also has constant symbols and the built-in numeric predicates ≤ and BIT; those are not covered here (a relational language has no constant symbols).

The helpers of the construction live in the namespace Cslib.Logic.Vocabulary.ModelChecker.

The decider is a counter program (Turing.CounterProgram) with random access to the encoded input (Cslib.Logic.Vocabulary.modelChecker). It first checks the shape of the input (Cslib.Logic.Vocabulary.ModelChecker.shapeCode): it counts the unary cardinality n by reading the markers of its frame, then for each relation symbol checks, with a counter, that the next frame holds exactly n ^ k bits for the arity k of the symbol, and finally that nothing follows the last table. It then evaluates φ recursively (Cslib.Logic.Vocabulary.ModelChecker.formulaCode), with one register per quantified variable, so as many registers as the nesting depth of quantifiers, a constant of φ. A quantifier loops over the values below n; an atomic formula compares two registers or reads the bit of a truth table at the position computed from the registers by index arithmetic (Cslib.Logic.tupleIndex). The compilation passes each subformula the labels to continue at when it is true and when it is false, so the program needs no stack. Every register stays below a polynomial in the input length, so the program runs in logarithmic space (Turing.CounterProgram.computableInLogSpace_of_reaches).

The empty structure, n = 0, is included: universal quantifiers hold and existential ones fail vacuously, and nullary relations are read from their one-bit tables.

Main definitions

• Cslib.Logic.Vocabulary.ModelChecker.shapeCode: the code checking that an input is well formed.
• Cslib.Logic.Vocabulary.ModelChecker.formulaCode: the code evaluating a formula.
• Cslib.Logic.Vocabulary.modelChecker: the counter program deciding a sentence.

Main results

• Cslib.Logic.Vocabulary.ModelChecker.reaches_shapeCode: the shape check accepts exactly the well-formed inputs.
• Cslib.Logic.Vocabulary.ModelChecker.reaches_formulaCode: the compiled code of a formula decides its truth in the decoded structure.
• Cslib.Logic.Vocabulary.queryLanguage_mem_L: first-order model checking is in L.
• Cslib.Logic.FO.Definable.queryLanguage_mem_L: the query language of a first-order definable class is in L.

References

• N. Immerman, Descriptive Complexity, Theorem 3.1
• M. Sipser, Introduction to the Theory of Computation, Section 8.4

Index arithmetic

def Cslib.Logic.Vocabulary.ModelChecker.arityAt {L : FirstOrder.Language} (v : Vocabulary L) (i : ℕ) : ℕ

The arity of the symbol at a position, 0 past the last one.

def Cslib.Logic.Vocabulary.ModelChecker.lenExpr {L : FirstOrder.Language} (v : Vocabulary L) (i : ℕ) : Turing.CounterProgram.Expr

The number of bits of the table at a position, n ^ k for the cardinality n in register 0 and the arity k.

def Cslib.Logic.Vocabulary.ModelChecker.startExpr {L : FirstOrder.Language} (v : Vocabulary L) (i : ℕ) : Turing.CounterProgram.Expr

The position of the table at a position in a well-formed input.

def Cslib.Logic.Vocabulary.ModelChecker.tupleExprWith {l : ℕ} (values : Fin l → Turing.CounterProgram.Expr) : Turing.CounterProgram.Expr

The table index of a tuple of computed values.

def Cslib.Logic.Vocabulary.ModelChecker.tupleExpr {l : ℕ} (vars : Fin l → ℕ) : Turing.CounterProgram.Expr

The index of the tuple of values of some registers.

def Cslib.Logic.Vocabulary.ModelChecker.bitExprWith {L : FirstOrder.Language} (v : Vocabulary L) (i : ℕ) {l : ℕ} (values : Fin l → Turing.CounterProgram.Expr) : Turing.CounterProgram.Expr

The position of a relation-table bit for a tuple of computed values.

def Cslib.Logic.Vocabulary.ModelChecker.bitExpr {L : FirstOrder.Language} (v : Vocabulary L) (i : ℕ) {l : ℕ} (vars : Fin l → ℕ) : Turing.CounterProgram.Expr

The position of the bit of the table at position i at the tuple of values of some registers, in a well-formed input.

theorem Cslib.Logic.Vocabulary.ModelChecker.eval_tupleExpr {l n : ℕ} (vars : Fin l → ℕ) {regs : List ℕ} (h0 : regs.getD 0 0 = n) (x : Fin l → Fin n) (hx : ∀ (m : Fin l), regs.getD (vars m) 0 = ↑(x m)) : Turing.CounterProgram.Expr.eval regs (tupleExpr vars) = tupleIndex x

theorem Cslib.Logic.Vocabulary.ModelChecker.eval_bitExprWith {L : FirstOrder.Language} {v : Vocabulary L} {a : EncodedStructure} (ha : v.WellFormed a) {regs : List ℕ} (h0 : regs.getD 0 0 = a.1) {i : ℕ} (hi : i ≤ v.count) {l : ℕ} (values : Fin l → Turing.CounterProgram.Expr) (x : Fin l → Fin a.1) (hx : ∀ (m : Fin l), Turing.CounterProgram.Expr.eval regs (values m) = ↑(x m)) : Turing.CounterProgram.Expr.eval regs (bitExprWith v i values) = tableStart a i + 2 * tupleIndex x + 1

Checking the shape of the input

def Cslib.Logic.Vocabulary.ModelChecker.tableCode {L : FirstOrder.Language} (v : Vocabulary L) (c i F : ℕ) : List Turing.CounterProgram.Instr

The code checking the table at position i, placed at the label c, with the cardinality n in register 0 and the position of the table in register 1: register 2 counts the markers of the table up to n ^ k, for the arity k of the symbol; then the code checks the terminator, moves register 1 past the table and goes to c + 6. It goes to F on a missing marker, a missing terminator, or the end of the input.

def Cslib.Logic.Vocabulary.ModelChecker.shapeCode {L : FirstOrder.Language} (v : Vocabulary L) (b T F : ℕ) : List Turing.CounterProgram.Instr

The code checking that an input is well formed, placed at the label b, with register 0 holding 0: it counts the markers of the unary cardinality into register 0, checks every table (Cslib.Logic.Vocabulary.ModelChecker.tableCode), and checks that the input ends after the last table. It goes to T if the input is well formed, with its cardinality in register 0, and to F otherwise.

theorem Cslib.Logic.Vocabulary.ModelChecker.length_shapeCode {L : FirstOrder.Language} (v : Vocabulary L) (b T F : ℕ) : (shapeCode v b T F).length = 4 + 6 * v.count

def Cslib.Logic.Vocabulary.ModelChecker.TableOk {L : FirstOrder.Language} (v : Vocabulary L) (a : EncodedStructure) (i : ℕ) : Prop

The table at position i exists and has n ^ k bits, for the arity k of the symbol.

@[instance_reducible]

instance Cslib.Logic.Vocabulary.ModelChecker.instDecidableTableOk {L : FirstOrder.Language} (v : Vocabulary L) (a : EncodedStructure) (i : ℕ) : Decidable (TableOk v a i)

theorem Cslib.Logic.Vocabulary.ModelChecker.reaches_shapeCode {L : FirstOrder.Language} {v : Vocabulary L} {P : Turing.CounterProgram} {a : EncodedStructure} {B b T F : ℕ} (hP : P.CodeAt b (shapeCode v b T F)) (hLB : ∀ (i : ℕ), a.1 ^ arityAt v i ≤ B) (hwB : (encStructure a).length ≤ B) (regs : List ℕ) (h0 : regs.getD 0 0 = 0) (hlen : 3 ≤ regs.length) (hB : ∀ r ∈ regs, r ≤ B) : ∃ (regs' : List ℕ), P.Reaches (encStructure a) (P.Running B) (b, regs) (if v.WellFormed a then T else F, regs') ∧ regs'.length = regs.length ∧ (v.WellFormed a → regs'.getD 0 0 = a.1) ∧ ∀ r ∈ regs', r ≤ B

The shape check accepts exactly the well-formed inputs: from the code of the shape check, with register 0 holding 0, the program goes to T with the cardinality in register 0 if the input is well formed, and to F otherwise. The registers stay below B if B bounds the length of the input and the sizes n ^ k of the tables.

theorem Cslib.Logic.Vocabulary.ModelChecker.pow_arityAt_le {L : FirstOrder.Language} (v : Vocabulary L) (a : EncodedStructure) (i : ℕ) : a.1 ^ arityAt v i ≤ ((encStructure a).length + 1) ^ v.maxArity

theorem Cslib.Logic.Vocabulary.ModelChecker.length_le_pow_maxArity {L : FirstOrder.Language} (v : Vocabulary L) (a : EncodedStructure) : (encStructure a).length ≤ ((encStructure a).length + 1) ^ v.maxArity

Evaluating formulas

def Cslib.Logic.Vocabulary.ModelChecker.termReg {L : FirstOrder.Language} [L.IsRelational] {α : Type u_1} (fv : α → ℕ) (base : ℕ) {k : ℕ} (t : L.Term (α ⊕ Fin k)) : ℕ

The register holding the variable of a term of a relational language: fv x for the free variable x, and base + i for the bound variable i.

def Cslib.Logic.Vocabulary.ModelChecker.atomicCompiler {L : FirstOrder.Language} (v : Vocabulary L) [L.IsRelational] {α : Type u_1} (fv : α → ℕ) (base : ℕ) : AtomicCompiler L α

The original order-free atomic handlers: variables are stored in registers, and input relations are read from their encoded truth tables.

def Cslib.Logic.Vocabulary.ModelChecker.formulaCode {L : FirstOrder.Language} (v : Vocabulary L) [L.IsRelational] {α : Type u_1} (fv : α → ℕ) (base : ℕ) {k : ℕ} (φ : L.BoundedFormula α k) (b T F : ℕ) : List Turing.CounterProgram.Instr

The code evaluating an order-free formula, with the cardinality in register 0, free variables in registers fv and bound variables starting at base.

theorem Cslib.Logic.Vocabulary.ModelChecker.reaches_read_bitExprWith {L : FirstOrder.Language} {v : Vocabulary L} [L.IsRelational] {a : EncodedStructure} (ha : v.WellFormed a) {r : ℕ} (R : L.Relations r) {values : Fin r → Turing.CounterProgram.Expr} {x : Fin r → Fin a.1} {P : Turing.CounterProgram} {b T F B : ℕ} {regs : List ℕ} (h0 : regs.getD 0 0 = a.1) (hB : ∀ y ∈ regs, y ≤ B) (hinstr : P.instr b = Turing.CounterProgram.Instr.read (bitExprWith v (v.index ⟨r, R⟩) values) T F F) (hx : ∀ (m : Fin r), Turing.CounterProgram.Expr.eval regs (values m) = ↑(x m)) : ∃ (res : Bool), (res = true ↔ FirstOrder.Language.Structure.RelMap R x) ∧ P.Reaches (encStructure a) (P.Running B) (b, regs) (if res = true then T else F, regs)

Reading a relation table. In a well-formed input, a read instruction at the table bit of R for computed values x branches to T exactly when R holds at x in the decoded structure. This is the relation case of both the order-free and the ordered atomic compilers.

theorem Cslib.Logic.Vocabulary.ModelChecker.atomicCompiler_correct {L : FirstOrder.Language} {v : Vocabulary L} [L.IsRelational] {a : EncodedStructure} (ha : v.WellFormed a) {α : Type u_1} (fv : α → ℕ) (base : ℕ) (val : α → Fin a.1) : have x := v.decode a; (atomicCompiler v fv base).Correct (encStructure a) fv base val

The order-free handlers implement their actual table/variable semantics.

theorem Cslib.Logic.Vocabulary.ModelChecker.reaches_formulaCode {L : FirstOrder.Language} {v : Vocabulary L} [L.IsRelational] {P : Turing.CounterProgram} {a : EncodedStructure} (ha : v.WellFormed a) {B : ℕ} (hnB : a.1 ≤ B) {α : Type u_1} (fv : α → ℕ) (base : ℕ) (hbase : 0 < base) (hfv : ∀ (x : α), fv x < base) (val : α → Fin a.1) {k : ℕ} (φ : L.BoundedFormula α k) (b T F : ℕ) (regs : List ℕ) (xs : Fin k → Fin a.1) : P.CodeAt b (formulaCode v fv base φ b T F) → base + FO.boundDepth φ ≤ regs.length → regs.getD 0 0 = a.1 → (∀ 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 (encStructure a) (P.Running B) (b, regs) (if res = true then T else F, regs') ∧ Turing.CounterProgram.Kept B (base + k) regs regs'

The compiled code of a formula decides its truth in the decoded structure of a well-formed input: from the code of φ at b, with the cardinality in register 0, the values val of the free variables in the registers fv below base and the values xs of the bound variables in the registers from base on, the program goes to T if φ holds under val and xs and to F otherwise, keeping the registers below base + k and the bound B of the registers.

The model checker

def Cslib.Logic.Vocabulary.modelChecker {L : FirstOrder.Language} (v : Vocabulary L) [L.IsRelational] (φ : L.Sentence) : Turing.CounterProgram

The counter program deciding a sentence: the shape check, then the evaluation of the sentence, then a halt with output [true] or [false]. Its registers are the cardinality, the position and the counter of the shape check, and one register per bound variable.

theorem Cslib.Logic.Vocabulary.queryLanguage_mem_L {L : FirstOrder.Language} (v : Vocabulary L) [L.IsRelational] (φ : L.Sentence) : v.queryLanguage {M : CategoryTheory.Bundled L.Structure | ↑M ⊨ φ} ∈ Complexity.L encStructure

First-order model checking is in logarithmic space: for a finite relational vocabulary v and a first-order sentence φ, the inputs encoding the finite structures that satisfy φ form a problem in L Immerman, Theorem 3.1. Malformed inputs are not in the problem; the empty structure is included. The sentence uses the relation symbols of the vocabulary and equality, without Immerman's constant symbols and built-in order and BIT.

theorem Cslib.Logic.FO.Definable.queryLanguage_mem_L {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) {K : Set (CategoryTheory.Bundled L.Structure)} (hK : Definable K) : v.queryLanguage K ∈ Complexity.L encStructure

First-order definable classes have query languages in logarithmic space: for a finite relational vocabulary v, the query language of a first-order definable class of finite structures is in L Immerman, Theorem 3.1. Definable classes are closed under isomorphism (Cslib.Logic.FO.Definable.isoClosed), so membership does not depend on the numbering of an encoded structure (Cslib.Logic.Vocabulary.mem_queryLanguage_encode). The defining sentence is over the relational language, without Immerman's constant symbols and built-in order and BIT.