Simulation of MOD_q circuits in AC¹, NC², and P/poly

Replacing the majority gate in modCircuitOfMajority by the logarithmic-depth De Morgan majority circuit (majorityDeMorganCircuit) simulates each operation of the MOD_q multiplicity basis over Unbounded.signature in polynomial size and logarithmic depth (Unbounded.modMultUnboundedCircuit, Unbounded.exists_unbounded_simulation_modGate) and over the De Morgan fan-in-two basis in polynomial size (Unbounded.exists_deMorgan_simulation_modGate).

This yields the hierarchy inclusions ACMod q i ⊆ AC (i + 1) (ACMod_subset_AC_succ), ACC0 ⊆ AC 1 ⊆ NC 2 ⊆ PPoly (ACC0_subset_AC_one, ACC0_subset_NC_two, ACC0_subset_PPoly), and the polynomial-size simulation SIZEMod_subset_SIZE of unbounded-depth MOD_q circuits by De Morgan circuits.

Main definitions

• Cslib.Circuits.Boolean.Unbounded.modMultUnboundedCircuit: logarithmic-depth unbounded-fan-in simulation of a single MOD_q multiplicity operation.
• Cslib.Circuits.Boolean.SIZEMod: languages decided by MOD_q circuits of size at most s n.

Main results

• Cslib.Circuits.Boolean.Unbounded.exists_unbounded_simulation_modGate, Cslib.Circuits.Boolean.Unbounded.exists_deMorgan_simulation_modGate: gate-by-gate simulations of MOD_q circuits.
• Cslib.Circuits.Boolean.ACMod_subset_AC_succ, Cslib.Circuits.Boolean.ACC0_subset_AC_one, Cslib.Circuits.Boolean.ACC0_subset_NC_two, Cslib.Circuits.Boolean.ACC0_subset_PPoly.
• Cslib.Circuits.Boolean.SIZEMod_subset_SIZE: simulating SIZEMod q in De Morgan SIZE.

References

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

def Cslib.Circuits.Boolean.Unbounded.modMultUnboundedCircuit (q : ℕ) (op : MultOp) : Circuit signature (multSignature.Arity op) 1

A circuit over the unbounded fan-in basis simulating each operation of the MOD_q multiplicity basis, using majorityDeMorganCircuit mapped into Unbounded.signature inside modCircuitOfMajority.

theorem Cslib.Circuits.Boolean.Unbounded.computes_modMultUnboundedCircuit (q : ℕ) (op : MultOp) : (modMultUnboundedCircuit q op).Computes interpretation (single (multInterpretation (modCount q) op))

modMultUnboundedCircuit q op computes op under Unbounded.interpretation.

theorem Cslib.Circuits.Boolean.Unbounded.size_modMultUnboundedCircuit_le (q : ℕ) (op : MultOp) : (modMultUnboundedCircuit q op).size ≤ 2100 * (max q 1 * multSignature.Arity op + 1) ^ 3

Polynomial size bound for modMultUnboundedCircuit q op.

theorem Cslib.Circuits.Boolean.Unbounded.depth_modMultUnboundedCircuit_le (q : ℕ) (op : MultOp) : (modMultUnboundedCircuit q op).depth ≤ 6 + 23 * Nat.clog 2 (2 * max q 1 * multSignature.Arity op + 3)

Logarithmic depth bound for modMultUnboundedCircuit q op.

theorem Cslib.Circuits.Boolean.Unbounded.exists_unbounded_simulation_modGate {n m : ℕ} (q : ℕ) (C : Circuit extSignature n m) : ∃ (D : Circuit signature n m), D.eval interpretation = C.eval (extInterpretation (modGate q)) ∧ D.size ≤ C.size * (2100 * (max q 1 * (n + C.size) + 1) ^ 3) ∧ D.depth ≤ (6 + 23 * Nat.clog 2 (2 * max q 1 * (n + C.size) + 3)) * C.depth

