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. 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.

This file defines evaluation (Circuit.eval), the flattened views Circuit.computation and Circuit.trace, the zero-gate identity circuit Circuit.id, and the structural bounded-fan-in predicate Circuit.FanInAtMost. Evaluation commutes with homomorphisms (Circuit.map_eval).

References

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

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

A straight-line program with designated output wires.

• program : Program σ inputCount gateCount

  The internal gates of the circuit.

• outputs : Fin outputCount → Wire inputCount gateCount

  The input or internal-gate wire carrying each output.

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

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

Equations

• Cslib.Circuits.Circuit.id σ inputCount = { program := Cslib.Circuits.Program.empty, outputs := fun (input : Fin inputCount) => Cslib.Circuits.Wire.input input }

def Cslib.Circuits.Circuit.FanInAtMost {σ : Signature} {inputCount gateCount outputCount : ℕ} (c : Circuit σ inputCount gateCount 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 gateCount outputCount : ℕ} (c : Circuit σ inputCount gateCount outputCount) (r : ℕ) : Decidable (c.FanInAtMost r)

Bounded fan-in is decidable for every concrete circuit.

Equations

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

def Cslib.Circuits.Circuit.size {σ : Signature} {inputCount gateCount outputCount : ℕ} : Circuit σ inputCount gateCount outputCount → ℕ

The number of gates in a circuit. Designating outputs is free.

Equations

• x✝.size = gateCount

def Cslib.Circuits.Circuit.outputDepths {σ : Signature} {inputCount gateCount outputCount : ℕ} (c : Circuit σ inputCount gateCount 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 gateCount outputCount : ℕ} (c : Circuit σ inputCount gateCount outputCount) : ℕ

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

Equations

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

def Cslib.Circuits.Circuit.eval {σ : Signature} {inputCount gateCount outputCount : ℕ} {U : Type u} (c : Circuit σ inputCount gateCount 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

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

A single-output circuit computes f when its output agrees with f on every input.

Equations

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

@[simp]

theorem Cslib.Circuits.Circuit.eval_id {σ : Signature} {inputCount : ℕ} {U : Type u} (interpretation : Interpretation σ U) (input : Fin inputCount → U) : (id σ inputCount).eval interpretation input = input

theorem Cslib.Circuits.Circuit.map_eval {σ : Signature} {inputCount gateCount outputCount : ℕ} {U₁ : Type u₁} {U₂ : Type u₂} {i₁ : Interpretation σ U₁} {i₂ : Interpretation σ U₂} (c : Circuit σ inputCount gateCount 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 gateCount outputCount : ℕ} {U : Type u} (c : Circuit σ inputCount gateCount outputCount) (i : Interpretation σ U) (x : Fin inputCount → U) : Fin (gateCount + 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 gateCount outputCount : ℕ} {U : Type u} (c : Circuit σ inputCount gateCount outputCount) (i : Interpretation σ U) (x : Fin inputCount → U) : Fin (inputCount + gateCount + outputCount) → U

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

Equations

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