The number written by a circuit is in FP

DescriptiveComplexity.circuitNumber_mem_FP: a definition in QFO(LFP) (DescriptiveComplexity.QLFPDef) of DescriptiveComplexity.CircuitNumber.

• The fixed point is the one of the circuit value problem: the ten gate rules DescriptiveComplexity.Cvp.cvpRules, read in the larger vocabulary (DescriptiveComplexity.HornClause.onLang), whose least model is the evaluation of the gates (DescriptiveComplexity.CircNum.lfpAssign_numRules_iff).
• The output is the quantitative term Σg. [out(g) ∧ T(g)] · Πh. ([out(h) ∧ h ≠ g ∧ below(h, g)] + 1) (DescriptiveComplexity.CircNum.numOut): the inner product is two to the number of outputs strictly below g, a factor being 2 for each of them and 1 for every other element. This is the shape of the normal form in the proof that QFO(LFP) captures FP (Arenas, Muñoz, Riveros 2020, Theorem 4.4), a number being written digit by digit.

Rules read in a larger vocabulary

def DescriptiveComplexity.HornClause.onLang {L L' : FirstOrder.Language} {B : SOBlock} {k : ℕ} (Φ : L →ᴸ L') (c : HornClause L B k) : HornClause L' B k

A rule, its guard read in a larger vocabulary.

Equations

• DescriptiveComplexity.HornClause.onLang Φ c = { guard := Φ.onFormula c.guard, body := c.body, head := c.head }

The fixed point: the gate rules

@[reducible, inline]

abbrev DescriptiveComplexity.CircNum.numLang : FirstOrder.Language

The vocabulary of the rules: circuits writing a number, with the order.

Equations

• DescriptiveComplexity.CircNum.numLang = FirstOrder.Language.numCircuit.sum FirstOrder.Language.order

def DescriptiveComplexity.CircNum.ordHom : Cvp.cvLang →ᴸ numLang

The vocabulary of the rules of the circuit value problem, read in the one of the rules here.

Equations

• DescriptiveComplexity.CircNum.ordHom = DescriptiveComplexity.circuitOfNum.sumMap (FirstOrder.Language.LHom.id FirstOrder.Language.order)

instance DescriptiveComplexity.CircNum.ordHom_isExpansionOn (A : Type) [FirstOrder.Language.numCircuit.Structure A] [LinearOrder A] : ordHom.IsExpansionOn A

noncomputable def DescriptiveComplexity.CircNum.numRules : List (HornClause numLang Cvp.valBlock Cvp.nvars)

The gate rules of DescriptiveComplexity.Cvp.cvpRules, over the larger vocabulary.

Equations

• DescriptiveComplexity.CircNum.numRules = List.map (DescriptiveComplexity.HornClause.onLang DescriptiveComplexity.CircNum.ordHom) DescriptiveComplexity.Cvp.cvpRules

theorem DescriptiveComplexity.CircNum.lfpAssign_numRules_iff {A : Type} [FirstOrder.Language.numCircuit.Structure A] [LinearOrder A] {b : Bool} {x : Fin 1 → A} : lfpAssign numRules b x ↔ GateVal b (x 0)

The least model of the rules is the evaluation of the gates.

The output term

@[reducible, inline]

abbrev DescriptiveComplexity.CircNum.outLang : FirstOrder.Language

The vocabulary of the output: the rules', and the two rails.

Equations

• DescriptiveComplexity.CircNum.outLang = DescriptiveComplexity.CircNum.numLang.sum DescriptiveComplexity.Cvp.valBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.CircNum.oOut : outLang.Relations 1

“Is an output gate”, in the vocabulary of the output.

Equations

• DescriptiveComplexity.CircNum.oOut = Sum.inl (Sum.inl FirstOrder.Language.ncOut)

@[reducible, inline]

abbrev DescriptiveComplexity.CircNum.oBelow : outLang.Relations 2

The comparison of the outputs, in the vocabulary of the output.

Equations

• DescriptiveComplexity.CircNum.oBelow = Sum.inl (Sum.inl FirstOrder.Language.ncBelow)

@[reducible, inline]

abbrev DescriptiveComplexity.CircNum.oTrue : outLang.Relations 1

The rail of the gates deriving 1, in the vocabulary of the output.

Equations

• DescriptiveComplexity.CircNum.oTrue = Sum.inr (DescriptiveComplexity.varSym DescriptiveComplexity.Cvp.valBlock true)

noncomputable def DescriptiveComplexity.CircNum.bitF : outLang.Formula (Empty ⊕ Fin 1)

“g is an output gate deriving 1”.

Equations

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

noncomputable def DescriptiveComplexity.CircNum.lowF : outLang.Formula ((Empty ⊕ Fin 1) ⊕ Fin 1)

“h is an output gate strictly below g”.

Equations

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

noncomputable def DescriptiveComplexity.CircNum.outOrdS : outLang.Sentence

“The outputs are linearly ordered.”

Equations

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

noncomputable def DescriptiveComplexity.CircNum.numOut : QTerm outLang Empty

The output term: [the outputs are linearly ordered] · Σg. [g holds the digit 1] · Πh. ([h is an output strictly below g] + 1).

Equations

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

noncomputable def DescriptiveComplexity.CircNum.numDef : QLFPDef FirstOrder.Language.numCircuit

The definition of the number written by a circuit in QFO(LFP).

Equations

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

theorem DescriptiveComplexity.circuitNumber_fpDefinable : FPDefinable CircuitNumber

The number written by a circuit is definable in QFO(LFP): the gate rules, and a term writing the number digit by digit.

theorem DescriptiveComplexity.circuitNumber_mem_FP : FP.Mem CircuitNumber

The number written by a circuit is in FP.