General protocols with bounded rounds and message alphabets

Each message is an element of M; card M ≤ 2^m expresses an m-bit per-message cost bound. Both coordinate orientations are allowed at leaves. The index bounds the number of messages on every path, with early termination.

inductive Complexity.KarchmerWigderson.RoundProtocol (ι : Type u_1) (M : Type u_2) : ℕ → Type (max u_1 u_2)

A general deterministic KW protocol with message alphabet M and at most d rounds. The speaker may depend on the preceding messages. An answer is a coordinate determined by the transcript, with no further input dependence.

• answer {ι : Type u_1} {M : Type u_2} {d : ℕ} (index : ι) : RoundProtocol ι M d

  Terminate with a coordinate, possibly before exhausting the round budget.

• alice {ι : Type u_1} {M : Type u_2} {d : ℕ} (send : (ι → Bool) → M) (next : M → RoundProtocol ι M d) : RoundProtocol ι M (d + 1)

  Alice sends one message computed from her input.

• bob {ι : Type u_1} {M : Type u_2} {d : ℕ} (send : (ι → Bool) → M) (next : M → RoundProtocol ι M d) : RoundProtocol ι M (d + 1)

  Bob sends one message computed from his input.

def Complexity.KarchmerWigderson.RoundProtocol.run {ι : Type u_1} {M : Type u_2} {d : ℕ} : RoundProtocol ι M d → (ι → Bool) → (ι → Bool) → ι

The coordinate output by a protocol on the two inputs.

Equations

• (Complexity.KarchmerWigderson.RoundProtocol.answer i).run x✝¹ x✝ = i
• (Complexity.KarchmerWigderson.RoundProtocol.alice send next).run x✝¹ x✝ = (next (send x✝¹)).run x✝¹ x✝
• (Complexity.KarchmerWigderson.RoundProtocol.bob send next).run x✝¹ x✝ = (next (send x✝)).run x✝¹ x✝

def Complexity.KarchmerWigderson.RoundProtocol.Solves {ι : Type u_1} {M : Type u_2} {d : ℕ} (P : RoundProtocol ι M d) (X Y : Finset (ι → Bool)) : Prop

Every pair in the input rectangle differs at the protocol's output coordinate.

Equations

• P.Solves X Y = ∀ (x : ι → Bool), x ∈ X → ∀ (y : ι → Bool), y ∈ Y → x (P.run x y) ≠ y (P.run x y)

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

Solve the general KW game of a Boolean function: Alice has a zero-input, Bob a one-input, and the protocol must output a differing coordinate.

Equations

• P.SolvesKW f = ∀ (x y : ι → Bool), f x = false → f y = true → x (P.run x y) ≠ y (P.run x y)

def Complexity.KarchmerWigderson.RoundProtocol.swapPlayers {ι : Type u_1} {M : Type u_2} {d : ℕ} : RoundProtocol ι M d → RoundProtocol ι M d

Swap the players throughout the protocol without changing its round or message bounds.

Equations

• (Complexity.KarchmerWigderson.RoundProtocol.answer i).swapPlayers = Complexity.KarchmerWigderson.RoundProtocol.answer i
• (Complexity.KarchmerWigderson.RoundProtocol.alice send next).swapPlayers = Complexity.KarchmerWigderson.RoundProtocol.bob send fun (a : M) => (next a).swapPlayers
• (Complexity.KarchmerWigderson.RoundProtocol.bob send next).swapPlayers = Complexity.KarchmerWigderson.RoundProtocol.alice send fun (a : M) => (next a).swapPlayers