CVP is in polynomial time

Membership is written in FO(LFP) and not in the Horn fragment, and the choice is the point of the file: the semantics of DescriptiveComplexity.CVP is a least fixed point (DescriptiveComplexity.GateVal), so the rule system DescriptiveComplexity.Cvp.cvpRules is the ten gate rules transcribed, one per line of the inductive definition, and the output sentence is the one first-order statement the Horn fragment could not make head-on: “some output gate is in the true rail”. A Horn program accepts when its least model satisfies its goal clauses, i.e., when something is not derived, so the same definition in the fragment would have to be written on the false rail and would need the circuit to be well-formed for the two rails to be complementary. Reading the value at an unrestricted first-order output formula avoids the detour, and DescriptiveComplexity.lfpDefinable_iff_mem_PTIME – Immerman–Vardi – turns it back into membership in the class.

The ≡ between the rule system's least model and the inductive semantics is proved in both directions in the usual way: the inductive predicate is closed under the rules (DescriptiveComplexity.Cvp.derives_of_gateVal), and it is a prefixpoint, so it contains the least one (DescriptiveComplexity.Cvp.gateVal_of_derives, by DescriptiveComplexity.lfpAssign_least_of_closed).

The block, the vocabulary of the rules, and their guards

@[reducible]

def DescriptiveComplexity.Cvp.valBlock : SOBlock

The two rails of the induction: one unary relation variable per truth value, true carrying the gates that evaluate to 1. Indexing the block by Bool rather than by Fin 2 is what lets ρ true and ρ false elaborate; the block is reducible so that a numeral elaborates at Fin (arity i).

Equations

• DescriptiveComplexity.Cvp.valBlock = { ι := Bool, ιFinite := Bool.instFinite, arity := fun (x : Bool) => 1 }

@[reducible, inline]

abbrev DescriptiveComplexity.Cvp.cvLang : FirstOrder.Language

The vocabulary the rules are written over: circuits, expanded by the order that every FO(LFP) definition may use (this one does not).

Equations

• DescriptiveComplexity.Cvp.cvLang = FirstOrder.Language.circuit.sum FirstOrder.Language.order

@[reducible, inline]

abbrev DescriptiveComplexity.Cvp.gIsTrue : cvLang.Relations 1

“Is a constant 1 input”, in the rules' vocabulary.

Equations

• DescriptiveComplexity.Cvp.gIsTrue = Sum.inl FirstOrder.Language.circIsTrue

@[reducible, inline]

abbrev DescriptiveComplexity.Cvp.gIsFalse : cvLang.Relations 1

“Is a constant 0 input”, in the rules' vocabulary.

Equations

• DescriptiveComplexity.Cvp.gIsFalse = Sum.inl FirstOrder.Language.circIsFalse

@[reducible, inline]

abbrev DescriptiveComplexity.Cvp.gIsAnd : cvLang.Relations 1

“Is a conjunction gate”, in the rules' vocabulary.

Equations

• DescriptiveComplexity.Cvp.gIsAnd = Sum.inl FirstOrder.Language.circIsAnd

@[reducible, inline]

abbrev DescriptiveComplexity.Cvp.gIsOr : cvLang.Relations 1

“Is a disjunction gate”, in the rules' vocabulary.

Equations

• DescriptiveComplexity.Cvp.gIsOr = Sum.inl FirstOrder.Language.circIsOr

@[reducible, inline]

abbrev DescriptiveComplexity.Cvp.gIsNot : cvLang.Relations 1

“Is a negation gate”, in the rules' vocabulary.

Equations

• DescriptiveComplexity.Cvp.gIsNot = Sum.inl FirstOrder.Language.circIsNot

@[reducible, inline]

abbrev DescriptiveComplexity.Cvp.gOut : cvLang.Relations 1

“Is an output gate”, in the rules' vocabulary.

Equations

• DescriptiveComplexity.Cvp.gOut = Sum.inl FirstOrder.Language.circOut

@[reducible, inline]

abbrev DescriptiveComplexity.Cvp.gLeft : cvLang.Relations 2

“Takes as first argument”, in the rules' vocabulary.

Equations

• DescriptiveComplexity.Cvp.gLeft = Sum.inl FirstOrder.Language.circLeft

@[reducible, inline]

abbrev DescriptiveComplexity.Cvp.gRight : cvLang.Relations 2

“Takes as second argument”, in the rules' vocabulary.

Equations

• DescriptiveComplexity.Cvp.gRight = Sum.inl FirstOrder.Language.circRight

@[reducible, inline]

abbrev DescriptiveComplexity.Cvp.nvars : ℕ

The rules quantify over three variables: the gate and its two arguments.

Equations

• DescriptiveComplexity.Cvp.nvars = 3

noncomputable def DescriptiveComplexity.Cvp.kindF (r : cvLang.Relations 1) (i : Fin nvars) : cvLang.Formula (Fin nvars)

A gate-kind guard on one of the three variables.

Equations

• DescriptiveComplexity.Cvp.kindF r i = r.formula₁ (FirstOrder.Language.var i)

noncomputable def DescriptiveComplexity.Cvp.wireF (r : cvLang.Relations 2) (i j : Fin nvars) : cvLang.Formula (Fin nvars)

A wire guard between two of the three variables.

Equations

• DescriptiveComplexity.Cvp.wireF r i j = r.formula₂ (FirstOrder.Language.var i) (FirstOrder.Language.var j)

