Documentation

Complexity.Computability.Circuit.Boolean.KarchmerWigderson

The Karchmer–Wigderson theorem #

In the 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 where x and y differ (Communication.DiffersAt). Karchmer and Wigderson showed that the least depth of a De Morgan formula for f, with negations free, is the communication complexity of this game (formulaDepth_eq_ecomplexity) [KW90], Jukna, Section 3.3, Kushilevitz and Nisan, Chapter 10.

A formula gives a protocol (Formula.kwProtocol): at an AND gate, the player holding the input where the gate is false says which argument is false there; at an OR gate, the player holding the input where it is true says which argument is true; a negation exchanges the roles; an input leaf names its bit. Conversely a protocol gives a formula (Protocol.kwFormula), with an OR at each of Alice's nodes, an AND at each of Bob's, and at each leaf the literal that separates the inputs of the two players that reach it, so with negations only at the leaves. The monotone counterparts are Formula.monotoneKWProtocol and Protocol.monotoneKWFormula.

The round protocols of Korten's top-down lower bounds give Alice the input where f is false instead (Communication.RoundProtocol.SolvesKW); exchanging the players translates (Communication.RoundProtocol.solvesKW_swapPlayers_ofProtocol).

Main definitions #

Main results #

References #

source
def Cslib.Circuits.Formula.kwProtocol {n : ℕ} [NeZero n] :
Formula Boolean.signature n → Bool → Communication.KWProtocol (Fin n)

The protocol of a De Morgan formula for the Karchmer–Wigderson game, when the formula is onAlice on Alice's input: the player holding the input where an AND gate is false, or where an OR gate is true, says which argument witnesses it. Constant subformulas, which never separate the two inputs, output the bit 0.

Instances For
    source
    theorem Cslib.Circuits.Formula.differsAt_run_kwProtocol {n : ℕ} [NeZero n] (F : Formula Boolean.signature n) (onAlice : Bool) {x y : BitString n} (hx : F.eval Boolean.interpretation x = onAlice) (hy : F.eval Boolean.interpretation y = !onAlice) :
    Communication.DiffersAt x y (Communication.Protocol.run (F.kwProtocol onAlice) x y)

    The protocol of a formula finds a bit where Alice's and Bob's inputs differ, when the formula is onAlice on Alice's input and !onAlice on Bob's.

    source
    theorem Cslib.Circuits.Formula.depth_kwProtocol_le {n : ℕ} [NeZero n] (F : Formula Boolean.signature n) (onAlice : Bool) :
    Communication.Protocol.depth (F.kwProtocol onAlice) ≤ depthWith Boolean.binaryCost F

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

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

    The formula of a protocol for the 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 a literal true on the inputs of A and false on those of B that reach it, or a constant if one side is empty.

    Instances For
      source
      theorem Cslib.Communication.Protocol.depthWith_kwFormula_le {n : ℕ} (p : KWProtocol (Fin n)) (A B : Set (BitString n)) :
      Circuits.Formula.depthWith Circuits.Boolean.binaryCost (kwFormula 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.

      source
      theorem Cslib.Communication.Protocol.eval_kwFormula_of_mem_left {n : ℕ} {p : KWProtocol (Fin n)} {A B : Set (BitString n)} (hp : Solves p DiffersAt A B) {x : BitString n} (hx : x ∈ A) :
      (kwFormula p A B).eval Circuits.Boolean.interpretation x = true

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

      source
      theorem Cslib.Communication.Protocol.eval_kwFormula_of_mem_right {n : ℕ} {p : KWProtocol (Fin n)} {A B : Set (BitString n)} (hp : Solves p DiffersAt A B) {y : BitString n} (hy : y ∈ B) :
      (kwFormula p A B).eval Circuits.Boolean.interpretation y = false

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

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

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

      source
      theorem Cslib.Circuits.Boolean.exists_formula_of_solves {n : ℕ} {f : BooleanFunction n} {p : Communication.KWProtocol (Fin n)} (hp : Communication.Protocol.Solves p Communication.DiffersAt {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 Karchmer–Wigderson game of f gives a formula computing f, with at most as many AND and OR gates on a path as the protocol sends bits.

      source
      theorem Cslib.Circuits.Boolean.formulaDepth_eq_ecomplexity {n : ℕ} [NeZero n] (f : BooleanFunction n) :
      ↑(formulaDepth f) = Communication.Protocol.ecomplexity Communication.DiffersAt {x : Fin n → Bool | f x = true} {y : Fin n → Bool | f y = false}

      The Karchmer–Wigderson theorem. The least depth of a De Morgan formula for a function of at least one bit, with negations free, is the communication complexity of its Karchmer–Wigderson game.