Modular counting and parity reduce to majority in constant depth

Over a basis containing the unbounded fan-in basis (through a meaning-preserving map φ), padding the input with constants turns a circuit for majority on 2 n + 2 bits into every threshold function on n bits (thresholdCircuitOfMajority), two thresholds give "exactly k bits are true" (exactlyCircuitOfMajority), and the MOD_q function is the disjunction of these for k not divisible by q (modCircuitOfMajority) [CSV84]. The circuit for MOD_q has depth 4 more and size polynomially larger than the circuit for majority, so if majority has polynomial-size constant-depth circuits then so do MOD_q and parity (ConstDepth.modGate_mem_of_majority_mem, ConstDepth.parity_mem_of_majority_mem). Over the unbounded fan-in basis itself this contradicts Cslib.Circuits.Boolean.parity_notMem_AC0: majority is not in AC⁰ [FSS84].

Main definitions

• Cslib.Circuits.Boolean.padCircuit: pad an n-bit input with min a (n + 2) copies of true followed by n + 2 - a copies of false.
• Cslib.Circuits.Boolean.modCircuitOfMajority: MOD_q from a circuit for majority.

Main results

• Cslib.Circuits.Boolean.computes_modCircuitOfMajority: the circuit computes MOD_q.
• Cslib.Circuits.Boolean.ConstDepth.modGate_mem_of_majority_mem, Cslib.Circuits.Boolean.ConstDepth.parity_mem_of_majority_mem: over a basis containing the unbounded fan-in basis, MOD_q and parity have polynomial-size constant-depth circuits if majority does.
• Cslib.Circuits.Boolean.majority_notMem_AC0: majority is not in AC⁰.

References

• [A. K. Chandra, L. Stockmeyer, U. Vishkin, Constant depth reducibility] [CSV84]
• M. Furst, J. B. Saxe, M. Sipser, Parity, circuits, and the polynomial-time hierarchy

def Cslib.Circuits.Boolean.padCircuit {σ : Signature} (φ : Unbounded.signature.Hom σ) (n a : ℕ) : Circuit σ n (n + (n + 2))

The inputs followed by a copies of true and then copies of false, n + 2 constants in all, read from two constant gates.

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

The threshold function Th^n_k for k ≤ n + 1, from a circuit M for majority on n + (n + 2) bits.

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

Whether exactly k of the bits are true, from a circuit for majority.

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".

@[simp]

theorem Cslib.Circuits.Boolean.size_padCircuit {n : ℕ} {σ : Signature} {φ : Unbounded.signature.Hom σ} (a : ℕ) : (padCircuit φ n a).size = 2

Padding costs two gates, one for each constant.

theorem Cslib.Circuits.Boolean.depth_padCircuit_le {n : ℕ} {σ : Signature} {φ : Unbounded.signature.Hom σ} (a : ℕ) : (padCircuit φ n a).depth ≤ 1

Padding has depth at most one.

theorem Cslib.Circuits.Boolean.size_thresholdCircuitOfMajority {n : ℕ} {σ : Signature} {φ : Unbounded.signature.Hom σ} {M : Circuit σ (n + (n + 2)) 1} (k : ℕ) : (thresholdCircuitOfMajority φ M k).size = 2 + M.size

A threshold costs the padding and the majority circuit.

theorem Cslib.Circuits.Boolean.depth_thresholdCircuitOfMajority_le {n : ℕ} {σ : Signature} {φ : Unbounded.signature.Hom σ} {M : Circuit σ (n + (n + 2)) 1} (k : ℕ) : (thresholdCircuitOfMajority φ M k).depth ≤ M.depth + 1

A threshold is one deeper than the majority circuit.

theorem Cslib.Circuits.Boolean.size_exactlyCircuitOfMajority {n : ℕ} {σ : Signature} {φ : Unbounded.signature.Hom σ} {M : Circuit σ (n + (n + 2)) 1} (k : ℕ) : (exactlyCircuitOfMajority φ M k).size = 2 * (2 + M.size) + 2

"Exactly k" costs two thresholds and two gates.

theorem Cslib.Circuits.Boolean.depth_exactlyCircuitOfMajority_le {n : ℕ} {σ : Signature} {φ : Unbounded.signature.Hom σ} {M : Circuit σ (n + (n + 2)) 1} (k : ℕ) : (exactlyCircuitOfMajority φ M k).depth ≤ M.depth + 3

"Exactly k" is three deeper than the majority circuit.

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.eval_padCircuit {n : ℕ} {σ : Signature} {φ : Unbounded.signature.Hom σ} {I : Interpretation σ Bool} [φ.Preserves Unbounded.interpretation I] (a : ℕ) (x : BitString n) : (padCircuit φ n a).eval I x = Fin.append x fun (j : Fin (n + 2)) => decide (↑j < a)

Evaluating padCircuit φ n a appends min a (n + 2) copies of true followed by n + 2 - a copies of false to the input x.

theorem Cslib.Circuits.Boolean.eval_thresholdCircuitOfMajority {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))))) {k : ℕ} (hk : k ≤ n + 1) (x : BitString n) : (thresholdCircuitOfMajority φ M k).eval I x 0 = threshold n k x

The threshold circuit computes the threshold function.

theorem Cslib.Circuits.Boolean.eval_exactlyCircuitOfMajority {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))))) {k : ℕ} (hk : k ≤ n) (x : BitString n) : (exactlyCircuitOfMajority φ M k).eval I x 0 = decide (BitString.weight x = k)

The circuit for "exactly k" decides whether exactly k bits are true.

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.

theorem Cslib.Circuits.Boolean.ConstDepth.modGate_mem_of_majority_mem {σ : Signature} {I : Interpretation σ Bool} (φ : Unbounded.signature.Hom σ) [φ.Preserves Unbounded.interpretation I] (q : ℕ) (h : Language.ofSlices majority ∈ ConstDepth I) : Language.ofSlices (modGate q) ∈ ConstDepth I

MOD_q reduces to majority: over a basis containing the unbounded fan-in basis, modGate q has polynomial-size constant-depth circuits if majority does.

theorem Cslib.Circuits.Boolean.ConstDepth.parity_mem_of_majority_mem {σ : Signature} {I : Interpretation σ Bool} (φ : Unbounded.signature.Hom σ) [φ.Preserves Unbounded.interpretation I] (h : Language.ofSlices majority ∈ ConstDepth I) : Language.ofSlices parity ∈ ConstDepth I

Parity reduces to majority: over a basis containing the unbounded fan-in basis, parity has polynomial-size constant-depth circuits if majority does.

theorem Cslib.Circuits.Boolean.majority_notMem_AC0 : Language.ofSlices majority ∉ AC0

Majority is not in AC⁰.