AC⁰[q]

The basis of AC⁰ together with MOD_q gates of unbounded fan-in, which output true exactly when the number of their true inputs is not divisible by q (modGate), and the class AC⁰[q] of languages decided by such circuits of polynomial size and constant depth Arora and Barak, Section 14.2: the unbounded fan-in basis extended by MOD_q (Unbounded.extInterpretation (modGate q)).

Main definitions

• Cslib.Circuits.Boolean.modGate: the MOD_q gate.
• Cslib.Circuits.Boolean.AC0Mod: the class AC⁰[q].

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach

def Cslib.Circuits.Boolean.modGate (q m : ℕ) (x : Fin m → Bool) : Bool

The MOD_q gate: whether the number of true bits of x is not divisible by q.

def Cslib.Circuits.Boolean.AC0Mod (q : ℕ) : Set (Language Bool)

AC⁰[q]: the languages over Bool decided, at every input length, by circuits with MOD_q gates of polynomially bounded size and constant depth.

theorem Cslib.Circuits.Boolean.AC0_subset_AC0Mod (q : ℕ) : AC0 ⊆ AC0Mod q

AC⁰ ⊆ AC⁰[q]: every AC⁰ circuit is a circuit with MOD_q gates.