Simulating unbounded fan-in with fan-in two

A disjunction of k ≥ 1 arguments is a balanced tree of k - 1 disjunctions of fan-in two, of depth ⌈log₂ k⌉ (Formula.size_orList_add_one, Formula.depthWith_orList_le), and so is a conjunction. Replacing every gate of a circuit over the unbounded fan-in basis by such a tree gives a De Morgan circuit for the same function. A gate may read one wire many times, so its fan-in is not bounded by the size of the circuit; but a conjunction or a disjunction keeps its value when it reads each of its wires once, so every circuit with n inputs and s gates has an equivalent circuit of the same size and no larger depth whose gates have fan-in at most n + s (Unbounded.dedup). Replacing its gates gives a De Morgan circuit with at most s (n + s) gates and depth at most max 1 ⌈log₂ (n + s)⌉ · d (Unbounded.exists_deMorgan_simulation).

For circuits of polynomial size log (n + s) is O(log n), so polynomial-size circuits of depth O((log n) ^ i) and unbounded fan-in become polynomial-size circuits of fan-in two and depth O((log n) ^ (i + 1)): ACⁱ ⊆ NCⁱ⁺¹ (AC_subset_NC_succ) Arora and Barak, Section 6.7, Vollmer, Chapter 4. With NCⁱ ⊆ ACⁱ, the two hierarchies have the same union (iUnion_NC_eq_iUnion_AC).

Main definitions

• Cslib.Circuits.Boolean.Unbounded.dedup: the circuit whose gates read their distinct wires.
• Cslib.Circuits.Boolean.Unbounded.Op.deMorganFormula: a De Morgan formula for each operation of the unbounded fan-in basis.

Main results

• Cslib.Circuits.Boolean.Unbounded.eval_dedup, Cslib.Circuits.Boolean.Unbounded.depth_dedup_le, Cslib.Circuits.Boolean.Unbounded.fanInAtMost_dedup: reading every wire once keeps the function and the size, makes no gate deeper, and bounds the fan-in by the number of inputs and gates.
• Cslib.Circuits.Boolean.Unbounded.exists_deMorgan_simulation: a circuit of unbounded fan-in with n inputs, s gates and depth d has an equivalent De Morgan circuit with at most s (n + s) gates and depth at most max 1 ⌈log₂ (n + s)⌉ · d.
• Cslib.Circuits.Boolean.AC_subset_NC_succ: ACⁱ ⊆ NCⁱ⁺¹.
• Cslib.Circuits.Boolean.AC0_subset_NC_one: AC⁰ ⊆ NC¹.
• Cslib.Circuits.Boolean.iUnion_NC_eq_iUnion_AC: NC = AC.
• Cslib.Circuits.Boolean.AC_subset_PPoly: ACⁱ ⊆ P/poly.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• H. Vollmer, Introduction to Circuit Complexity

Reading every wire once

def Cslib.Circuits.Boolean.Unbounded.dedupLine {n g : ℕ} : Line signature n g → Line signature n g

The line reading the distinct wires of line, each once. A conjunction or a disjunction does not depend on how often it reads a wire, so this keeps the value of the line.

theorem Cslib.Circuits.Boolean.Unbounded.eval_dedupLine {n g : ℕ} (line : Line signature n g) (x : Fin n → Bool) (gates : Fin g → Bool) : (dedupLine line).eval interpretation x gates = line.eval interpretation x gates

Reading every wire once keeps the value of a line.

theorem Cslib.Circuits.Boolean.Unbounded.depth_dedupLine_le {n g : ℕ} (line : Line signature n g) (depths : Wire n g → ℕ) : (dedupLine line).depth depths ≤ line.depth depths

Reading every wire once makes no line deeper.

theorem Cslib.Circuits.Boolean.Unbounded.arity_dedupLine_le {n g : ℕ} (line : Line signature n g) : signature.Arity (dedupLine line).op ≤ n + g

A line reading every wire once reads at most all n + g wires.

def Cslib.Circuits.Boolean.Unbounded.dedup {n m : ℕ} (C : Circuit signature n m) : Circuit signature n m

The circuit whose gates read their distinct wires, each once. It computes the same function (eval_dedup) with the same size and no larger depth (depth_dedup_le), and its gates have fan-in at most the number of inputs and gates (fanInAtMost_dedup).

@[simp]

