Protocols with messages from an alphabet

In a round protocol (RoundProtocol X Y M Z d) Alice holds x : X, Bob holds y : Y, and the players send at most d messages from an alphabet M: at each step the speaker, who may depend on the messages so far, sends one message computed from their input, and the protocol ends with an output in Z determined by the transcript (RoundProtocol.run). Bit protocols are the case of one-bit messages: a bit protocol of depth at most d is a round protocol with d messages from Bool (RoundProtocol.ofProtocol). Counting messages from a larger alphabet rather than bits is the measure of protocols with few rounds Kushilevitz and Nisan, Chapter 4. As for bit protocols, a round protocol solves a relation R on A × B when its output does (RoundProtocol.Solves, through Communication.Solves). Exchanging the speakers exchanges the inputs (RoundProtocol.run_swapPlayers), and relabelling the inputs is precomposition (RoundProtocol.run_comap).

For the Karchmer–Wigderson game on the coordinates ι both players hold inputs ι → Bool and the protocol names a coordinate (KWRoundProtocol). Such a protocol solves the game of a Boolean function f when, for every x with f x = false held by Alice and y with f y = true held by Bob, the inputs differ at the named coordinate (RoundProtocol.SolvesKW). This is the model of the top-down lower bounds of Korten Korten, Section 1.1, in which a circuit of AND/OR depth d with w wires gives a protocol with d messages from an alphabet of size w. Exchanging the speakers solves the game of the negated function (RoundProtocol.SolvesKW.swapPlayers).

Following Korten, SolvesKW f gives Alice the input where f is false. The Karchmer–Wigderson theorem for formulas (Circuits.Boolean.formulaDepth_eq_ecomplexity) uses the bit protocols of Protocol and gives Alice the input where f is true. Such a bit protocol of depth at most d solves, as a round protocol, the game of the negated function in Korten's convention (RoundProtocol.solvesKW_not_ofProtocol), so of f after exchanging the players (RoundProtocol.solvesKW_swapPlayers_ofProtocol).

Main definitions

• Cslib.Communication.RoundProtocol: protocols with at most d messages from M.
• Cslib.Communication.RoundProtocol.run, Cslib.Communication.RoundProtocol.Solves.
• Cslib.Communication.RoundProtocol.swapPlayers, Cslib.Communication.RoundProtocol.comap: exchanging the players and relabelling the inputs.
• Cslib.Communication.RoundProtocol.ofProtocol: a bit protocol as a round protocol.
• Cslib.Communication.KWRoundProtocol, Cslib.Communication.RoundProtocol.SolvesKW: round protocols for Karchmer–Wigderson games.

Main results

• Cslib.Communication.RoundProtocol.run_swapPlayers, Cslib.Communication.RoundProtocol.run_comap: exchanging the players and relabelling the inputs.
• Cslib.Communication.RoundProtocol.run_ofProtocol, Cslib.Communication.RoundProtocol.solvesKW_not_ofProtocol: bit protocols as round protocols.

References

• E. Kushilevitz and N. Nisan, Communication Complexity
• O. Korten, Top-Down Lower Bounds for All Depths

inductive Cslib.Communication.RoundProtocol (X : Type u_1) (Y : Type u_2) (M : Type u_3) (Z : Type u_4) : ℕ → Type (max (max (max u_1 u_2) u_3) u_4)

A protocol between Alice, holding x : X, and Bob, holding y : Y, with at most d messages from the alphabet M and outputs in Z. The speaker may depend on the preceding messages, and the output depends only on the transcript.

• output {X : Type u_1} {Y : Type u_2} {M : Type u_3} {Z : Type u_4} {d : ℕ} (z : Z) : RoundProtocol X Y M Z d

  Output z, possibly before exhausting the message budget.

• alice {X : Type u_1} {Y : Type u_2} {M : Type u_3} {Z : Type u_4} {d : ℕ} (send : X → M) (next : M → RoundProtocol X Y M Z d) : RoundProtocol X Y M Z (d + 1)

  Alice sends one message computed from her input.

• bob {X : Type u_1} {Y : Type u_2} {M : Type u_3} {Z : Type u_4} {d : ℕ} (send : Y → M) (next : M → RoundProtocol X Y M Z d) : RoundProtocol X Y M Z (d + 1)

  Bob sends one message computed from his input.

def Cslib.Communication.RoundProtocol.run {X : Type u_1} {Y : Type u_2} {M : Type u_5} {Z : Type u_6} {d : ℕ} : RoundProtocol X Y M Z d → X → Y → Z

The output of a protocol when Alice holds x and Bob holds y.

@[simp]

