MOD_q gates from majority gates: ACⁱ[q] ⊆ TCⁱ

Over a basis containing the unbounded fan-in basis, the MOD_q function on n bits is the disjunction, over the k ≤ n not divisible by q, of "exactly k bits are true", each of which is two thresholds, so two majority gates on padded inputs (modCircuitOfMajority) Chandra, Stockmeyer and Vishkin. With a single majority gate this is a circuit of 8 n + 9 gates and depth five.

A MOD_q gate depends on how often it reads each wire, but only modulo q (for q = 0, only on whether it reads it at all): after aggregating multiplicities (Unbounded.multCircuit), a gate reading N distinct wires is a MOD_q function of at most max q 1 · N bits, wired from its arguments (Unbounded.modMultCircuit). Replacing every gate of a polynomial-size circuit with MOD_q gates, of depth d, gives a polynomial-size circuit with majority gates of depth at most 5 d: ACⁱ[q] ⊆ TCⁱ (ACMod_subset_TC) Vollmer, Chapter 4, in particular AC⁰[q] ⊆ TC⁰ (AC0Mod_subset_TC0).

Main definitions

• Cslib.Circuits.Boolean.modCircuitOfMajority: MOD_q from a circuit for majority.
• Cslib.Circuits.Boolean.Unbounded.modMultCircuit: a circuit with majority gates for every operation of the basis with MOD_q gates and multiplicities.

Main results

• Cslib.Circuits.Boolean.computes_modCircuitOfMajority: the circuit computes MOD_q.
• Cslib.Circuits.Boolean.Unbounded.exists_majority_simulation_modGate: a circuit with MOD_q gates of n inputs, s gates and depth d has an equivalent circuit with majority gates of at most s (9 + 8 max q 1 · (n + s)) gates and depth at most 5 d.
• Cslib.Circuits.Boolean.ACMod_subset_TC: ACⁱ[q] ⊆ TCⁱ.
• Cslib.Circuits.Boolean.AC0Mod_subset_TC0: AC⁰[q] ⊆ TC⁰.

References

• [A. K. Chandra, L. Stockmeyer, U. Vishkin, Constant depth reducibility] [CSV84]
• H. Vollmer, Introduction to Circuit Complexity

def Cslib.Circuits.Boolean.modCircuitOfMajority {n : ℕ} {σ : Signature} (φ : Unbounded.signature.Hom σ) (q : ℕ) (M : Circuit σ (n + (n + 2)) 1) : Circuit σ n 1

MOD_q from majority: the disjunction, over k ≤ n not divisible by q, of "exactly k bits are true".

theorem Cslib.Circuits.Boolean.size_modCircuitOfMajority_le {n : ℕ} {σ : Signature} {φ : Unbounded.signature.Hom σ} {M : Circuit σ (n + (n + 2)) 1} (q : ℕ) : (modCircuitOfMajority φ q M).size ≤ 1 + (n + 1) * (2 * (2 + M.size) + 2)

MOD_q costs n + 1 circuits for "exactly k" and one disjunction.

theorem Cslib.Circuits.Boolean.depth_modCircuitOfMajority_le {n : ℕ} {σ : Signature} {φ : Unbounded.signature.Hom σ} {M : Circuit σ (n + (n + 2)) 1} (q : ℕ) : (modCircuitOfMajority φ q M).depth ≤ M.depth + 4

MOD_q is four deeper than the majority circuit.

theorem Cslib.Circuits.Boolean.computes_modCircuitOfMajority {n : ℕ} {σ : Signature} {φ : Unbounded.signature.Hom σ} {I : Interpretation σ Bool} {M : Circuit σ (n + (n + 2)) 1} [φ.Preserves Unbounded.interpretation I] (hM : M.Computes I (single (majority (n + (n + 2))))) (q : ℕ) : (modCircuitOfMajority φ q M).Computes I (single (modGate q n))

The circuit computes MOD_q.

def Cslib.Circuits.Boolean.Unbounded.modCount (q : ℕ) : ℕ → (c : ℕ) → Bool

The count of true arguments that a MOD_q gate sees: whether it is divisible by q.

