ACC⁰ and lower bounds against modular-counting circuits

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 development is split into two submodules, both re-exported here:

• Complexity.Computability.Circuit.Boolean.ACC0.Basic: the definition of ACC0, the degenerate moduli q = 0, 1, divisibility monotonicity AC0Mod q ⊆ AC0Mod q' for q ∣ q', Boolean closure, ACC0 ⊆ TC0, and the strict inclusions AC0 ⊂ ACC0 and AC0Mod p ⊂ ACC0 (p an odd prime) obtained from Håstad's and Razborov–Smolensky's lower bounds for parity.
• Complexity.Computability.Circuit.Boolean.ACC0.Simulation: logarithmic-depth simulation of MOD_q gates by unbounded fan-in circuits, giving ACMod q i ⊆ AC (i + 1) and ACC0 ⊆ AC 1 ⊆ NC 2 ⊆ PPoly, and the polynomial-size simulation of unbounded-depth MOD_q circuits (SIZEMod q) by fan-in-two De Morgan circuits (SIZEMod_subset_SIZE).

This module adds the resulting separations:

• P ⊄ AC⁰ and P ⊄ AC⁰[p]: parity lies in P (parity_mem_P), so it witnesses languages in P outside AC0 (exists_mem_P_notMem_AC0) [Has86] and outside AC0Mod p for every odd prime p (exists_mem_P_notMem_AC0Mod) [Raz87], [Smo87].
• Fixed-exponent MOD_q circuit lower bounds in Σ₂: for every modulus q (prime or composite) and every exponent k, combining SIZEMod_subset_SIZE with Kannan's theorem gives a language in Σ₂ with no MOD_q circuits of size O(n ^ k) of any depth (Kannan.language_notMem_SIZEMod, exists_mem_SigmaP_two_notMem_SIZEMod) [Kan82].

Main results

• Cslib.Circuits.Boolean.parity_mem_P: parity is in P.
• Cslib.Circuits.Boolean.exists_mem_P_notMem_AC0, Cslib.Circuits.Boolean.exists_mem_P_notMem_AC0Mod: P ⊄ AC⁰ and P ⊄ AC⁰[p] for odd primes p.
• Cslib.Circuits.Boolean.Kannan.language_notMem_SIZEMod, Cslib.Circuits.Boolean.exists_mem_SigmaP_two_notMem_SIZEMod: fixed-exponent MOD_q circuit lower bounds in Σ₂ for every modulus q.

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
• J. Håstad, Almost optimal lower bounds for small depth circuits
• A. A. Razborov, Lower bounds on the size of bounded depth circuits over a complete basis with logical addition
• R. Smolensky, Algebraic methods in the theory of lower bounds for Boolean circuit complexity
• R. Kannan, Circuit-size lower bounds and non-reducibility to sparse sets

theorem Cslib.Circuits.Boolean.foldl_bne_eq_parity (w : List Bool) : List.foldl bne false w = parity w.length fun (i : Fin w.length) => w[i]

Folding xor over a Boolean word computes parity of its slice.

theorem Cslib.Circuits.Boolean.parity_mem_P : Language.ofSlices parity ∈ Complexity.P Turing.MultiTapeTM.encBits

Parity is in P (Language.ofSlices parity ∈ P encBits).

theorem Cslib.Circuits.Boolean.exists_mem_P_notMem_AC0 : ∃ L ∈ Complexity.P Turing.MultiTapeTM.encBits, L ∉ AC0

Unconditional separation P ⊄ AC⁰: parity is in P and not in AC⁰ [Has86].

theorem Cslib.Circuits.Boolean.exists_mem_P_notMem_AC0Mod {p : ℕ} [Fact (Nat.Prime p)] (hp2 : p ≠ 2) : ∃ L ∈ Complexity.P Turing.MultiTapeTM.encBits, L ∉ AC0Mod p

Unconditional separation P ⊄ AC⁰[p] for every odd prime p: parity is in P and not in AC⁰[p] [Raz87], [Smo87].

theorem Cslib.Circuits.Boolean.Kannan.language_notMem_SIZEMod (q k c : ℕ) : Complexity.Kannan.language (8 * (k + 1)) ∉ SIZEMod q fun (n : ℕ) => c * (n + 1) ^ k

Kannan's language escapes SIZEMod q: for every q, k, c : ℕ, Kannan.language (8 * (k + 1)) has no circuits over the AC⁰[q] basis of size c * (n + 1) ^ k [Kan82].

theorem Cslib.Circuits.Boolean.exists_mem_SigmaP_two_notMem_SIZEMod (q k : ℕ) : ∃ L ∈ Complexity.SigmaP 2 Turing.MultiTapeTM.encBits, ∀ (c : ℕ), L ∉ SIZEMod q fun (n : ℕ) => c * (n + 1) ^ k

Unconditional fixed-exponent MOD_q circuit lower bound in Σ₂ (for every modulus q, prime or composite): for every q, k : ℕ, some language in Σ₂ has no circuits over the AC⁰[q] basis of size O(n ^ k) (even of unbounded depth), by combining SIZEMod_subset_SIZE with Kannan's theorem [Kan82].