Definition, divisibility monotonicity, and Boolean closure of ACC⁰

ACC⁰ (Cslib.Circuits.Boolean.ACC0) is the union of the modular constant-depth circuit classes AC0Mod q over all fixed moduli q ≥ 2 [Bar89], Vollmer, Chapter 4, Arora and Barak, Section 14.2: the languages over Bool decided at every input length by polynomial-size, constant-depth nonuniform circuits over negations, unbounded fan-in conjunctions and disjunctions, and unbounded fan-in MOD_q gates (modGate q). Since modGate 0 is disjunction and modGate 1 is the constant false, the union over all q : ℕ gives the same class (ACC0_eq_iUnion_AC0Mod).

Repeating each input wire of a MOD_q gate k ≥ 1 times multiplies the Hamming weight by k, and (w * k) % (q * k) = (w % q) * k, so a single MOD_{q * k} gate simulates a MOD_q gate (AC0Mod_subset_AC0Mod_mul_right, AC0Mod_subset_AC0Mod_of_dvd). Two circuits with moduli q₁ and q₂ therefore embed into the common modulus q₁ * q₂, making ACC0 closed under complement, intersection, and union (ACC0.compl, ACC0.inf, ACC0.sup). By Håstad's and Razborov–Smolensky's lower bounds for parity, AC0 ⊂ AC0Mod 2 ⊆ ACC0 (AC0_ssubset_AC0Mod_two, AC0_ssubset_ACC0) and AC0Mod p ⊂ ACC0 for every odd prime p (AC0Mod_ssubset_ACC0).

Main definitions

• Cslib.Circuits.Boolean.ACC0: the class ACC⁰ = ⋃ q ≥ 2, AC0Mod q.
• Cslib.Circuits.Boolean.modZeroCircuit, Cslib.Circuits.Boolean.modOneCircuit, Cslib.Circuits.Boolean.modMulCircuit: gate simulations for q = 0, q = 1, and q ∣ q * k.

Main results

