Circuits

A circuit is a straight-line Program together with a choice of output wires. Any input or internal-gate wire may be designated as an output, and designating an output is free: projections and duplicated outputs cost no gates. The size of a circuit is its gate count and its depth is the maximum depth of a designated output wire.

For the standard Boolean circuit model, see [Arora and Barak, Section 6.1][AroraBarak09]. Here a topological ordering is part of the representation, and the Boolean gate basis is generalized to an arbitrary Signature and Interpretation. Our size counts only operation gates; Arora and Barak count all nodes, including inputs. An output wire may also supply a later gate.

A circuit computes a function with as many values as it has outputs when its designated outputs agree with the function on every input; a single-valued function is computed by a circuit with one output. Evaluation commutes with homomorphisms of interpretations.

References

• [S. Arora and B. Barak, Computational Complexity: A Modern Approach, Section 6.1][AroraBarak09]

structure Cslib.Circuits.Circuit (σ : Signature) (inputCount outputCount : ℕ) : Type u_1

A straight-line program with designated output wires.

• size : ℕ

  The number of gates in the program; inputs and designated outputs cost nothing.

• program : Program σ inputCount self.size

  The internal gates of the circuit.

• outputs : Fin outputCount → Wire inputCount self.size

  The input or internal-gate wire carrying each output.

def Cslib.Circuits.Circuit.wiring {inputCount outputCount : ℕ} (σ : Signature) (select : Fin outputCount → Fin inputCount) : Circuit σ inputCount outputCount

The zero-gate circuit whose outputs are the inputs chosen by select. Projections, duplications, and permutations of the inputs cost no gates.

Equations

• Cslib.Circuits.Circuit.wiring σ select = { size := 0, program := Cslib.Circuits.Program.empty, outputs := fun (output : Fin outputCount) => Cslib.Circuits.Wire.input (select output) }

@[reducible, inline]

abbrev Cslib.Circuits.Circuit.id (σ : Signature) (inputCount : ℕ) : Circuit σ inputCount inputCount

The zero-gate identity circuit, whose outputs are its inputs.

Equations

• Cslib.Circuits.Circuit.id σ inputCount = Cslib.Circuits.Circuit.wiring σ id

@[simp]

theorem Cslib.Circuits.Circuit.size_wiring {σ : Signature} {inputCount outputCount : ℕ} (select : Fin outputCount → Fin inputCount) : (wiring σ select).size = 0

@[simp]

theorem Cslib.Circuits.Circuit.program_wiring {σ : Signature} {inputCount outputCount : ℕ} (select : Fin outputCount → Fin inputCount) : (wiring σ select).program = Program.empty

@[simp]

theorem Cslib.Circuits.Circuit.outputs_wiring {σ : Signature} {inputCount outputCount : ℕ} (select : Fin outputCount → Fin inputCount) : (wiring σ select).outputs = fun (output : Fin outputCount) => Wire.input (select output)

def Cslib.Circuits.Circuit.FanInAtMost {σ : Signature} {inputCount outputCount : ℕ} (c : Circuit σ inputCount outputCount) (r : ℕ) : Prop

Every gate in a circuit has at most r arguments.

Equations

• c.FanInAtMost r = c.program.FanInAtMost r

@[instance_reducible]

instance Cslib.Circuits.Circuit.instDecidableFanInAtMost {σ : Signature} {inputCount outputCount : ℕ} (c : Circuit σ inputCount outputCount) (r : ℕ) : Decidable (c.FanInAtMost r)

Bounded fan-in is decidable for every concrete circuit.

Equations

• c.instDecidableFanInAtMost r = c.program.instDecidableFanInAtMost r

@[simp]

theorem Cslib.Circuits.Circuit.fanInAtMost_wiring {σ : Signature} {inputCount outputCount : ℕ} (select : Fin outputCount → Fin inputCount) (r : ℕ) : (wiring σ select).FanInAtMost r

def Cslib.Circuits.Circuit.outputDepths {σ : Signature} {inputCount outputCount : ℕ} (c : Circuit σ inputCount outputCount) : Fin outputCount → ℕ

The depth of every designated output wire in a circuit.

Equations

• c.outputDepths = c.program.wireDepths ∘ c.outputs

def Cslib.Circuits.Circuit.depth {σ : Signature} {inputCount outputCount : ℕ} (c : Circuit σ inputCount outputCount) : ℕ

The maximum depth of a designated output wire in a circuit.

Equations

• c.depth = Fin.foldl outputCount (fun (depth : ℕ) (k : Fin outputCount) => max depth (c.outputDepths k)) 0

@[simp]

theorem Cslib.Circuits.Circuit.outputDepths_wiring {σ : Signature} {inputCount outputCount : ℕ} (select : Fin outputCount → Fin inputCount) : (wiring σ select).outputDepths = fun (x : Fin outputCount) => 0