Unbounded fan-in circuits simulate MOD_q gates in logarithmic depth: a circuit with MOD_q gates of n inputs, s gates and depth d has an equivalent circuit over the unbounded fan-in basis of at most 2100 * s * (max q 1 * (n + s) + 1) ^ 3 gates and depth at most (6 + 23 * ⌈log₂ (2 * max q 1 * (n + s) + 3)⌉) * d.

theorem Cslib.Circuits.Boolean.Unbounded.exists_deMorgan_simulation_modGate {n m : ℕ} (q : ℕ) (C : Circuit extSignature n m) : ∃ (D : Circuit Boolean.signature n m), D.eval Boolean.interpretation = C.eval (extInterpretation (modGate q)) ∧ D.size ≤ (2100 * max q 1 ^ 3) ^ 2 * (n + C.size + 1) ^ 8

De Morgan circuits simulate MOD_q circuits in polynomial size: every circuit over the AC⁰[q] basis of n inputs and s gates has an equivalent fan-in-two De Morgan circuit of size at most (2100 * (max q 1) ^ 3) ^ 2 * (n + s + 1) ^ 8.

theorem Cslib.Circuits.Boolean.ACMod_subset_AC_succ (q i : ℕ) : ACMod q i ⊆ AC (i + 1)

ACⁱ[q] ⊆ ACⁱ⁺¹: polynomial-size circuits with MOD_q gates of depth O((log n) ^ i) are simulated by polynomial-size circuits over the unbounded fan-in basis of depth O((log n) ^ (i + 1)).

theorem Cslib.Circuits.Boolean.AC0Mod_subset_AC_one (q : ℕ) : AC0Mod q ⊆ AC 1

AC⁰[q] ⊆ AC¹.

theorem Cslib.Circuits.Boolean.ACC0_subset_AC_one : ACC0 ⊆ AC 1

ACC⁰ ⊆ AC¹.

theorem Cslib.Circuits.Boolean.AC0Mod_subset_NC_two (q : ℕ) : AC0Mod q ⊆ NC 2

AC⁰[q] ⊆ NC².

theorem Cslib.Circuits.Boolean.ACC0_subset_NC_two : ACC0 ⊆ NC 2

ACC⁰ ⊆ NC².

theorem Cslib.Circuits.Boolean.AC0Mod_subset_PPoly (q : ℕ) : AC0Mod q ⊆ PPoly

AC⁰[q] ⊆ P/poly for every modulus q.

theorem Cslib.Circuits.Boolean.ACC0_subset_PPoly : ACC0 ⊆ PPoly

ACC⁰ ⊆ P/poly.

theorem Cslib.Circuits.Boolean.exists_notMem_ACC0 : ∃ (L : Language Bool), L ∉ ACC0

Some language over Bool is not in ACC⁰ (by Shannon's counting argument and ACC0 ⊆ PPoly).

Unbounded-depth MOD_q circuit size classes (SIZEMod)

def Cslib.Circuits.Boolean.SIZEMod (q : ℕ) (s : ℕ → ℕ) : Set (Language Bool)

The class of languages over Bool decided at every input length n by circuits over the AC⁰[q] basis (Unbounded.extInterpretation (modGate q)) of size at most s n (of arbitrary depth).

theorem Cslib.Circuits.Boolean.SIZEMod_mono (q : ℕ) : Monotone (SIZEMod q)

SIZEMod q is monotone in the size bound.

theorem Cslib.Circuits.Boolean.SIZEMod_subset_SIZE (q c k : ℕ) : (SIZEMod q fun (n : ℕ) => c * (n + 1) ^ k) ⊆ SIZE fun (n : ℕ) => (2100 * max q 1 ^ 3) ^ 2 * (c + 1) ^ 8 * (n + 1) ^ (8 * (k + 1))

Simulating SIZEMod q in De Morgan SIZE: a circuit with MOD_q gates of size at most c * (n + 1) ^ k is simulated by a fan-in-two De Morgan circuit of size at most (2100 * (max q 1) ^ 3) ^ 2 * (c + 1) ^ 8 * (n + 1) ^ (8 * (k + 1)).