Documentation

Complexity.Computability.Communication.KarchmerWigderson

Karchmer–Wigderson games #

In the Karchmer–Wigderson game of a Boolean function f on the coordinates ι, Alice holds an input x : ι → Bool with f x = 1, Bob holds an input y with f y = 0, and they must name a coordinate where x and y differ (DiffersAt). In the monotone game they must name a coordinate that is one in x and zero in y (ExceedsAt), which exists when f is monotone. Protocols for both games are deterministic protocols naming a coordinate (KWProtocol). The Karchmer–Wigderson theorems identify the communication complexities of these games with the least depths of De Morgan and of monotone formulas [KW90], Jukna, Section 3.3, Kushilevitz and Nisan, Chapter 10.

Main definitions #

Main results #

References #

source
def Cslib.Communication.DiffersAt {ι : Type u_1} (x y : ι → Bool) (i : ι) :
Prop

The Karchmer–Wigderson relation: Alice's input x and Bob's input y differ at coordinate i.

Instances For
    source
    @[simp]
    theorem Cslib.Communication.differsAt_iff {ι : Type u_1} {x y : ι → Bool} {i : ι} :
    DiffersAt x y i ↔ x i ≠ y i
    source
    theorem Cslib.Communication.DiffersAt.symm {ι : Type u_1} {x y : ι → Bool} {i : ι} (h : DiffersAt x y i) :
    DiffersAt y x i

    Exchanging the inputs keeps the coordinates where they differ.

    source
    def Cslib.Communication.ExceedsAt {ι : Type u_1} (x y : ι → Bool) (i : ι) :
    Prop

    The monotone Karchmer–Wigderson relation: coordinate i is one in Alice's input x and zero in Bob's input y.

    Instances For
      source
      @[simp]
      theorem Cslib.Communication.exceedsAt_iff {ι : Type u_1} {x y : ι → Bool} {i : ι} :
      ExceedsAt x y i ↔ x i = true ∧ y i = false
      source
      theorem Cslib.Communication.ExceedsAt.differsAt {ι : Type u_1} {x y : ι → Bool} {i : ι} (h : ExceedsAt x y i) :
      DiffersAt x y i

      A solution of the monotone Karchmer–Wigderson game is a solution of the Karchmer–Wigderson game.

      source
      @[reducible, inline]
      abbrev Cslib.Communication.KWProtocol (ι : Type u_2) :
      Type u_2

      Protocols for Karchmer–Wigderson games on the coordinates ι: Alice and Bob hold inputs ι → Bool and the protocol names a coordinate.

      Instances For