The monotone Karchmer–Wigderson theorem

In the monotone Karchmer–Wigderson game of a Boolean function f, Alice holds an input x with f x = 1, Bob holds an input y with f y = 0, and they must find a bit that is one in x and zero in y (Communication.ExceedsAt). Karchmer and Wigderson showed that the least depth of a monotone formula for f, with constants free, is the communication complexity of this game (Monotone.eformulaDepth_eq_ecomplexity) [KW90], Jukna, Section 3.3, Kushilevitz and Nisan, Chapter 10. Both are finite exactly when f is monotone (Monotone.eformulaDepth_ne_top_iff): when x ≤ y, no bit is one in x and zero in y.

The two translations follow the proof of the non-monotone theorem (Boolean.formulaDepth_eq_ecomplexity), and are named in parallel with it. A monotone formula gives a protocol (Formula.monotoneKWProtocol) on the pairs where it is true on Alice's input and false on Bob's: at an AND gate Bob says which argument is false on his input, at an OR gate Alice says which argument is true on hers, and an input leaf names its bit, which is then one in x and zero in y. Conversely a protocol gives a monotone formula (Protocol.monotoneKWFormula), with an OR at each of Alice's nodes, an AND at each of Bob's, and at each leaf the input it names, which is true on the inputs of Alice and false on those of Bob that reach it.

Main definitions

• Cslib.Circuits.Formula.monotoneKWProtocol: the protocol of a monotone formula.
• Cslib.Communication.Protocol.monotoneKWFormula: the monotone formula of a protocol.

Main results

• Cslib.Circuits.Monotone.exists_kwProtocol_of_computes, Cslib.Circuits.Monotone.exists_formula_of_solves: a monotone formula gives a protocol for the monotone game of no greater depth, and conversely.
• Cslib.Circuits.Monotone.eformulaDepth_eq_ecomplexity: the monotone Karchmer–Wigderson theorem.

References

• M. Karchmer and A. Wigderson, Monotone circuits for connectivity require super-logarithmic depth
• S. Jukna, Boolean Function Complexity: Advances and Frontiers
• E. Kushilevitz and N. Nisan, Communication Complexity

The protocol of a formula

def Cslib.Circuits.Formula.monotoneKWProtocol {n : ℕ} [NeZero n] : Formula Monotone.signature n → Communication.KWProtocol (Fin n)

The protocol of a monotone formula for the monotone Karchmer–Wigderson game. At an AND gate, Bob sends the value of the first argument on his input, and the protocol continues with the first argument if it is false there and with the second otherwise; at an OR gate, Alice sends the value of the first argument on her input, and the protocol continues with the first argument if it is true there and with the second otherwise; an input leaf names its bit. Constant subformulas, which the protocol never reaches when the formula is true on Alice's input and false on Bob's, output the bit 0.

theorem Cslib.Circuits.Formula.exceedsAt_run_monotoneKWProtocol {n : ℕ} [NeZero n] (F : Formula Monotone.signature n) {x y : BitString n} (hx : F.eval Monotone.interpretation x = true) (hy : F.eval Monotone.interpretation y = false) : Communication.ExceedsAt x y (Communication.Protocol.run F.monotoneKWProtocol x y)

The protocol of a monotone formula finds a bit that is one in Alice's input and zero in Bob's, when the formula is true on Alice's input and false on Bob's.

theorem Cslib.Circuits.Formula.depth_monotoneKWProtocol_le {n : ℕ} [NeZero n] (F : Formula Monotone.signature n) : Communication.Protocol.depth F.monotoneKWProtocol ≤ depthWith Monotone.binaryCost F

The protocol of a monotone formula sends at most as many bits as the formula has AND and OR gates on a path.

The formula of a protocol

noncomputable def Cslib.Communication.Protocol.monotoneKWFormula {n : ℕ} : KWProtocol (Fin n) → Set (BitString n) → Set (BitString n) → Circuits.Formula Circuits.Monotone.signature n

The monotone formula of a protocol for the monotone Karchmer–Wigderson game on A × B: an OR at each of Alice's nodes, an AND at each of Bob's, and at each leaf the input it names, or a constant if one side is empty.

theorem Cslib.Communication.Protocol.eval_monotoneKWFormula_of_mem_left {n : ℕ} {p : KWProtocol (Fin n)} {A B : Set (BitString n)} (hp : Solves p ExceedsAt A B) {x : BitString n} (hx : x ∈ A) : (monotoneKWFormula p A B).eval Circuits.Monotone.interpretation x = true

The formula of a protocol solving the monotone Karchmer–Wigderson game on A × B is true on A.

theorem Cslib.Communication.Protocol.eval_monotoneKWFormula_of_mem_right {n : ℕ} {p : KWProtocol (Fin n)} {A B : Set (BitString n)} (hp : Solves p ExceedsAt A B) {y : BitString n} (hy : y ∈ B) : (monotoneKWFormula p A B).eval Circuits.Monotone.interpretation y = false

The formula of a protocol solving the monotone Karchmer–Wigderson game on A × B is false on B.

theorem Cslib.Communication.Protocol.depthWith_monotoneKWFormula_le {n : ℕ} (p : KWProtocol (Fin n)) (A B : Set (BitString n)) : Circuits.Formula.depthWith Circuits.Monotone.binaryCost (monotoneKWFormula p A B) ≤ depth p

The formula of a protocol has as many AND and OR gates on a path as the protocol sends bits.

The monotone Karchmer–Wigderson theorem

theorem Cslib.Circuits.Monotone.exists_kwProtocol_of_computes {n : ℕ} {f : BooleanFunction n} [NeZero n] {F : Formula signature n} (hF : F.Computes interpretation f) : ∃ (p : Communication.KWProtocol (Fin n)), Communication.Protocol.Solves p Communication.ExceedsAt {x : Fin n → Bool | f x = true} {y : Fin n → Bool | f y = false} ∧ Communication.Protocol.depth p ≤ Formula.depthWith binaryCost F

A monotone formula computing f gives a protocol for its monotone Karchmer–Wigderson game, with at most as many bits as the formula has AND and OR gates on a path.

theorem Cslib.Circuits.Monotone.exists_formula_of_solves {n : ℕ} {f : BooleanFunction n} {p : Communication.KWProtocol (Fin n)} (hp : Communication.Protocol.Solves p Communication.ExceedsAt {x : Fin n → Bool | f x = true} {y : Fin n → Bool | f y = false}) : ∃ (F : Formula signature n), F.Computes interpretation f ∧ Formula.depthWith binaryCost F ≤ Communication.Protocol.depth p

A protocol for the monotone Karchmer–Wigderson game of f gives a monotone formula computing f, with at most as many AND and OR gates on a path as the protocol sends bits.

theorem Cslib.Circuits.Monotone.eformulaDepth_eq_ecomplexity {n : ℕ} [NeZero n] (f : BooleanFunction n) : eformulaDepth f = Communication.Protocol.ecomplexity Communication.ExceedsAt {x : Fin n → Bool | f x = true} {y : Fin n → Bool | f y = false}

The monotone Karchmer–Wigderson theorem. The least depth of a monotone formula for a function of at least one bit, with constants free, is the communication complexity of its monotone Karchmer–Wigderson game; in particular both are ⊤ when no monotone formula computes it.