def DescriptiveComplexity.Cvp.rail (b : Bool) (i : Fin nvars) : SOAtom valBlock nvars

The atom “variable i is in the rail b”.

Equations

• DescriptiveComplexity.Cvp.rail b i = { idx := b, args := fun (x : Fin (DescriptiveComplexity.Cvp.valBlock.arity b)) => i }

The rules

One rule per constructor of DescriptiveComplexity.GateVal, with the gate as variable 0 and its two arguments as variables 1 and 2.

noncomputable def DescriptiveComplexity.Cvp.cvpRules : List (HornClause cvLang valBlock nvars)

The ten gate rules, read off the inductive semantics.

Equations

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

The output sentence: some output gate is in the true rail

noncomputable def DescriptiveComplexity.Cvp.cvpOut : (cvLang.sum valBlock.lang).Sentence

The output sentence of the definition: ∃ g, out(g) ∧ T(g), read at the least fixed point. This is the formula the Horn fragment has no room for.

Equations

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

noncomputable def DescriptiveComplexity.Cvp.cvpDef : LFPDef FirstOrder.Language.circuit

The FO(LFP) definition of CVP: the gate rules, read at “some output gate is true”.

Equations

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

The least model of the rules is the inductive semantics

theorem DescriptiveComplexity.Cvp.realize_kindF {A : Type} [FirstOrder.Language.circuit.Structure A] [LinearOrder A] (r : cvLang.Relations 1) (i : Fin nvars) (v : Fin nvars → A) : (kindF r i).Realize v ↔ FirstOrder.Language.Structure.RelMap r ![v i]

Realization of a kind guard, down to the circuit structure.

theorem DescriptiveComplexity.Cvp.realize_wireF {A : Type} [FirstOrder.Language.circuit.Structure A] [LinearOrder A] (r : cvLang.Relations 2) (i j : Fin nvars) (v : Fin nvars → A) : (wireF r i j).Realize v ↔ FirstOrder.Language.Structure.RelMap r ![v i, v j]

Realization of a wire guard, down to the circuit structure.

@[reducible, inline]

abbrev DescriptiveComplexity.Cvp.gateAssign {A : Type} [FirstOrder.Language.circuit.Structure A] : valBlock.Assignment A

The assignment cut out by the inductive semantics: a gate is in the rail b when it derives the value b.

Equations

• DescriptiveComplexity.Cvp.gateAssign b x = DescriptiveComplexity.GateVal b (x 0)

theorem DescriptiveComplexity.Cvp.gateAssign_rail {A : Type} [FirstOrder.Language.circuit.Structure A] (b : Bool) (i : Fin nvars) (v : Fin nvars → A) : (rail b i).Holds gateAssign v ↔ GateVal b (v i)

A rail atom holds of the inductive semantics exactly when the variable it names derives the value it names.

theorem DescriptiveComplexity.Cvp.gateAssign_closed {A : Type} [FirstOrder.Language.circuit.Structure A] [LinearOrder A] (c : HornClause cvLang valBlock nvars) : c ∈ cvpRules → ∀ (a : SOAtom valBlock nvars), c.head = some a → ∀ (v : Fin nvars → A), c.guard.Realize v → (∀ b ∈ c.body, b.Holds gateAssign v) → a.Holds gateAssign v

The inductive semantics is closed under the rules, one case per gate rule.

theorem DescriptiveComplexity.Cvp.gateVal_of_derives {A : Type} [FirstOrder.Language.circuit.Structure A] [LinearOrder A] {b : Bool} {x : Fin 1 → A} (h : Derives cvpRules ⟨b, x⟩) : GateVal b (x 0)

Everything the rules derive has its value derivable by the gate rules: the least fixed point is contained in the inductive semantics.

theorem DescriptiveComplexity.Cvp.derives_of_gateVal {A : Type} [FirstOrder.Language.circuit.Structure A] [LinearOrder A] {b : Bool} {g : A} (h : GateVal b g) : Derives cvpRules ⟨b, fun (x : Fin (valBlock.arity b)) => g⟩

Conversely, every derivable value is derived by the rules. The tuple is written fun _ => g throughout, which is the shape DescriptiveComplexity.Derives.rule produces for a unary head.

theorem DescriptiveComplexity.Cvp.lfpAssign_iff {A : Type} [FirstOrder.Language.circuit.Structure A] [LinearOrder A] {b : Bool} {x : Fin 1 → A} : lfpAssign cvpRules b x ↔ GateVal b (x 0)

The least model of the rules is the inductive semantics.

The value of the definition

theorem DescriptiveComplexity.Cvp.realize_cvpOut {A : Type} [FirstOrder.Language.circuit.Structure A] [LinearOrder A] : A ⊨ cvpOut ↔ CircuitAccepts A

Realization of the output sentence at the least fixed point: some output gate is in the true rail.

theorem DescriptiveComplexity.Cvp.cvpDef_holds {A : Type} [FirstOrder.Language.circuit.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : cvpDef.Holds A ↔ CircuitAccepts A

The FO(LFP) definition computes CVP.

Definability and membership

theorem DescriptiveComplexity.Cvp.cvp_lfpDefinable : LFPDefinable CVP

CVP is FO(LFP) definable: the gate rules, read at “some output gate is true”.

theorem DescriptiveComplexity.cvp_mem_PTIME : PTIME.Mem CVP

CVP is in polynomial time, by Immerman–Vardi (DescriptiveComplexity.lfpDefinable_iff_mem_PTIME) applied to the FO(LFP) definition that transcribes the gate rules.