First-order evaluation by arithmetic bit access

Evaluate terms and formulas directly on a bit string, with a supplied universe size and natural-number variable values. Constants are found by bounded search of their one-hot blocks; quantifiers enumerate the natural numbers below the universe size. The operations are total even on malformed input. The surface module proves correctness on encodings and combines evaluation with validation. Formula.tableCode scans all free-variable assignments in the encoder's tuple order to produce a complete relation truth table.

This is the standard fixed-formula model-checking argument for first-order queries, following Immerman's Descriptive Complexity. Its polynomial-time proof uses the library's machine-backed UnaryFn and FPPred closure rules.

def Complexity.DescriptiveComplexity.Term.evalCode {V : Vocabulary} {n : ℕ} (card : ℕ) (bits : List Bool) (σ : Fin n → ℕ) : Term V n → ℕ

Evaluate a term by its variable value or the first marked bit in its constant block.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DescriptiveComplexity.Term.evalCode card bits σ (Complexity.DescriptiveComplexity.Term.var i) = σ i

def Complexity.DescriptiveComplexity.Formula.evalCode {V : Vocabulary} (card : ℕ) (bits : List Bool) {n : ℕ} : Formula V n → (Fin n → ℕ) → Bool

Evaluate a formula with arithmetic table reads and bounded first-order quantifiers.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DescriptiveComplexity.Formula.evalCode card bits φ.neg x✝ = !Complexity.DescriptiveComplexity.Formula.evalCode card bits φ x✝
• Complexity.DescriptiveComplexity.Formula.evalCode card bits φ.exist x✝ = (List.range card).any fun (a : ℕ) => Complexity.DescriptiveComplexity.Formula.evalCode card bits φ (Fin.cons a x✝)
• Complexity.DescriptiveComplexity.Formula.evalCode card bits φ.all x✝ = (List.range card).all fun (a : ℕ) => Complexity.DescriptiveComplexity.Formula.evalCode card bits φ (Fin.cons a x✝)

def Complexity.DescriptiveComplexity.Formula.tableCode {V : Vocabulary} {n : ℕ} (φ : Formula V n) (card : ℕ) (bits : List Bool) : List Bool

The truth table of an open formula, scanning assignments in the structure encoder's order.

Equations

• One or more equations did not get rendered due to their size.