The number written by a circuit: definition

The function counterpart of the circuit value problem (DescriptiveComplexity.CVP). An instance is a Boolean circuit with several output gates and a comparison below between them; the outputs, read in that order, are the binary digits of a natural number, and DescriptiveComplexity.CircuitNumber is the problem of computing it.

• FirstOrder.Language.numCircuit: the vocabulary of circuits (FirstOrder.Language.circuit) with one more binary symbol, below.
• A circuit over it is a circuit in the sense of DescriptiveComplexity.CVP, by forgetting below (DescriptiveComplexity.circuitOfNum): its gates are evaluated by DescriptiveComplexity.GateVal.
• DescriptiveComplexity.circuitNumber: an output gate g deriving the value 1 contributes 2 ^ r, where r is the number of output gates strictly below g (DescriptiveComplexity.outRank). This is the number whose binary digits are the values of the output gates, the lowest holding the least significant digit, when below linearly orders the output gates (DescriptiveComplexity.OutOrder); an instance whose below does not writes 0.

@[reducible, inline]

abbrev FirstOrder.Language.ncIsAnd : Language.numCircuit.Relations 1

isAnd g: the element g is a conjunction gate.

Equations

• FirstOrder.Language.ncIsAnd = FirstOrder.Language.numCircuitRel.isAnd

@[reducible, inline]

abbrev FirstOrder.Language.ncLeft : Language.numCircuit.Relations 2

left g x: the gate g takes x as its first argument.

Equations

• FirstOrder.Language.ncLeft = FirstOrder.Language.numCircuitRel.left

@[reducible, inline]

abbrev FirstOrder.Language.ncIsOr : Language.numCircuit.Relations 1

isOr g: the element g is a disjunction gate.

Equations

• FirstOrder.Language.ncIsOr = FirstOrder.Language.numCircuitRel.isOr

@[reducible, inline]

abbrev FirstOrder.Language.ncIsNot : Language.numCircuit.Relations 1

isNot g: the element g is a negation gate, its argument read off left.

Equations

• FirstOrder.Language.ncIsNot = FirstOrder.Language.numCircuitRel.isNot

inductive FirstOrder.Language.numCircuitRel : ℕ → Type

The relation symbols of the language.

• isTrue : numCircuitRel 1

  isTrue g: the element g is a constant input gate holding 1.

• isFalse : numCircuitRel 1

  isFalse g: the element g is a constant input gate holding 0.

• isAnd : numCircuitRel 1

  isAnd g: the element g is a conjunction gate.

• isOr : numCircuitRel 1

  isOr g: the element g is a disjunction gate.

• isNot : numCircuitRel 1

  isNot g: the element g is a negation gate, its argument read off left.

• out : numCircuitRel 1

  out g: the element g is an output gate, holding one digit.

• left : numCircuitRel 2

  left g x: the gate g takes x as its first argument.

• right : numCircuitRel 2

  right g x: the gate g takes x as its second argument.

• below : numCircuitRel 2

  below h g: the digit held by h is at most as significant as the one held by g.

@[reducible, inline]

abbrev FirstOrder.Language.ncIsFalse : Language.numCircuit.Relations 1

isFalse g: the element g is a constant input gate holding 0.

Equations

• FirstOrder.Language.ncIsFalse = FirstOrder.Language.numCircuitRel.isFalse

@[reducible, inline]

abbrev FirstOrder.Language.ncOut : Language.numCircuit.Relations 1

out g: the element g is an output gate, holding one digit.

Equations

• FirstOrder.Language.ncOut = FirstOrder.Language.numCircuitRel.out

@[reducible, inline]

abbrev FirstOrder.Language.ncIsTrue : Language.numCircuit.Relations 1

isTrue g: the element g is a constant input gate holding 1.

Equations

• FirstOrder.Language.ncIsTrue = FirstOrder.Language.numCircuitRel.isTrue

instance FirstOrder.Language.instIsRelationalNumCircuit : Language.numCircuit.IsRelational

def FirstOrder.Language.numCircuit : Language

The relational language of Boolean circuits writing a number: the symbols of FirstOrder.Language.circuit, and a comparison of the output gates.

Equations

• FirstOrder.Language.numCircuit = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.numCircuitRel }

@[reducible, inline]

abbrev FirstOrder.Language.ncRight : Language.numCircuit.Relations 2

right g x: the gate g takes x as its second argument.

Equations

• FirstOrder.Language.ncRight = FirstOrder.Language.numCircuitRel.right

