AC⁰ and parity

AC⁰ is the class of languages decided, at every input length, by circuits of negations and conjunctions and disjunctions of unbounded fan-in, of polynomial size and constant depth Arora and Barak, Section 6.7.1. By Håstad's theorem (Unbounded.two_pow_le_size_of_computes_parity), parity is not in AC⁰ Arora and Barak, Theorem 14.1, [FSS84], [Ajt83], [Has86].

Over any basis containing the unbounded fan-in basis through a meaning-preserving map φ, the small circuits constCircuit φ, notCircuit φ and binCircuit φ show that polynomial-size constant-depth circuits decide the constant languages and are closed under the Boolean operations (ConstDepth.bot_mem, ConstDepth.top_mem, ConstDepth.compl, ConstDepth.inf, ConstDepth.sup); for AC⁰ take φ the identity.

Main definitions

• Cslib.Circuits.Boolean.AC0: the class AC⁰.
• Cslib.Circuits.Boolean.Unbounded.constCircuit, notCircuit, binCircuit: a constant, a negation, and a gate of two arguments on top of circuits.

Main results

• Cslib.Circuits.Boolean.parity_notMem_AC0: parity is not in AC⁰.
• Cslib.Circuits.Boolean.ConstDepth.compl, ConstDepth.inf, ConstDepth.sup: closure under the Boolean operations.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• M. Furst, J. B. Saxe, M. Sipser, Parity, circuits, and the polynomial-time hierarchy
• M. Ajtai, Σ¹₁-formulae on finite structures
• J. Håstad, Almost optimal lower bounds for small depth circuits

Small circuits over a basis containing the unbounded fan-in basis

def Cslib.Circuits.Boolean.Unbounded.constCircuit {n : ℕ} {σ : Signature} (φ : signature.Hom σ) : Bool → Circuit σ n 1

The constant b, as one gate: the conjunction or the disjunction of no arguments.

def Cslib.Circuits.Boolean.Unbounded.notCircuit {n : ℕ} {σ : Signature} (φ : signature.Hom σ) (C : Circuit σ n 1) : Circuit σ n 1

The circuit C followed by a negation.

def Cslib.Circuits.Boolean.Unbounded.binCircuit {n : ℕ} {σ : Signature} (φ : signature.Hom σ) (op : Op) (h : op.arity = 2) (C D : Circuit σ n 1) : Circuit σ n 1

The circuits C and D side by side, followed by a gate op of two arguments.

@[simp]

theorem Cslib.Circuits.Boolean.Unbounded.eval_constCircuit {n : ℕ} {σ : Signature} {φ : signature.Hom σ} {I : Interpretation σ Bool} [φ.Preserves interpretation I] (b : Bool) (x : BitString n) (j : Fin 1) : (constCircuit φ b).eval I x j = b

@[simp]

theorem Cslib.Circuits.Boolean.Unbounded.size_constCircuit {n : ℕ} {σ : Signature} {φ : signature.Hom σ} (b : Bool) : (constCircuit φ b).size = 1

theorem Cslib.Circuits.Boolean.Unbounded.depth_constCircuit_le {n : ℕ} {σ : Signature} {φ : signature.Hom σ} (b : Bool) : (constCircuit φ b).depth ≤ 1

A constant has depth at most one.

@[simp]

theorem Cslib.Circuits.Boolean.Unbounded.eval_notCircuit {n : ℕ} {σ : Signature} {φ : signature.Hom σ} {I : Interpretation σ Bool} [φ.Preserves interpretation I] (C : Circuit σ n 1) (x : BitString n) (j : Fin 1) : (notCircuit φ C).eval I x j = !C.eval I x 0

@[simp]

theorem Cslib.Circuits.Boolean.Unbounded.size_notCircuit {n : ℕ} {σ : Signature} {φ : signature.Hom σ} (C : Circuit σ n 1) : (notCircuit φ C).size = C.size + 1

theorem Cslib.Circuits.Boolean.Unbounded.depth_notCircuit_le {n : ℕ} {σ : Signature} {φ : signature.Hom σ} (C : Circuit σ n 1) : (notCircuit φ C).depth ≤ C.depth + 1

A negation adds one to the depth.