theorem Cslib.Communication.RoundProtocol.run_output {X : Type u_1} {Y : Type u_2} {M : Type u_5} {Z : Type u_6} {d : ℕ} (z : Z) (x : X) (y : Y) : (output z).run x y = z

@[simp]

theorem Cslib.Communication.RoundProtocol.run_alice {X : Type u_1} {Y : Type u_2} {M : Type u_5} {Z : Type u_6} {d : ℕ} (send : X → M) (next : M → RoundProtocol X Y M Z d) (x : X) (y : Y) : (alice send next).run x y = (next (send x)).run x y

@[simp]

theorem Cslib.Communication.RoundProtocol.run_bob {X : Type u_1} {Y : Type u_2} {M : Type u_5} {Z : Type u_6} {d : ℕ} (send : Y → M) (next : M → RoundProtocol X Y M Z d) (x : X) (y : Y) : (bob send next).run x y = (next (send y)).run x y

def Cslib.Communication.RoundProtocol.Solves {X : Type u_1} {Y : Type u_2} {M : Type u_5} {Z : Type u_6} {d : ℕ} (P : RoundProtocol X Y M Z d) (R : X → Y → Z → Prop) (A : Set X) (B : Set Y) : Prop

A protocol solves the relation R on A × B when its output does: its output on every pair of inputs from A × B is related to them. Communication.Solves.mono and Communication.Solves.of_imp apply to it.

def Cslib.Communication.RoundProtocol.speak {X : Type u_1} {M : Type u_5} {Z : Type u_6} {d : ℕ} (b : Bool) (msg : X → M) (next : M → RoundProtocol X X M Z d) : RoundProtocol X X M Z (d + 1)

One message, from players holding inputs of the same type, sent by Bob if b and by Alice otherwise.

@[simp]

theorem Cslib.Communication.RoundProtocol.run_speak {X : Type u_1} {M : Type u_5} {Z : Type u_6} {d : ℕ} (b : Bool) (msg : X → M) (next : M → RoundProtocol X X M Z d) (x y : X) : (speak b msg next).run x y = (next (msg (if b = true then y else x))).run x y

def Cslib.Communication.RoundProtocol.swapPlayers {X : Type u_1} {Y : Type u_2} {M : Type u_5} {Z : Type u_6} {d : ℕ} : RoundProtocol X Y M Z d → RoundProtocol Y X M Z d

Exchange the speakers throughout the protocol.

@[simp]

theorem Cslib.Communication.RoundProtocol.run_swapPlayers {X : Type u_1} {Y : Type u_2} {M : Type u_5} {Z : Type u_6} {d : ℕ} (P : RoundProtocol X Y M Z d) (y : Y) (x : X) : P.swapPlayers.run y x = P.run x y

Exchanging the speakers exchanges the inputs.

@[simp]

theorem Cslib.Communication.RoundProtocol.swapPlayers_swapPlayers {X : Type u_1} {Y : Type u_2} {M : Type u_5} {Z : Type u_6} {d : ℕ} (P : RoundProtocol X Y M Z d) : P.swapPlayers.swapPlayers = P

theorem Cslib.Communication.RoundProtocol.Solves.swapPlayers {X : Type u_1} {Y : Type u_2} {M : Type u_5} {Z : Type u_6} {d : ℕ} {P : RoundProtocol X Y M Z d} {R : X → Y → Z → Prop} {A : Set X} {B : Set Y} (h : P.Solves R A B) : P.swapPlayers.Solves (fun (y : Y) (x : X) => R x y) B A

Exchanging the speakers solves the relation with the inputs exchanged.

def Cslib.Communication.RoundProtocol.comap {X : Type u_1} {Y : Type u_2} {X' : Type u_3} {Y' : Type u_4} {M : Type u_5} {Z : Type u_6} (φ : X' → X) (ψ : Y' → Y) {d : ℕ} : RoundProtocol X Y M Z d → RoundProtocol X' Y' M Z d

Apply φ to Alice's input and ψ to Bob's input before running the protocol.

@[simp]

theorem Cslib.Communication.RoundProtocol.run_comap {X : Type u_1} {Y : Type u_2} {X' : Type u_3} {Y' : Type u_4} {M : Type u_5} {Z : Type u_6} (φ : X' → X) (ψ : Y' → Y) {d : ℕ} (P : RoundProtocol X Y M Z d) (x : X') (y : Y') : (comap φ ψ P).run x y = P.run (φ x) (ψ y)

Relabelling the inputs is precomposition: P.comap φ ψ outputs on x and y what P outputs on φ x and ψ y.

