Shallow circuits for symmetric functions

The theorem of Lecomte and Ramakrishnan Lecomte and Ramakrishnan, Theorems 1 and 2: for every depth d ≥ 2 there is a constant C such that every symmetric Boolean function of n bits (one depending only on the number of true bits, BooleanFunction.IsSymmetric), majority among them, has alternating formulas of depth d with at most 2 ^ (C n ^ (1 / (d - 1))) AND and OR gates (AltFormula.exists_of_isSymmetric), so circuits over the unbounded fan-in basis of AND/OR depth d with at most n more gates (Unbounded.exists_circuit_of_isSymmetric). For depth three this is 2 ^ (C √n). The exponent is optimal for majority, by Korten's top-down bounds for alternating formulas (AltFormula.two_rpow_lt_size_of_eval_eq_majority) and for circuits of AND/OR depth d (Unbounded.two_rpow_lt_add_size_of_computes_majority).

The proof is by induction on the depth: at depth d + 2, symmetric functions of at most k ^ (d + 1) bits have alternating formulas with 2 ^ (C_d k) gates (exists_symmetric_altFormula), and depth two is a normal form. For the step to depth d + 3 and n ≤ k ^ (d + 2) bits, a symmetric function is an OR over the accepted weights t of the exact-weight tests #x = t. Choose d + 2 pairwise coprime moduli mᵢ between k and C k with product above n (exists_moduli), and split the inputs into the mᵢ residue classes modulo each mᵢ. The weight is t exactly when, modulo each mᵢ, the class weights sum to t; that holds exactly when some shifts s, summing to ∑ a - t, make the shifted class weights pairwise distinct (ShiftTest), and a random shift works with probability at least 3 ^ (-mᵢ), so 3 ^ ∑ mᵢ (n + 1) shifts cover every input of weight t (exists_simultaneous_shiftTest_cover). Each shifted comparison of two class weights is a symmetric function of their bits after negating one class, on 2 (n / mᵢ + 1) ≤ (4 k) ^ (d + 1) bits, so it has 2 ^ (C_d · 4 k) gates at depth d + 2 by induction (exists_pairComparison), and the comparisons of one test merge into one gate layer.

Main results

• Cslib.Circuits.Boolean.AltFormula.exists_of_isSymmetric_nat, Cslib.Circuits.Boolean.AltFormula.exists_of_isSymmetric: the theorem of Lecomte and Ramakrishnan, for alternating formulas.
• Cslib.Circuits.Boolean.Unbounded.exists_circuit_of_isSymmetric: the same for circuits over the unbounded fan-in basis.
• Cslib.Circuits.Boolean.AltFormula.exists_of_isSymmetric_depth_three, Cslib.Circuits.Boolean.AltFormula.exists_majority: depth three, and majority.

References

• V. Lecomte, P. Ramakrishnan, Optimal Shallow Circuits for Majority

theorem Cslib.Circuits.Boolean.ShallowSymmetric.exists_symmetric_altFormula (d : ℕ) : ∃ (C : ℕ), ∀ (n k : ℕ), 1 ≤ k → n ≤ k ^ (d + 1) → ∀ (a : ℕ → Bool) (op : AltOp), ∃ (f : AltFormula n (d + 2)), f.size ≤ 2 ^ (C * k) ∧ ∀ (x : BitString n), AltFormula.eval op f x = a (BitString.weight x)

The depth induction: at depth d + 2, every symmetric function of at most k ^ (d + 1) bits has alternating formulas with either root operation of size at most 2 ^ (C k).

theorem Cslib.Circuits.Boolean.AltFormula.exists_of_isSymmetric_nat {d : ℕ} (hd : 2 ≤ d) : ∃ (C : ℕ), ∀ (n : ℕ) (f : BitString n → Bool), BooleanFunction.IsSymmetric f → ∀ (op : AltOp), ∃ (g : AltFormula n d), g.size ≤ 2 ^ (C * ((d - 1).nthRoot n + 1)) ∧ ∀ (x : BitString n), eval op g x = f x

The theorem of Lecomte and Ramakrishnan Lecomte and Ramakrishnan, Theorem 1, with an integer root: for every depth d ≥ 2 there is a constant C such that every symmetric function of n bits has alternating formulas of depth d, with either root operation, with at most 2 ^ (C (⌊n ^ (1 / (d - 1))⌋ + 1)) AND and OR gates.

theorem Cslib.Circuits.Boolean.AltFormula.exists_of_isSymmetric {d : ℕ} (hd : 2 ≤ d) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), 1 ≤ n → ∀ (f : BitString n → Bool), BooleanFunction.IsSymmetric f → ∀ (op : AltOp), ∃ (g : AltFormula n d), ↑g.size ≤ 2 ^ (C * ↑n ^ (↑(d - 1))⁻¹) ∧ ∀ (x : BitString n), eval op g x = f x

The theorem of Lecomte and Ramakrishnan Lecomte and Ramakrishnan, Theorem 1: for every depth d ≥ 2 there is a constant C such that every symmetric function of n ≥ 1 bits has alternating formulas of depth d, with either root operation, with at most 2 ^ (C n ^ (1 / (d - 1))) AND and OR gates.

theorem Cslib.Circuits.Boolean.AltFormula.exists_of_isSymmetric_depth_three : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), 1 ≤ n → ∀ (f : BitString n → Bool), BooleanFunction.IsSymmetric f → ∀ (op : AltOp), ∃ (g : AltFormula n 3), ↑g.size ≤ 2 ^ (C * √↑n) ∧ ∀ (x : BitString n), eval op g x = f x

Depth three Lecomte and Ramakrishnan, Theorem 2: symmetric functions of n ≥ 1 bits have alternating formulas of depth three with at most 2 ^ (C √n) gates.

theorem Cslib.Circuits.Boolean.AltFormula.exists_majority {d : ℕ} (hd : 2 ≤ d) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), 1 ≤ n → ∀ (op : AltOp), ∃ (g : AltFormula n d), ↑g.size ≤ 2 ^ (C * ↑n ^ (↑(d - 1))⁻¹) ∧ ∀ (x : BitString n), eval op g x = majority n x

Majority of n ≥ 1 bits has alternating formulas of depth d ≥ 2 with at most 2 ^ (C n ^ (1 / (d - 1))) gates.

theorem Cslib.Circuits.Boolean.Unbounded.exists_circuit_of_isSymmetric {d : ℕ} (hd : 2 ≤ d) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), 1 ≤ n → ∀ (f : BitString n → Bool), BooleanFunction.IsSymmetric f → ∃ (c : Circuit signature n 1), c.Computes interpretation (single f) ∧ Circuit.depthWith andOrCost c ≤ d ∧ c.depth ≤ d + 1 ∧ ↑c.size ≤ 2 ^ (C * ↑n ^ (↑(d - 1))⁻¹) + ↑n

The theorem of Lecomte and Ramakrishnan, for circuits [LR26]: for every d ≥ 2 there is a constant C such that every symmetric function of n ≥ 1 bits has circuits over the unbounded fan-in basis of AND/OR depth at most d, and of depth at most d + 1 counting negations, with at most 2 ^ (C n ^ (1 / (d - 1))) + n gates.