theorem Cslib.Circuits.Boolean.Unbounded.eval_binCircuit {n : ℕ} {σ : Signature} {φ : signature.Hom σ} {I : Interpretation σ Bool} [φ.Preserves interpretation I] (op : Op) (h : op.arity = 2) (C D : Circuit σ n 1) (x : BitString n) (j : Fin 1) : (binCircuit φ op h C D).eval I x j = interpretation op fun (a : Fin (signature.Arity op)) => ![C.eval I x 0, D.eval I x 0] (Fin.cast h a)

The gate of binCircuit φ op h C D applied to the outputs of C and D.

@[simp]

theorem Cslib.Circuits.Boolean.Unbounded.eval_binCircuit_and {n : ℕ} {σ : Signature} {φ : signature.Hom σ} {I : Interpretation σ Bool} [φ.Preserves interpretation I] (C D : Circuit σ n 1) (x : BitString n) (j : Fin 1) : (binCircuit φ (Op.and 2) ⋯ C D).eval I x j = (C.eval I x 0 && D.eval I x 0)

@[simp]

theorem Cslib.Circuits.Boolean.Unbounded.eval_binCircuit_or {n : ℕ} {σ : Signature} {φ : signature.Hom σ} {I : Interpretation σ Bool} [φ.Preserves interpretation I] (C D : Circuit σ n 1) (x : BitString n) (j : Fin 1) : (binCircuit φ (Op.or 2) ⋯ C D).eval I x j = (C.eval I x 0 || D.eval I x 0)

@[simp]

theorem Cslib.Circuits.Boolean.Unbounded.size_binCircuit {n : ℕ} {σ : Signature} {φ : signature.Hom σ} (op : Op) (h : op.arity = 2) (C D : Circuit σ n 1) : (binCircuit φ op h C D).size = C.size + D.size + 1

theorem Cslib.Circuits.Boolean.Unbounded.depth_binCircuit_le {n : ℕ} {σ : Signature} {φ : signature.Hom σ} (op : Op) (h : op.arity = 2) (C D : Circuit σ n 1) : (binCircuit φ op h C D).depth ≤ max C.depth D.depth + 1

A gate of two arguments adds one to the larger depth.

AC⁰

def Cslib.Circuits.Boolean.AC0 : Set (Language Bool)

AC⁰: the languages over Bool decided, at every input length, by circuits of negations and unbounded fan-in conjunctions and disjunctions of polynomially bounded size and constant depth.

theorem Cslib.Circuits.Boolean.parity_notMem_AC0 : Language.ofSlices parity ∉ AC0

Parity is not in AC⁰.

Closure under the Boolean operations

theorem Cslib.Circuits.Boolean.ConstDepth.bot_mem {σ : Signature} {I : Interpretation σ Bool} (φ : Unbounded.signature.Hom σ) [φ.Preserves Unbounded.interpretation I] : ⊥ ∈ ConstDepth I

The empty language has constant-depth circuits over a basis containing the unbounded fan-in basis.

theorem Cslib.Circuits.Boolean.ConstDepth.top_mem {σ : Signature} {I : Interpretation σ Bool} (φ : Unbounded.signature.Hom σ) [φ.Preserves Unbounded.interpretation I] : ⊤ ∈ ConstDepth I

The full language has constant-depth circuits over a basis containing the unbounded fan-in basis.

theorem Cslib.Circuits.Boolean.ConstDepth.compl {σ : Signature} {I : Interpretation σ Bool} {L : Language Bool} (φ : Unbounded.signature.Hom σ) [φ.Preserves Unbounded.interpretation I] (hL : L ∈ ConstDepth I) : Lᶜ ∈ ConstDepth I

Over a basis containing the unbounded fan-in basis, constant-depth circuits are closed under complement.

theorem Cslib.Circuits.Boolean.ConstDepth.inf {σ : Signature} {I : Interpretation σ Bool} {L M : Language Bool} (φ : Unbounded.signature.Hom σ) [φ.Preserves Unbounded.interpretation I] (hL : L ∈ ConstDepth I) (hM : M ∈ ConstDepth I) : L ⊓ M ∈ ConstDepth I

Over a basis containing the unbounded fan-in basis, constant-depth circuits are closed under intersection.

theorem Cslib.Circuits.Boolean.ConstDepth.sup {σ : Signature} {I : Interpretation σ Bool} {L M : Language Bool} (φ : Unbounded.signature.Hom σ) [φ.Preserves Unbounded.interpretation I] (hL : L ∈ ConstDepth I) (hM : M ∈ ConstDepth I) : L ⊔ M ∈ ConstDepth I

Over a basis containing the unbounded fan-in basis, constant-depth circuits are closed under union.