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.
• Cslib.Circuits.Program.gateFormula_eq_gate, Cslib.Circuits.Program.exists_wireFormula_eq_of_eq_gate: the formula of a gate is its operation applied to the formulas of the wires it reads, so the formulas of the wires are closed under taking arguments.
• Cslib.Circuits.Formula.toFormula_toCircuit, Cslib.Circuits.Formula.gateFormula_toCircuit_of_closed: the circuit of a formula unfolds to the formula, and the formulas of its gates are subformulas.

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

Unfolding an input wire .input i gives the input 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

Unfolding a gate wire .gate k gives the gate formula 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)

The formula of the newly added last gate is line.op applied to the formulas of its argument wires.

@[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

Appending a gate leaves the formulas of earlier gates unchanged.

@[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

Appending a gate leaves the formulas of earlier wires unchanged.

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

The formula of a gate is its operation applied to the formulas of the wires its line reads.

theorem Cslib.Circuits.Program.exists_wireFormula_eq_of_eq_gate {σ : Signature} {n g : ℕ} (p : Program σ n g) {w : Wire n g} {op : σ.Op} {args : Fin (σ.Arity op) → Formula σ n} (h : p.wireFormula w = Formula.gate op args) (j : Fin (σ.Arity op)) : ∃ (w' : Wire n g), p.wireFormula w' = args j

The arguments of the root of the formula of a wire are formulas of wires: the formulas of the wires of a program are closed under taking arguments.

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

Unfolding the circuit of a formula

@[simp]

theorem Cslib.Circuits.Program.wireFormula_append_castAdd {σ : Signature} {n k g₁ g₂ : ℕ} (p : Program σ n g₁) (feed : Fin k → Wire n g₁) (q : Program σ k g₂) (w : Wire n g₁) : (p.append feed q).wireFormula (Wire.castAdd g₂ w) = p.wireFormula w

Continuing p by q leaves the formulas of the wires of p unchanged.

@[simp]

theorem Cslib.Circuits.Program.wireFormula_append_input_appendedWire {σ : Signature} {n g₁ g₂ : ℕ} (p : Program σ n g₁) (q : Program σ n g₂) (w : Wire n g₂) : (p.append Wire.input q).wireFormula (appendedWire Wire.input w) = q.wireFormula w

Continuing p by q on the inputs, a wire of q unfolds to its formula in q.

theorem Cslib.Circuits.Program.gateFormula_append_input_of_forall {σ : Signature} {n g₁ g₂ : ℕ} (P : Formula σ n → Prop) (p : Program σ n g₁) (q : Program σ n g₂) (hp : ∀ (k : Fin g₁), P (p.gateFormula k)) (hq : ∀ (k : Fin g₂), P (q.gateFormula k)) (k : Fin (g₁ + g₂)) : P ((p.append Wire.input q).gateFormula k)

The formulas of the gates of p continued by q on the inputs are formulas of gates of p or of q.

@[simp]

theorem Cslib.Circuits.Circuit.toFormula_pi {σ : Signature} {n m : ℕ} (cs : Fin m → Circuit σ n 1) (j : Fin m) : (pi cs).toFormula j = (cs j).toFormula 0

Output j of circuits side by side unfolds to the output of the j-th circuit.

theorem Cslib.Circuits.Circuit.gateFormula_pi_of_forall {σ : Signature} {n : ℕ} (P : Formula σ n → Prop) {m : ℕ} (cs : Fin m → Circuit σ n 1) (h : ∀ (j : Fin m) (k : Fin (cs j).size), P ((cs j).program.gateFormula k)) (k : Fin (pi cs).size) : P ((pi cs).program.gateFormula k)

The formulas of the gates of circuits side by side are formulas of gates of the circuits.

@[simp]

theorem Cslib.Circuits.Formula.toFormula_toCircuit {σ : Signature} {n : ℕ} (F : Formula σ n) : F.toCircuit.toFormula 0 = F

The circuit of a formula unfolds to the formula.

theorem Cslib.Circuits.Formula.gateFormula_toCircuit_of_closed {σ : Signature} {n : ℕ} (P : Formula σ n → Prop) (hP : ∀ (op : σ.Op) (args : Fin (σ.Arity op) → Formula σ n) (j : Fin (σ.Arity op)), P (gate op args) → P (args j)) {F : Formula σ n} (hF : P F) (k : Fin F.toCircuit.size) : P (F.toCircuit.program.gateFormula k)

The formulas of the gates of the circuit of a formula F are subformulas of F: they satisfy every property of F inherited by the arguments of operation nodes.