Parity reduces 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 parity is the disjunction of these for odd k (parityCircuitOfMajority) [CSV84]. The circuit for parity has depth 4 more and size polynomially larger than the circuit for majority, so if majority has polynomial-size constant-depth circuits then so does parity (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.parityCircuitOfMajority: parity from a circuit for majority.

Main results

• Cslib.Circuits.Boolean.ConstDepth.parity_mem_of_majority_mem: over a basis containing the unbounded fan-in basis, parity has 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.parityCircuitOfMajority {n : ℕ} {σ : Signature} (φ : Unbounded.signature.Hom σ) (M : Circuit σ (n + (n + 2)) 1) : Circuit σ n 1

Parity from majority: the disjunction, over odd k ≤ n, 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_parityCircuitOfMajority_le {n : ℕ} {σ : Signature} {φ : Unbounded.signature.Hom σ} {M : Circuit σ (n + (n + 2)) 1} : (parityCircuitOfMajority φ M).size ≤ 1 + (n + 1) * (2 * (2 + M.size) + 2)

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

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

Parity 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)

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_parityCircuitOfMajority {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))))) : (parityCircuitOfMajority φ M).Computes I (single (parity n))

The parity circuit computes parity.

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