Top-down lower bounds for alternating formulas

An alternating formula gives a Karchmer–Wigderson protocol with one message per gate layer (AltFormula.kwProtocol): at a conjunction the player whose input makes it false names an argument false there, at a disjunction the player whose input makes it true names an argument true there, and at the bottom the named literal separates the inputs. Negations are free, so a formula of depth d with S gates gives a protocol with d messages from an alphabet of S + 1 + 2 n symbols (AltFormula.kwProtocol_solves). By Korten's bound for parity Korten, Theorem 3 and its extension to majority, alternating formulas of depth d for parity or majority have S + 2 n + 1 > 2 ^ (ε n ^ (1 / (d - 1))) for large n (AltFormula.two_rpow_lt_size_of_eval_eq_parity, AltFormula.two_rpow_lt_size_of_eval_eq_majority), so the theorem of Lecomte and Ramakrishnan (AltFormula.exists_majority) is optimal for majority up to the constant in the exponent.

Main definitions

• Cslib.Circuits.Boolean.AltFormula.kwProtocol: the Karchmer–Wigderson protocol of an alternating formula.

Main results

• Cslib.Circuits.Boolean.AltFormula.kwProtocol_solves: it solves the game of the formula.
• Cslib.Circuits.Boolean.AltFormula.two_rpow_lt_size_of_eval_eq_parity, Cslib.Circuits.Boolean.AltFormula.two_rpow_lt_size_of_eval_eq_majority: Korten's bounds for alternating formulas.

References

• O. Korten, Top-Down Lower Bounds for All Depths
• V. Lecomte, P. Ramakrishnan, Optimal Shallow Circuits for Majority

def Cslib.Circuits.Boolean.AltFormula.speaker : AltOp → Bool → Bool

The player who speaks at a gate with root op when Alice's input makes it s: the holder of the false input at a conjunction and of the true input at a disjunction (true is Bob).

def Cslib.Circuits.Boolean.AltFormula.witness : AltOp → Bool

The value a speaker's argument has at a gate with root op: false at a conjunction, true at a disjunction.

def Cslib.Circuits.Boolean.AltFormula.childIndex {n d : ℕ} (op : AltOp) (fs : List (AltFormula n d)) (b : Bool) (x : BitString n) : ℕ

The position of the first child of fs whose value with root op is b on x, or 0.

def Cslib.Circuits.Boolean.AltFormula.childLiteral {n : ℕ} (i₀ : Fin n) (ls : List (Logic.PL.Literal (Fin n))) (b : Bool) (x : BitString n) : Logic.PL.Literal (Fin n)

The first literal of the clause or term ls whose value is b on x, or (i₀, true).

def Cslib.Circuits.Boolean.AltFormula.kwProtocol {n : ℕ} (S : ℕ) (i₀ : Fin n) {d : ℕ} : AltOp → AltFormula n d → Bool → Communication.KWRoundProtocol (Fin n) (Fin (S + 1) ⊕ Logic.PL.Literal (Fin n)) d

The Karchmer–Wigderson protocol of an alternating formula with root op, when Alice's input makes it s, with messages a child position below S + 1 or a literal.

theorem Cslib.Circuits.Boolean.AltFormula.childIndex_spec {n d : ℕ} {op : AltOp} {fs : List (AltFormula n d)} {b : Bool} {x : BitString n} (h : ∃ (j : Fin fs.length), eval op (fs.get j) x = b) : ∃ (j : Fin fs.length), childIndex op fs b x = ↑j ∧ eval op (fs.get j) x = b

theorem Cslib.Circuits.Boolean.AltFormula.childLiteral_spec {n : ℕ} {i₀ : Fin n} {ls : List (Logic.PL.Literal (Fin n))} {b : Bool} {x : BitString n} (h : ∃ l ∈ ls, Logic.PL.Literal.eval x l = b) : childLiteral i₀ ls b x ∈ ls ∧ Logic.PL.Literal.eval x (childLiteral i₀ ls b x) = b

theorem Cslib.Circuits.Boolean.AltFormula.one_le_size {n d : ℕ} (f : AltFormula n (d + 1)) : 1 ≤ f.size

theorem Cslib.Circuits.Boolean.AltFormula.kwProtocol_solves {n : ℕ} (S : ℕ) (i₀ : Fin n) {d : ℕ} (op : AltOp) (f : AltFormula n d) : f.size ≤ S → ∀ (s : Bool) (x y : BitString n), eval op f x = s → eval op f y = !s → x (Communication.RoundProtocol.run (kwProtocol S i₀ op f s) x y) ≠ y (Communication.RoundProtocol.run (kwProtocol S i₀ op f s) x y)

The protocol of an alternating formula solves its game: if f has at most S gates, Alice's input makes it s and Bob's makes it !s, the inputs differ at the named coordinate.

theorem Cslib.Circuits.Boolean.AltFormula.two_rpow_lt_size_of_eval_eq_parity {d : ℕ} (hd : 2 ≤ d) : ∃ (ε : ℝ), 0 < ε ∧ ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (op : AltOp) (f : AltFormula n d), (∀ (x : BitString n), eval op f x = parity n x) → 2 ^ (ε * ↑n ^ (↑(d - 1))⁻¹) < ↑f.size + 2 * ↑n + 1

Korten's theorem for alternating formulas: for every depth d ≥ 2 there is ε > 0 such that alternating formulas of depth d computing the parity of n bits, for large n, have S + 2 n + 1 > 2 ^ (ε n ^ (1 / (d - 1))) gates S.

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

Korten's bound for alternating formulas, for majority, extending [Kor26]: the bound of two_rpow_lt_size_of_eval_eq_parity holds for majority, so the theorem of Lecomte and Ramakrishnan (exists_majority) is optimal up to the constant in the exponent.