• Cslib.Circuits.Boolean.AC0Mod_zero, Cslib.Circuits.Boolean.AC0Mod_one: AC⁰[0] = AC⁰[1] = AC⁰.
• Cslib.Circuits.Boolean.AC0Mod_subset_AC0Mod_of_dvd: AC⁰[q] ⊆ AC⁰[q'] when q ∣ q' and 0 < q'.
• Cslib.Circuits.Boolean.ACC0_eq_iUnion_AC0Mod: ACC⁰ = ⋃ q, AC⁰[q].
• Cslib.Circuits.Boolean.ACC0.compl, Cslib.Circuits.Boolean.ACC0.inf, Cslib.Circuits.Boolean.ACC0.sup: Boolean closure of ACC⁰.
• Cslib.Circuits.Boolean.ACC0_subset_TC0: ACC⁰ ⊆ TC⁰.
• Cslib.Circuits.Boolean.AC0_ssubset_ACC0, Cslib.Circuits.Boolean.AC0Mod_ssubset_ACC0: strictness of AC⁰ ⊂ ACC⁰ and AC⁰[p] ⊂ ACC⁰ for odd prime p.

References

• D. A. M. Barrington, Bounded-width polynomial-size branching programs recognize exactly those languages in NC¹
• H. Vollmer, Introduction to Circuit Complexity
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

Degenerate moduli q = 0, 1 and divisibility monotonicity for AC0Mod

theorem Cslib.Circuits.Boolean.modGate_zero (m : ℕ) (x : Fin m → Bool) : modGate 0 m x = Unbounded.interpretation (Unbounded.Op.or m) x

For q = 0, modGate 0 m tests whether the Hamming weight is nonzero, which is the unbounded disjunction .or m.

@[simp]

theorem Cslib.Circuits.Boolean.modGate_one (m : ℕ) (x : Fin m → Bool) : modGate 1 m x = false

For q = 1, modGate 1 m is the constant false.

theorem Cslib.Circuits.Boolean.modGate_two_eq_parity (m : ℕ) : modGate 2 m = parity m

For q = 2, modGate 2 m is the m-bit parity function parity m.

def Cslib.Circuits.Boolean.modZeroCircuit (op : Unbounded.ExtOp) : Circuit Unbounded.signature (Unbounded.extSignature.Arity op) 1

A circuit over the AC⁰ basis simulating an operation of AC⁰[0].

theorem Cslib.Circuits.Boolean.computes_modZeroCircuit (op : Unbounded.ExtOp) : (modZeroCircuit op).Computes Unbounded.interpretation (single (Unbounded.extInterpretation (modGate 0) op))

@[simp]

theorem Cslib.Circuits.Boolean.AC0Mod_zero : AC0Mod 0 = AC0

AC⁰[0] = AC⁰: modulo 0, a MOD_0 gate is an unbounded OR gate.

def Cslib.Circuits.Boolean.modOneCircuit (op : Unbounded.ExtOp) : Circuit Unbounded.signature (Unbounded.extSignature.Arity op) 1

A circuit over the AC⁰ basis simulating an operation of AC⁰[1].

theorem Cslib.Circuits.Boolean.computes_modOneCircuit (op : Unbounded.ExtOp) : (modOneCircuit op).Computes Unbounded.interpretation (single (Unbounded.extInterpretation (modGate 1) op))

@[simp]

theorem Cslib.Circuits.Boolean.AC0Mod_one : AC0Mod 1 = AC0

AC⁰[1] = AC⁰: modulo 1, a MOD_1 gate is the constant false.

theorem Cslib.Circuits.Boolean.weight_comp_finProdFinEquiv_fst {m k : ℕ} (x : Fin m → Bool) : (BitString.weight fun (j : Fin (m * k)) => x (finProdFinEquiv.symm j).1) = BitString.weight x * k

Repeating each of the m coordinates of x k times via finProdFinEquiv multiplies the Hamming weight by k.

theorem Cslib.Circuits.Boolean.modGate_mul_right (q m : ℕ) {k : ℕ} (hk : 0 < k) (x : Fin m → Bool) : (modGate (q * k) (m * k) fun (j : Fin (m * k)) => x (finProdFinEquiv.symm j).1) = modGate q m x

A MOD_q gate on m inputs is computed by a single MOD_{q * k} gate on m * k inputs when 0 < k, by repeating each input wire k times.

def Cslib.Circuits.Boolean.modMulCircuit (k : ℕ) (op : Unbounded.ExtOp) : Circuit Unbounded.extSignature (Unbounded.extSignature.Arity op) 1

A circuit over the AC⁰[q * k] basis simulating a single operation of AC⁰[q].

theorem Cslib.Circuits.Boolean.computes_modMulCircuit (q : ℕ) {k : ℕ} (hk : 0 < k) (op : Unbounded.ExtOp) : (modMulCircuit k op).Computes (Unbounded.extInterpretation (modGate (q * k))) (single (Unbounded.extInterpretation (modGate q) op))

theorem Cslib.Circuits.Boolean.AC0Mod_subset_AC0Mod_mul_right (q : ℕ) {k : ℕ} (hk : 0 < k) : AC0Mod q ⊆ AC0Mod (q * k)

AC⁰[q] ⊆ AC⁰[q * k] for every k > 0: a MOD_{q * k} gate simulates a MOD_q gate by repeating each wire k times.

theorem Cslib.Circuits.Boolean.AC0Mod_subset_AC0Mod_mul_left {k : ℕ} (hk : 0 < k) (q : ℕ) : AC0Mod q ⊆ AC0Mod (k * q)

AC⁰[q] ⊆ AC⁰[k * q] for every k > 0.

theorem Cslib.Circuits.Boolean.AC0Mod_subset_AC0Mod_of_dvd {q q' : ℕ} (hq' : 0 < q') (h : q ∣ q') : AC0Mod q ⊆ AC0Mod q'

Divisibility monotonicity: if q ∣ q' and 0 < q', then AC⁰[q] ⊆ AC⁰[q'].

Definition of ACC⁰ and closure properties

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

ACC⁰: the class of languages over Bool decided at every input length by constant-depth, polynomial-size circuits over negation, unbounded fan-in conjunction and disjunction, and unbounded fan-in MOD_q gates for some fixed modulus q ≥ 2 [Bar89], Vollmer, Chapter 4.

theorem Cslib.Circuits.Boolean.mem_ACC0_iff {L : Language Bool} : L ∈ ACC0 ↔ ∃ q ≥ 2, L ∈ AC0Mod q

Membership in ACC⁰: a language belongs to ACC0 iff it belongs to AC0Mod q for some modulus q ≥ 2.

theorem Cslib.Circuits.Boolean.AC0_subset_ACC0 : AC0 ⊆ ACC0

AC⁰ ⊆ ACC⁰: every AC⁰ language belongs to AC⁰[2] ⊆ ACC⁰.

theorem Cslib.Circuits.Boolean.AC0Mod_subset_ACC0 (q : ℕ) : AC0Mod q ⊆ ACC0

AC⁰[q] ⊆ ACC⁰ for every modulus q : ℕ (including q = 0, 1).

theorem Cslib.Circuits.Boolean.ACC0_eq_iUnion_AC0Mod : ACC0 = ⋃ (q : ℕ), AC0Mod q

ACC⁰ is the union of AC⁰[q] over all q : ℕ.

theorem Cslib.Circuits.Boolean.mem_ACC0_iff_exists_AC0Mod {L : Language Bool} : L ∈ ACC0 ↔ ∃ (q : ℕ), L ∈ AC0Mod q

Membership in ACC⁰ is equivalent to membership in AC⁰[q] for some q : ℕ.

theorem Cslib.Circuits.Boolean.modGate_mem_AC0Mod (q : ℕ) : Language.ofSlices (modGate q) ∈ AC0Mod q

The modular counting language Language.ofSlices (modGate q) is in AC⁰[q].

theorem Cslib.Circuits.Boolean.modGate_mem_ACC0 (q : ℕ) : Language.ofSlices (modGate q) ∈ ACC0

The modular counting language Language.ofSlices (modGate q) is in ACC⁰.

theorem Cslib.Circuits.Boolean.parity_mem_AC0Mod_two : Language.ofSlices parity ∈ AC0Mod 2

Parity is in AC⁰[2].

theorem Cslib.Circuits.Boolean.parity_mem_ACC0 : Language.ofSlices parity ∈ ACC0

Parity is in ACC⁰.

theorem Cslib.Circuits.Boolean.AC0_ssubset_AC0Mod_two : AC0 ⊂ AC0Mod 2

AC⁰ is strictly contained in AC⁰[2].

theorem Cslib.Circuits.Boolean.AC0_ssubset_ACC0 : AC0 ⊂ ACC0

AC⁰ is strictly contained in ACC⁰.

theorem Cslib.Circuits.Boolean.AC0Mod_ssubset_ACC0 {p : ℕ} [Fact (Nat.Prime p)] (hp2 : p ≠ 2) : AC0Mod p ⊂ ACC0

AC⁰[p] is strictly contained in ACC⁰ for every odd prime p, witnessed by parity [Raz87], [Smo87].

theorem Cslib.Circuits.Boolean.AC0Mod.bot_mem (q : ℕ) : ⊥ ∈ AC0Mod q

The empty language is in AC⁰[q].

theorem Cslib.Circuits.Boolean.AC0Mod.top_mem (q : ℕ) : ⊤ ∈ AC0Mod q

The full language is in AC⁰[q].

theorem Cslib.Circuits.Boolean.AC0Mod.compl {q : ℕ} {L : Language Bool} (hL : L ∈ AC0Mod q) : Lᶜ ∈ AC0Mod q

AC⁰[q] is closed under complement.

theorem Cslib.Circuits.Boolean.AC0Mod.inf {q : ℕ} {L M : Language Bool} (hL : L ∈ AC0Mod q) (hM : M ∈ AC0Mod q) : L ⊓ M ∈ AC0Mod q

AC⁰[q] is closed under intersection.

theorem Cslib.Circuits.Boolean.AC0Mod.sup {q : ℕ} {L M : Language Bool} (hL : L ∈ AC0Mod q) (hM : M ∈ AC0Mod q) : L ⊔ M ∈ AC0Mod q

AC⁰[q] is closed under union.

theorem Cslib.Circuits.Boolean.ACC0.bot_mem : ⊥ ∈ ACC0

The empty language is in ACC⁰.

theorem Cslib.Circuits.Boolean.ACC0.top_mem : ⊤ ∈ ACC0

The full language is in ACC⁰.

theorem Cslib.Circuits.Boolean.ACC0.compl {L : Language Bool} (hL : L ∈ ACC0) : Lᶜ ∈ ACC0

ACC⁰ is closed under complement.

theorem Cslib.Circuits.Boolean.ACC0.inf {L M : Language Bool} (hL : L ∈ ACC0) (hM : M ∈ ACC0) : L ⊓ M ∈ ACC0

ACC⁰ is closed under intersection: circuits with moduli q₁ and q₂ embed into AC⁰[q₁ * q₂].

theorem Cslib.Circuits.Boolean.ACC0.sup {L M : Language Bool} (hL : L ∈ ACC0) (hM : M ∈ ACC0) : L ⊔ M ∈ ACC0

ACC⁰ is closed under union: circuits with moduli q₁ and q₂ embed into AC⁰[q₁ * q₂].

theorem Cslib.Circuits.Boolean.ACC0_subset_TC0 : ACC0 ⊆ TC0

ACC⁰ ⊆ TC⁰ Vollmer, Chapter 4: every AC⁰[q] is contained in TC⁰.