A finite model checker for ordered FO(LFP)

The formula is fixed while the finite input structure varies. Each least fixed point is computed by iterating its body n ^ k times on a truth table, where n is the universe size and k is the relation arity. Outer assignments and relation tables remain fixed throughout the iteration. Nested fixed points use the same evaluator recursively.

The evaluator is defined on raw syntax and all encoded inputs. Its agreement with least-fixed-point semantics requires the formula's formation certificate and a universe of size at least two, as in the library's canonical ordered structures. Malformed input tables are dealt with separately by the final decision procedure.

Main results

• Cslib.Logic.FO.LFP.ModelChecker.eval_eq_true_iff: bounded evaluation agrees with realization of every well-formed formula, including nested fixed points and captured parameters.
• Cslib.Logic.FO.LFP.ModelChecker.getD_tableOf: tabulation uses the same tuple numbering as encoded input relations.

References

• N. Immerman, Relational queries computable in polynomial time, Section 2, Fact 2.1, for the finite iteration bound.

def Cslib.Logic.FO.LFP.ModelChecker.relIndex {Γ : List ℕ} {k : ℕ} : Operator.RelVar Γ k → ℕ

The index of a scoped relation variable in the stack of truth tables.

def Cslib.Logic.FO.LFP.ModelChecker.termValue {L : FirstOrder.Language} [L.IsRelational] {α : Type w} (n : ℕ) (σ : α → ℕ) : (Ordered.language L).Term α → ℕ

A term's numerical value. Input vocabularies are relational; numeric functions are constants.

def Cslib.Logic.FO.LFP.ModelChecker.valuesIndex (n : ℕ) {k : ℕ} : (Fin k → ℕ) → ℕ

The colexicographic truth-table index of a tuple of natural-number coordinates.

def Cslib.Logic.FO.LFP.ModelChecker.relBit {L : FirstOrder.Language} (v : Vocabulary L) (a : EncodedStructure) {k : ℕ} (r : (Ordered.language L).Relations k) (xs : Fin k → ℕ) : Bool

Input atoms read the supplied tables; order and BIT are computed from natural indices.

def Cslib.Logic.FO.LFP.ModelChecker.foEval {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) (a : EncodedStructure) {α : Type w} (σ : α → ℕ) {k : ℕ} : (Ordered.language L).BoundedFormula α k → (Fin k → ℕ) → Bool

Evaluate an ordinary bounded formula with separate free and bound assignments.

def Cslib.Logic.FO.LFP.ModelChecker.tableOf (n k : ℕ) (f : (Fin k → ℕ) → Bool) : List Bool

Tabulate a Boolean predicate over all tuples, with coordinate zero the least significant.

def Cslib.Logic.FO.LFP.ModelChecker.eval {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) {Γ : List ℕ} {α : Type w} : RawFormula (Ordered.language L) Γ α → EncodedStructure → List (List Bool) → (α → ℕ) → Bool

A raw FO(LFP) evaluator. Bounded iteration gives a total algorithm even for invalid syntax.

def Cslib.Logic.FO.LFP.ModelChecker.tableRelation (n k : ℕ) (table : List Bool) : Set (Fin k → Fin n)

Read one relation table using the standard tuple numbering.

def Cslib.Logic.FO.LFP.ModelChecker.relations (Γ : List ℕ) (n : ℕ) (tables : List (List Bool)) : Operator.RelEnv Γ (Fin n)

Interpret a stack of relation tables at the arities of a scoped context.

@[simp]

theorem Cslib.Logic.FO.LFP.ModelChecker.tableRelation_nil (n k : ℕ) : tableRelation n k [] = ∅

An empty table denotes the empty relation, including nullary relations.

theorem Cslib.Logic.FO.LFP.ModelChecker.relations_cons (Γ : List ℕ) (n k : ℕ) (table : List Bool) (tables : List (List Bool)) : @relations (k :: Γ) n (table :: tables) = @Operator.RelEnv.cons Γ (Fin n) k (tableRelation n k table) (@relations Γ n tables)

Extending the table stack agrees with the typed relation binder.

@[simp]

theorem Cslib.Logic.FO.LFP.ModelChecker.length_tableOf (n k : ℕ) (f : (Fin k → ℕ) → Bool) : (tableOf n k f).length = n ^ k

A tabulation always has exactly one bit per tuple, including for arity zero.

theorem Cslib.Logic.FO.LFP.ModelChecker.getD_tableOf {n k : ℕ} (f : (Fin k → ℕ) → Bool) (xs : Fin k → Fin n) : (tableOf n k f).getD (tupleIndex xs) false = f fun (j : Fin k) => ↑(xs j)

Reading a tabulated predicate recovers its value on the given tuple.

theorem Cslib.Logic.FO.LFP.ModelChecker.valuesIndex_val {n k : ℕ} (xs : Fin k → Fin n) : (valuesIndex n fun (j : Fin k) => ↑(xs j)) = tupleIndex xs

Natural coordinates give the standard truth-table index.

theorem Cslib.Logic.FO.LFP.ModelChecker.eval_eq_true_iff {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) {a : EncodedStructure} (hn : 2 ≤ a.1) {Γ : List ℕ} {α : Type w} (φ : RawFormula (Ordered.language L) Γ α) (hφ : Operator.Formula.wellFormed policy φ = true) (tables : List (List Bool)) (σ : α → Fin a.1) : (eval v φ a tables fun (x : α) => ↑(σ x)) = true ↔ Operator.Formula.Realize interpretation φ (fun {k : ℕ} => relations Γ a.1 tables) σ

The bounded evaluator decides the standard realization of every checked formula in the canonical ordered expansion of a decoded input.