@[simp]

theorem Cslib.Circuits.Circuit.depth_wiring {σ : Signature} {inputCount outputCount : ℕ} (select : Fin outputCount → Fin inputCount) : (wiring σ select).depth = 0

def Cslib.Circuits.Circuit.eval {σ : Signature} {inputCount outputCount : ℕ} {U : Type u} (c : Circuit σ inputCount outputCount) (i : Interpretation σ U) (x : Fin inputCount → U) : Fin outputCount → U

Read the designated output wires after evaluating the program.

Equations

• c.eval i x = c.program.trace i x ∘ c.outputs

@[simp]

theorem Cslib.Circuits.Circuit.eval_wiring {σ : Signature} {inputCount outputCount : ℕ} {U : Type u} (select : Fin outputCount → Fin inputCount) (interpretation : Interpretation σ U) (input : Fin inputCount → U) : (wiring σ select).eval interpretation input = input ∘ select

Output j of a wiring circuit is input select j.

def Cslib.Circuits.Circuit.Computes {σ : Signature} {inputCount outputCount : ℕ} {U : Type u} (c : Circuit σ inputCount outputCount) (interpretation : Interpretation σ U) (f : (Fin inputCount → U) → Fin outputCount → U) : Prop

A circuit computes f when its outputs agree with f on every input.

Equations

• c.Computes interpretation f = ∀ (x : Fin inputCount → U), c.eval interpretation x = f x

def Cslib.Circuits.Circuit.ComputesOn {σ : Signature} {inputCount outputCount : ℕ} {U : Type u} (c : Circuit σ inputCount outputCount) (interpretation : Interpretation σ U) (S : Set (Fin inputCount → U)) (f : (Fin inputCount → U) → Fin outputCount → U) : Prop

A circuit computes f on the support S when its outputs agree with f on every input in S; what f does outside S does not matter.

Equations

• c.ComputesOn interpretation S f = Set.EqOn (c.eval interpretation) f S

@[simp]

theorem Cslib.Circuits.Circuit.computesOn_univ_iff {σ : Signature} {inputCount outputCount : ℕ} {U : Type u} (c : Circuit σ inputCount outputCount) (interpretation : Interpretation σ U) (f : (Fin inputCount → U) → Fin outputCount → U) : c.ComputesOn interpretation Set.univ f ↔ c.Computes interpretation f

Computing on every input is computing.

theorem Cslib.Circuits.Circuit.Computes.computesOn {σ : Signature} {inputCount outputCount : ℕ} {U : Type u} {c : Circuit σ inputCount outputCount} {interpretation : Interpretation σ U} {f : (Fin inputCount → U) → Fin outputCount → U} (h : c.Computes interpretation f) (S : Set (Fin inputCount → U)) : c.ComputesOn interpretation S f

A circuit that computes f computes it on every support.

theorem Cslib.Circuits.Circuit.wiring_computes {σ : Signature} {inputCount outputCount : ℕ} {U : Type u} (select : Fin outputCount → Fin inputCount) (interpretation : Interpretation σ U) : (wiring σ select).Computes interpretation fun (x : Fin inputCount → U) => x ∘ select

A wiring circuit computes the selection of its inputs.

theorem Cslib.Circuits.Circuit.map_eval {σ : Signature} {inputCount outputCount : ℕ} {U₁ : Type u₁} {U₂ : Type u₂} {i₁ : Interpretation σ U₁} {i₂ : Interpretation σ U₂} (c : Circuit σ inputCount outputCount) (h : Homomorphism i₁ i₂) (x : Fin inputCount → U₁) : h.map ∘ c.eval i₁ x = c.eval i₂ (h.map ∘ x)

Evaluating a circuit commutes with a homomorphism.

def Cslib.Circuits.Circuit.computation {σ : Signature} {inputCount outputCount : ℕ} {U : Type u} (c : Circuit σ inputCount outputCount) (i : Interpretation σ U) (x : Fin inputCount → U) : Fin (c.size + outputCount) → U

All internal-gate values followed by the designated output values.

Equations

• c.computation i✝ x i = Fin.addCases (c.program.eval i✝ x) (c.eval i✝ x) i

def Cslib.Circuits.Circuit.trace {σ : Signature} {inputCount outputCount : ℕ} {U : Type u} (c : Circuit σ inputCount outputCount) (i : Interpretation σ U) (x : Fin inputCount → U) : Fin (inputCount + c.size + outputCount) → U

The input and internal-gate values followed by the designated outputs.

Equations

• c.trace i✝ x i = Fin.addCases (fun (i : Fin (inputCount + c.size)) => Fin.addCases x (c.program.eval i✝ x) i) (c.eval i✝ x) i