theorem Cslib.Communication.RoundProtocol.Solves.comap {X : Type u_1} {Y : Type u_2} {X' : Type u_3} {Y' : Type u_4} {M : Type u_5} {Z : Type u_6} {d : ℕ} {P : RoundProtocol X Y M Z d} {R : X → Y → Z → Prop} {A : Set X} {B : Set Y} (h : P.Solves R A B) (φ : X' → X) (ψ : Y' → Y) : (RoundProtocol.comap φ ψ P).Solves (fun (x : X') (y : Y') => R (φ x) (ψ y)) (φ ⁻¹' A) (ψ ⁻¹' B)

Relabelling the inputs solves the relation on the preimages.

def Cslib.Communication.RoundProtocol.ofProtocol {X : Type u_1} {Y : Type u_2} {Z : Type u_6} (p : Protocol X Y Z) (d : ℕ) : p.depth ≤ d → RoundProtocol X Y Bool Z d

A bit protocol of depth at most d as a round protocol with d messages of one bit.

@[simp]

theorem Cslib.Communication.RoundProtocol.run_ofProtocol {X : Type u_1} {Y : Type u_2} {Z : Type u_6} (p : Protocol X Y Z) (d : ℕ) (h : p.depth ≤ d) (x : X) (y : Y) : (ofProtocol p d h).run x y = p.run x y

A bit protocol of depth at most d, run as a round protocol with d messages, has the same output.

@[simp]

theorem Cslib.Communication.RoundProtocol.solves_ofProtocol_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_6} {d : ℕ} {p : Protocol X Y Z} {h : p.depth ≤ d} {R : X → Y → Z → Prop} {A : Set X} {B : Set Y} : (ofProtocol p d h).Solves R A B ↔ p.Solves R A B

A bit protocol and its round protocol solve the same relations.

@[reducible, inline]

abbrev Cslib.Communication.KWRoundProtocol (ι : Type u_1) (M : Type u_2) (d : ℕ) : Type (max u_1 u_2)

Round protocols for Karchmer–Wigderson games on the coordinates ι: Alice and Bob hold inputs ι → Bool, send at most d messages from M, and the protocol names a coordinate.

def Cslib.Communication.RoundProtocol.SolvesKW {ι : Type u_1} {M : Type u_2} {d : ℕ} (P : KWRoundProtocol ι M d) (f : (ι → Bool) → Bool) : Prop

The protocol solves the Karchmer–Wigderson game of f: Alice holds an input with f x = false, Bob one with f y = true, and they differ at the named coordinate.

theorem Cslib.Communication.RoundProtocol.solvesKW_iff_solves {ι : Type u_1} {M : Type u_2} {d : ℕ} {P : KWRoundProtocol ι M d} {f : (ι → Bool) → Bool} : SolvesKW P f ↔ Solves P DiffersAt {x : ι → Bool | f x = false} {y : ι → Bool | f y = true}

theorem Cslib.Communication.RoundProtocol.SolvesKW.swapPlayers {ι : Type u_1} {M : Type u_2} {d : ℕ} {P : KWRoundProtocol ι M d} {f : (ι → Bool) → Bool} (h : SolvesKW P f) : (RoundProtocol.swapPlayers P).SolvesKW fun (x : ι → Bool) => !f x

Exchanging the speakers solves the game of the negated function.

theorem Cslib.Communication.RoundProtocol.SolvesKW.comap_compl {ι : Type u_1} {M : Type u_2} {d : ℕ} {P : KWRoundProtocol ι M d} {f : (ι → Bool) → Bool} (h : SolvesKW P f) : (comap compl compl P).SolvesKW fun (x : ι → Bool) => f xᶜ

Negating both players' inputs solves the game of the function of the negated input.

theorem Cslib.Communication.RoundProtocol.solvesKW_not_ofProtocol {ι : Type u_1} {f : (ι → Bool) → Bool} {p : KWProtocol ι} (hp : Protocol.Solves p DiffersAt {x : ι → Bool | f x = true} {y : ι → Bool | f y = false}) (d : ℕ) (h : Protocol.depth p ≤ d) : (ofProtocol p d h).SolvesKW fun (x : ι → Bool) => !f x

A bit protocol for the Karchmer–Wigderson game of f with Alice holding the input where f is true solves, as a round protocol, the game of the negation of f in Korten's convention.

theorem Cslib.Communication.RoundProtocol.solvesKW_swapPlayers_ofProtocol {ι : Type u_1} {f : (ι → Bool) → Bool} {p : KWProtocol ι} (hp : Protocol.Solves p DiffersAt {x : ι → Bool | f x = true} {y : ι → Bool | f y = false}) (d : ℕ) (h : Protocol.depth p ≤ d) : (ofProtocol p d h).swapPlayers.SolvesKW f

A bit protocol for the Karchmer–Wigderson game of f with Alice holding the input where f is true gives, with the players exchanged, a round protocol solving SolvesKW f with one bit per message.