theorem Cslib.Circuits.Boolean.Unbounded.modGate_eq_modCount (q m : ℕ) (x : Fin m → Bool) : modGate q m x = modCount q m (BitString.weight x)

The MOD_q gate computes modCount q of the number of its true arguments.

def Cslib.Circuits.Boolean.Unbounded.modMult (q k : ℕ) : ℕ

The multiplicity of a wire that matters to a MOD_q gate: modulo q, and for q = 0 whether it is read at all.

theorem Cslib.Circuits.Boolean.Unbounded.modMult_le (q k : ℕ) : modMult q k ≤ max q 1

theorem Cslib.Circuits.Boolean.Unbounded.multWeight_modMult_mod_ne_zero_iff {N : ℕ} (q : ℕ) (mult : Fin N → ℕ) (x : Fin N → Bool) : multWeight (fun (i : Fin N) => modMult q (mult i)) x % q ≠ 0 ↔ multWeight mult x % q ≠ 0

Reducing multiplicities with modMult keeps divisibility of the weighted count by q.

def Cslib.Circuits.Boolean.Unbounded.expandIndex {N : ℕ} (r : Fin N → ℕ) (j : Fin (∑ i : Fin N, r i)) : Fin N

The argument of a symmetric gate read by each of its ∑ i, r i copies.

theorem Cslib.Circuits.Boolean.Unbounded.weight_comp_expandIndex {N : ℕ} (r : Fin N → ℕ) (x : Fin N → Bool) : BitString.weight (x ∘ expandIndex r) = multWeight r x

Repeating the ith argument r i times counts it with multiplicity r i.

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

A circuit with majority gates for each operation of the basis with MOD_q gates and multiplicities: an operation of the unbounded fan-in basis is one gate, and a MOD_q gate is modCircuitOfMajority on its arguments repeated with their multiplicities reduced by modMult.

theorem Cslib.Circuits.Boolean.Unbounded.computes_modMultCircuit (q : ℕ) (op : MultOp) : (modMultCircuit q op).Computes (extInterpretation majority) (single (multInterpretation (modCount q) op))

The circuit of an operation computes it.

theorem Cslib.Circuits.Boolean.Unbounded.size_modMultCircuit_le (q : ℕ) (op : MultOp) : (modMultCircuit q op).size ≤ 9 + 8 * max q 1 * multSignature.Arity op

The circuit of an operation reading N wires has at most 9 + 8 max q 1 · N gates.

theorem Cslib.Circuits.Boolean.Unbounded.depth_modMultCircuit_le (q : ℕ) (op : MultOp) : (modMultCircuit q op).depth ≤ 5

The circuit of an operation has depth at most five.

theorem Cslib.Circuits.Boolean.Unbounded.exists_majority_simulation_modGate {n m : ℕ} (q : ℕ) (C : Circuit extSignature n m) : ∃ (D : Circuit extSignature n m), D.eval (extInterpretation majority) = C.eval (extInterpretation (modGate q)) ∧ D.size ≤ C.size * (9 + 8 * max q 1 * (n + C.size)) ∧ D.depth ≤ 5 * C.depth

Majority gates simulate MOD_q gates Vollmer, Chapter 4: a circuit with MOD_q gates of n inputs, s gates and depth d has an equivalent circuit with majority gates of at most s (9 + 8 max q 1 · (n + s)) gates and depth at most 5 d. Its gates are first made to read their distinct wires with multiplicities (multCircuit), and then replaced by modMultCircuit.

theorem Cslib.Circuits.Boolean.ACMod_subset_TC (q i : ℕ) : ACMod q i ⊆ TC i

ACⁱ[q] ⊆ TCⁱ Vollmer, Chapter 4: polynomial-size circuits with MOD_q gates of depth O((log n) ^ i) are simulated by polynomial-size circuits with majority gates of depth O((log n) ^ i).

theorem Cslib.Circuits.Boolean.AC0Mod_subset_TC0 (q : ℕ) : AC0Mod q ⊆ TC0

AC⁰[q] ⊆ TC⁰.