theorem Cslib.Circuits.Boolean.Unbounded.size_dedup {n m : ℕ} (C : Circuit signature n m) : (dedup C).size = C.size

Reading every wire once keeps the size.

@[simp]

theorem Cslib.Circuits.Boolean.Unbounded.eval_dedup {n m : ℕ} (C : Circuit signature n m) : (dedup C).eval interpretation = C.eval interpretation

Reading every wire once keeps the function computed.

theorem Cslib.Circuits.Boolean.Unbounded.depth_dedup_le {n m : ℕ} (C : Circuit signature n m) : (dedup C).depth ≤ C.depth

Reading every wire once makes no gate deeper.

theorem Cslib.Circuits.Boolean.Unbounded.arity_lines_dedup_le {n m : ℕ} (C : Circuit signature n m) (k : Fin C.size) : signature.Arity ((dedup C).program.lines k).op ≤ n + C.size

Every gate of dedup C reads at most all n + C.size wires.

theorem Cslib.Circuits.Boolean.Unbounded.fanInAtMost_dedup {n m : ℕ} (C : Circuit signature n m) : (dedup C).FanInAtMost (n + C.size)

Fan-in reduction: the gates of dedup C have fan-in at most the number of inputs and gates of C.

Balanced trees for the gates

def Cslib.Circuits.Boolean.Unbounded.Op.deMorganFormula (op : Op) : Formula Boolean.signature op.arity

A De Morgan formula for each operation of the unbounded fan-in basis: the negation of the input, and the balanced conjunction and disjunction of the inputs.

theorem Cslib.Circuits.Boolean.Unbounded.Op.computes_deMorganFormula (op : Op) : op.deMorganFormula.Computes Boolean.interpretation (interpretation op)

The De Morgan formula of an operation computes it.

theorem Cslib.Circuits.Boolean.Unbounded.Op.size_deMorganFormula_le (op : Op) : op.deMorganFormula.size ≤ max 1 op.arity

The De Morgan formula of an operation of k arguments has at most max 1 k nodes: one negation, a constant for no arguments, and k - 1 binary gates for k ≥ 1 arguments.

theorem Cslib.Circuits.Boolean.Unbounded.Op.depth_deMorganFormula_le (op : Op) : op.deMorganFormula.depth ≤ max 1 (Nat.clog 2 op.arity)

The De Morgan formula of an operation of k arguments has depth at most max 1 ⌈log₂ k⌉: one for a negation or a constant, and ⌈log₂ k⌉ for a balanced tree of k ≥ 1 arguments.

Simulation

theorem Cslib.Circuits.Boolean.Unbounded.exists_deMorgan_simulation {n m : ℕ} (C : Circuit signature n m) : ∃ (D : Circuit Boolean.signature n m), D.eval Boolean.interpretation = C.eval interpretation ∧ D.size ≤ C.size * (n + C.size) ∧ D.depth ≤ max 1 (Nat.clog 2 (n + C.size)) * C.depth

Fan-in two simulates unbounded fan-in Arora and Barak, Section 6.7: a circuit of unbounded fan-in with n inputs, s gates and depth d has an equivalent De Morgan circuit with at most s (n + s) gates and depth at most max 1 ⌈log₂ (n + s)⌉ · d. Its gates are first made to read every wire once (dedup), and then replaced by balanced trees.

ACⁱ ⊆ NCⁱ⁺¹

theorem Cslib.Circuits.Boolean.AC_subset_NC_succ (i : ℕ) : AC i ⊆ NC (i + 1)

ACⁱ ⊆ NCⁱ⁺¹ Arora and Barak, Section 6.7, Vollmer, Chapter 4: polynomial-size circuits of depth O((log n) ^ i) and unbounded fan-in are simulated by polynomial-size circuits of depth O((log n) ^ (i + 1)) and fan-in two.

theorem Cslib.Circuits.Boolean.AC0_subset_NC_one : AC0 ⊆ NC 1

AC⁰ ⊆ NC¹.

theorem Cslib.Circuits.Boolean.iUnion_NC_eq_iUnion_AC : ⋃ (i : ℕ), NC i = ⋃ (i : ℕ), AC i

NC = AC: the NC and AC hierarchies have the same union.

theorem Cslib.Circuits.Boolean.AC_subset_PPoly (i : ℕ) : AC i ⊆ PPoly

ACⁱ ⊆ P/poly for every i.