Expanding first-order formulas into unbounded Boolean formulas

For a fixed universe size, the input consists of relation truth tables and one-hot constant blocks. StructureInput assigns wires to those bits. The compiler supports arbitrary arities, constants, and open formulas. A quantifier becomes one unbounded gate over all possible values; atomic formulas select their arguments through the constant blocks.

This is the finite quantifier expansion underlying Immerman's Theorem 5.22, Section 5.4: https://people.cs.umass.edu/~immerman/book/ch5.pdf. The target is the existing AC0Formula tree representation. The surface module combines it with circuit realization. Circuit.Validity supplies encoding validation, and DescriptiveComplexity.AC0 packages the complete circuit family.

structure Complexity.DescriptiveComplexity.StructureInput (V : Vocabulary) (card N : ℕ) : Type

Positions of relation bits and one-hot constant bits in an input vector.

• rel (i : Fin V.numRels) : (Fin (V.relArity i) → Fin card) → Fin N

  The bit for each relation symbol and tuple.

• const : Fin V.numConsts → Fin card → Fin N

  The bit asserting that a constant has a specified value.

def Complexity.DescriptiveComplexity.StructureInput.Represents {V : Vocabulary} {N : ℕ} (A : DecFinStruct V) (L : StructureInput V A.card N) (input : BitString N) : Prop

The assigned wires carry the relation tables and exact constant values of a structure.

Equations

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

def Complexity.DescriptiveComplexity.StructureInput.termTest {V : Vocabulary} {card N n : ℕ} (L : StructureInput V card N) (σ : Env card n) : Term V n → Fin card → AC0Formula N

Test whether a term has a given value using a constant leaf or one input literal.

Equations

• L.termTest σ (Complexity.DescriptiveComplexity.Term.var i) x✝ = Complexity.AC0Formula.const (decide (σ i = x✝))
• L.termTest σ (Complexity.DescriptiveComplexity.Term.const c) x✝ = Complexity.AC0Formula.lit { var := L.const c x✝, polarity := true }

def Complexity.DescriptiveComplexity.StructureInput.relationTest {V : Vocabulary} {card N n : ℕ} (L : StructureInput V card N) (σ : Env card n) (i : Fin V.numRels) (ts : Fin (V.relArity i) → Term V n) : AC0Formula N

Select a relation-table entry by testing all its argument values.

Equations

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

def Complexity.DescriptiveComplexity.StructureInput.equalityTest {V : Vocabulary} {card N n : ℕ} (L : StructureInput V card N) (σ : Env card n) (t₁ t₂ : Term V n) : AC0Formula N

Equality holds when the two term selectors agree on some value.

Equations

• L.equalityTest σ t₁ t₂ = Complexity.AC0Formula.orList (List.map (fun (a : Fin card) => Complexity.AC0Formula.andList [L.termTest σ t₁ a, L.termTest σ t₂ a]) (List.finRange card))

def Complexity.DescriptiveComplexity.StructureInput.compile {V : Vocabulary} {card N : ℕ} (L : StructureInput V card N) {n : ℕ} : Formula V n → Env card n → AC0Formula N

Expand a formula into an unbounded Boolean formula over the structure input.

Equations

• L.compile (Complexity.DescriptiveComplexity.Formula.relApp i ts) x✝ = L.relationTest x✝ i ts
• L.compile (Complexity.DescriptiveComplexity.Formula.eq t₁ t₂) x✝ = L.equalityTest x✝ t₁ t₂
• L.compile φ.neg x✝ = (L.compile φ x✝).neg
• L.compile (φ.conj ψ) x✝ = Complexity.AC0Formula.andList [L.compile φ x✝, L.compile ψ x✝]
• L.compile (φ.disj ψ) x✝ = Complexity.AC0Formula.orList [L.compile φ x✝, L.compile ψ x✝]
• L.compile φ.exist x✝ = Complexity.AC0Formula.orList (List.map (fun (a : Fin card) => L.compile φ (Complexity.DescriptiveComplexity.envCons a x✝)) (List.finRange card))
• L.compile φ.all x✝ = Complexity.AC0Formula.andList (List.map (fun (a : Fin card) => L.compile φ (Complexity.DescriptiveComplexity.envCons a x✝)) (List.finRange card))

noncomputable def Complexity.DescriptiveComplexity.Formula.expansionPolynomial {V : Vocabulary} {n : ℕ} : Formula V n → Polynomial ℕ

The exact syntax-tree size of the quantifier expansion, as a polynomial in universe size.

Equations

• (Complexity.DescriptiveComplexity.Formula.relApp i a).expansionPolynomial = 1 + Polynomial.X ^ V.relArity i * Polynomial.C (V.relArity i + 2)
• (Complexity.DescriptiveComplexity.Formula.eq a a_1).expansionPolynomial = 1 + Polynomial.X * Polynomial.C 3
• φ.neg.expansionPolynomial = φ.expansionPolynomial
• (φ.conj ψ).expansionPolynomial = 1 + φ.expansionPolynomial + ψ.expansionPolynomial
• (φ.disj ψ).expansionPolynomial = 1 + φ.expansionPolynomial + ψ.expansionPolynomial
• φ.exist.expansionPolynomial = 1 + Polynomial.X * φ.expansionPolynomial
• φ.all.expansionPolynomial = 1 + Polynomial.X * φ.expansionPolynomial