Unfolding circuits into formulas

Every wire of a program carries the function of a formula: unfold the gates below it into a tree, copying a gate once for each time it is read (Program.wireFormula). The formula of an output of a circuit (Circuit.toFormula) computes that output (Circuit.eval_toFormula) and has exactly its depth, whatever each operation costs (Circuit.depthWith_toFormula). Copying gates can make the formula exponentially larger than the circuit, but no larger than its depth allows: over a basis of fan-in at most r ≥ 2, the formula of an output of a circuit of depth d has fewer than r ^ d operation nodes (Circuit.size_toFormula_lt). So circuits of fan-in two and logarithmic depth are formulas of logarithmic depth and polynomial size Jukna, Chapter 6.

Main definitions

• Cslib.Circuits.Program.gateFormula, Cslib.Circuits.Program.wireFormula: the formulas unfolding the gates and the wires of a program.
• Cslib.Circuits.Circuit.toFormula: the formula unfolding an output of a circuit.

Main results

• Cslib.Circuits.Circuit.eval_toFormula, Cslib.Circuits.Circuit.Computes.toFormula: the formula of an output computes it.
• Cslib.Circuits.Circuit.depthWith_toFormula, Cslib.Circuits.Circuit.depth_toFormula_le: it is as deep as the output, so no deeper than the circuit.
• Cslib.Circuits.Circuit.size_toFormula_lt: under bounded fan-in, its size is at most exponential in the depth of the circuit.

References

• S. Jukna, Boolean Function Complexity: Advances and Frontiers

def Cslib.Circuits.Program.gateFormula {σ : Signature} {n g : ℕ} : Program σ n g → Fin g → Formula σ n

The formulas unfolding the gates of a program: a gate is its operation applied to the formulas of the wires it reads, so a gate read several times is copied.

def Cslib.Circuits.Program.wireFormula {σ : Signature} {n g : ℕ} (p : Program σ n g) : Wire n g → Formula σ n

The formula unfolding a wire of a program: an input, or the formula of a gate.

@[simp]

theorem Cslib.Circuits.Program.wireFormula_input {σ : Signature} {n g : ℕ} (p : Program σ n g) (i : Fin n) : p.wireFormula (Wire.input i) = Formula.input i

@[simp]

theorem Cslib.Circuits.Program.wireFormula_gate {σ : Signature} {n g : ℕ} (p : Program σ n g) (k : Fin g) : p.wireFormula (Wire.gate k) = p.gateFormula k

@[simp]

theorem Cslib.Circuits.Program.gateFormula_gate_last {σ : Signature} {n g : ℕ} (p : Program σ n g) (line : Line σ n g) : (p.gate line).gateFormula (Fin.last g) = Formula.gate line.op fun (a : Fin (σ.Arity line.op)) => p.wireFormula (line.wires a)

@[simp]

theorem Cslib.Circuits.Program.gateFormula_gate_castSucc {σ : Signature} {n g : ℕ} (p : Program σ n g) (line : Line σ n g) (k : Fin g) : (p.gate line).gateFormula k.castSucc = p.gateFormula k

@[simp]

theorem Cslib.Circuits.Program.wireFormula_gate_castSucc {σ : Signature} {n g : ℕ} (p : Program σ n g) (line : Line σ n g) (w : Wire n g) : (p.gate line).wireFormula w.castSucc = p.wireFormula w

@[simp]

theorem Cslib.Circuits.Program.eval_gateFormula {σ : Signature} {n g : ℕ} {U : Type u_1} (I : Interpretation σ U) (p : Program σ n g) (k : Fin g) (x : Fin n → U) : (p.gateFormula k).eval I x = p.eval I x k

The formula of a gate computes the gate.

@[simp]

theorem Cslib.Circuits.Program.eval_wireFormula {σ : Signature} {n g : ℕ} {U : Type u_1} (I : Interpretation σ U) (p : Program σ n g) (w : Wire n g) (x : Fin n → U) : (p.wireFormula w).eval I x = p.trace I x w

The formula of a wire computes the wire.

@[simp]

theorem Cslib.Circuits.Program.depthWith_gateFormula {σ : Signature} {n g : ℕ} (cost : σ.Op → ℕ) (p : Program σ n g) (k : Fin g) : Formula.depthWith cost (p.gateFormula k) = depthsWith cost p k

The formula of a gate is as deep as the gate, whatever each operation costs.

@[simp]

theorem Cslib.Circuits.Program.depthWith_wireFormula {σ : Signature} {n g : ℕ} (cost : σ.Op → ℕ) (p : Program σ n g) (w : Wire n g) : Formula.depthWith cost (p.wireFormula w) = wireDepthsWith cost p w

The formula of a wire is as deep as the wire, whatever each operation costs.

@[simp]

theorem Cslib.Circuits.Program.depth_wireFormula {σ : Signature} {n g : ℕ} (p : Program σ n g) (w : Wire n g) : (p.wireFormula w).depth = p.wireDepths w

The formula of a wire is as deep as the wire.

def Cslib.Circuits.Circuit.toFormula {σ : Signature} {n m : ℕ} (C : Circuit σ n m) (j : Fin m) : Formula σ n

The formula unfolding output j of a circuit.

@[simp]

theorem Cslib.Circuits.Circuit.eval_toFormula {σ : Signature} {n m : ℕ} {U : Type u_1} (C : Circuit σ n m) (j : Fin m) (I : Interpretation σ U) (x : Fin n → U) : (C.toFormula j).eval I x = C.eval I x j

The formula of an output computes the output.

theorem Cslib.Circuits.Circuit.Computes.toFormula {σ : Signature} {n m : ℕ} {U : Type u_1} {C : Circuit σ n m} {I : Interpretation σ U} {f : (Fin n → U) → Fin m → U} (h : C.Computes I f) (j : Fin m) : (C.toFormula j).Computes I fun (x : Fin n → U) => f x j

The formula of an output of a circuit computing f computes that output of f.

@[simp]

theorem Cslib.Circuits.Circuit.depthWith_toFormula {σ : Signature} {n m : ℕ} (C : Circuit σ n m) (j : Fin m) (cost : σ.Op → ℕ) : Formula.depthWith cost (C.toFormula j) = Program.wireDepthsWith cost C.program (C.outputs j)

The formula of an output is as deep as the output, whatever each operation costs.

theorem Cslib.Circuits.Circuit.depthWith_toFormula_le {σ : Signature} {n m : ℕ} (C : Circuit σ n m) (j : Fin m) (cost : σ.Op → ℕ) : Formula.depthWith cost (C.toFormula j) ≤ depthWith cost C

The formula of an output is no deeper than the circuit, whatever each operation costs.

@[simp]

theorem Cslib.Circuits.Circuit.depth_toFormula {σ : Signature} {n m : ℕ} (C : Circuit σ n m) (j : Fin m) : (C.toFormula j).depth = C.outputDepths j

The formula of an output is as deep as the output.

theorem Cslib.Circuits.Circuit.depth_toFormula_le {σ : Signature} {n m : ℕ} (C : Circuit σ n m) (j : Fin m) : (C.toFormula j).depth ≤ C.depth

The formula of an output is no deeper than the circuit.

theorem Cslib.Circuits.Circuit.size_toFormula_lt {σ : Signature} {n m : ℕ} (C : Circuit σ n m) (j : Fin m) {r : ℕ} (hr : ∀ (op : σ.Op), σ.Arity op ≤ r) (hr₂ : 2 ≤ r) : (C.toFormula j).size < r ^ C.depth

Over a basis of fan-in at most r, where 2 ≤ r, the formula of an output of a circuit of depth d has fewer than r ^ d operation nodes.