def FirstOrder.Language.instDecidableEqNumCircuitRel.decEq {a✝ : ℕ} (x✝ x✝¹ : numCircuitRel a✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqNumCircuitRel {a✝ : ℕ} : DecidableEq (numCircuitRel a✝)

Equations

• FirstOrder.Language.instDecidableEqNumCircuitRel = FirstOrder.Language.instDecidableEqNumCircuitRel.decEq

@[reducible, inline]

abbrev FirstOrder.Language.ncBelow : Language.numCircuit.Relations 2

below h g: the digit held by h is at most as significant as the one held by g.

Equations

• FirstOrder.Language.ncBelow = FirstOrder.Language.numCircuitRel.below

The underlying circuit

def DescriptiveComplexity.circuitOfNum : FirstOrder.Language.circuit →ᴸ FirstOrder.Language.numCircuit

Forgetting the comparison of the outputs: the vocabulary of circuits, read in the vocabulary of circuits writing a number.

Equations

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

@[instance_reducible]

instance DescriptiveComplexity.numCircuitStructure (A : Type) [FirstOrder.Language.numCircuit.Structure A] : FirstOrder.Language.circuit.Structure A

A circuit writing a number is a circuit.

Equations

• DescriptiveComplexity.numCircuitStructure A = DescriptiveComplexity.circuitOfNum.reduct A

def DescriptiveComplexity.numCircuitEquiv {A B : Type} [FirstOrder.Language.numCircuit.Structure A] [FirstOrder.Language.numCircuit.Structure B] (e : FirstOrder.Language.numCircuit.Equiv A B) : FirstOrder.Language.circuit.Equiv A B

An isomorphism of circuits writing a number is an isomorphism of the underlying circuits.

Equations

• DescriptiveComplexity.numCircuitEquiv e = { toEquiv := e.toEquiv, map_fun' := ⋯, map_rel' := ⋯ }

The number

def DescriptiveComplexity.OutBit {A : Type} [FirstOrder.Language.numCircuit.Structure A] (g : A) : Prop

The output gate g holds the digit 1.

Equations

• DescriptiveComplexity.OutBit g = (FirstOrder.Language.Structure.RelMap FirstOrder.Language.ncOut ![g] ∧ DescriptiveComplexity.GateVal true g)

def DescriptiveComplexity.LowerOut {A : Type} [FirstOrder.Language.numCircuit.Structure A] (g h : A) : Prop

h is an output gate strictly below g.

Equations

• DescriptiveComplexity.LowerOut g h = (FirstOrder.Language.Structure.RelMap FirstOrder.Language.ncOut ![h] ∧ h ≠ g ∧ FirstOrder.Language.Structure.RelMap FirstOrder.Language.ncBelow ![h, g])

noncomputable def DescriptiveComplexity.outRank {A : Type} [FirstOrder.Language.numCircuit.Structure A] (g : A) : ℕ

The rank of a gate among the outputs: the number of output gates strictly below it.

Equations

• DescriptiveComplexity.outRank g = Nat.card { h : A // DescriptiveComplexity.LowerOut g h }

def DescriptiveComplexity.OutOrder (A : Type) [FirstOrder.Language.numCircuit.Structure A] : Prop

The comparison of the outputs is a linear order on them: reflexive, transitive, antisymmetric and total among the output gates.

Equations

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

noncomputable def DescriptiveComplexity.circuitNumber (A : Type) [FirstOrder.Language.numCircuit.Structure A] : ℕ

The number written by a circuit: each output gate deriving the value 1 contributes two to the power of its rank among the outputs; 0 unless the outputs are linearly ordered.

Equations

• DescriptiveComplexity.circuitNumber A = if DescriptiveComplexity.OutOrder A then ∑ᶠ (g : A), if DescriptiveComplexity.OutBit g then 2 ^ DescriptiveComplexity.outRank g else 0 else 0

Isomorphism-invariance and the bundled problem

theorem DescriptiveComplexity.circuitNumber_iso {A B : Type} [FirstOrder.Language.numCircuit.Structure A] [FirstOrder.Language.numCircuit.Structure B] (e : FirstOrder.Language.numCircuit.Equiv A B) : circuitNumber A = circuitNumber B

The number written is isomorphism-invariant.

noncomputable def DescriptiveComplexity.CircuitNumber : CountingProblem FirstOrder.Language.numCircuit

The number written by a circuit, as a counting problem on Language.numCircuit-structures: the function counterpart of DescriptiveComplexity.CVP.

Equations

• DescriptiveComplexity.CircuitNumber = { Count := fun (A : Type) (inst : FirstOrder.Language.numCircuit.Structure A) => DescriptiveComplexity.circuitNumber A, iso_invariant := ⋯ }