Deterministic communication protocols

Alice holds x : X and Bob holds y : Y. A deterministic protocol is a binary tree whose internal nodes are owned by one of the players, who sends one bit computed from their input to choose the branch, and whose leaves are labelled by outputs (Protocol.run) Kushilevitz and Nisan, Chapter 1. Its depth is the number of bits sent in the worst case, and a protocol of depth d has at most 2 ^ d leaves (Protocol.leaves_le_two_pow_depth). A function of the two inputs solves a relation R on inputs from A × B when its value on every such pair is related to the pair (Solves), and a protocol solves R when its output does (Protocol.Solves); the communication complexity of R on A × B is the least depth of a protocol solving it, or ⊤ if there is none (Protocol.ecomplexity) Kushilevitz and Nisan, Chapter 5. The communication complexity of computing a function f is that of the relation f x y = z on all inputs (Protocol.ecomplexityFun), and a protocol solves that relation exactly when it computes f (Protocol.solves_univ_iff). A protocol can be run on transformed inputs (Protocol.comap).

Alice can send a bit string in as many bits (Protocol.aliceSend), so every Boolean function of Alice's n bits and Bob's input has a protocol with n + 1 bits: Alice sends her input and Bob announces the value (Protocol.ecomplexityFun_le_succ).

Main definitions

• Cslib.Communication.Solves: a function of the two inputs solves a relation.
• Cslib.Communication.Protocol: deterministic two-party protocols.
• Cslib.Communication.Protocol.run, Cslib.Communication.Protocol.depth, Cslib.Communication.Protocol.leaves, Cslib.Communication.Protocol.Solves.
• Cslib.Communication.Protocol.ecomplexity: the communication complexity of a relation.
• Cslib.Communication.Protocol.ecomplexityFun: the communication complexity of a function.
• Cslib.Communication.Protocol.comap: running a protocol on transformed inputs.
• Cslib.Communication.Protocol.aliceSend: Alice sends a bit string.

Main results

• Cslib.Communication.Protocol.leaves_le_two_pow_depth: a protocol has at most 2 ^ depth leaves.
• Cslib.Communication.Protocol.ecomplexity_le_iff, Cslib.Communication.Protocol.le_ecomplexity_iff: upper and lower bounds on communication complexity.
• Cslib.Communication.Protocol.ecomplexityFun_le_iff, Cslib.Communication.Protocol.le_ecomplexityFun_iff: the same for functions.
• Cslib.Communication.Protocol.ecomplexityFun_le_succ: the trivial protocol.

References

• E. Kushilevitz and N. Nisan, Communication Complexity

def Cslib.Communication.Solves {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (f : X → Y → Z) (R : X → Y → Z → Prop) (A : Set X) (B : Set Y) : Prop

A function f of Alice's input x : X and Bob's input y : Y solves the relation R on A × B when f x y is related to x and y for every pair from A × B. A protocol solves a relation when its output does (Protocol.Solves).

theorem Cslib.Communication.Solves.mono {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y → Z} {R : X → Y → Z → Prop} {A A' : Set X} {B B' : Set Y} (h : Solves f R A B) (hA : A' ⊆ A) (hB : B' ⊆ B) : Solves f R A' B'

A function solving a relation on A × B solves it on smaller sets.

theorem Cslib.Communication.Solves.of_imp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y → Z} {R R' : X → Y → Z → Prop} {A : Set X} {B : Set Y} (h : Solves f R A B) (hR : ∀ (x : X) (y : Y) (z : Z), R x y z → R' x y z) : Solves f R' A B

A function solving a relation solves every weaker relation.

inductive Cslib.Communication.Protocol (X : Type u_1) (Y : Type u_2) (Z : Type u_3) : Type (max (max u_1 u_2) u_3)

A deterministic protocol between Alice, holding x : X, and Bob, holding y : Y, with outputs in Z.

• output {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (z : Z) : Protocol X Y Z

  Output z.

• alice {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (send : X → Bool) (ifFalse ifTrue : Protocol X Y Z) : Protocol X Y Z

  Alice sends send x and the protocol continues with ifFalse or ifTrue.

• bob {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (send : Y → Bool) (ifFalse ifTrue : Protocol X Y Z) : Protocol X Y Z

  Bob sends send y and the protocol continues with ifFalse or ifTrue.

def Cslib.Communication.Protocol.run {X : Type u_1} {Y : Type u_2} {Z : Type u_3} : Protocol X Y Z → X → Y → Z

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

def Cslib.Communication.Protocol.depth {X : Type u_1} {Y : Type u_2} {Z : Type u_3} : Protocol X Y Z → ℕ

The number of bits sent in the worst case.

def Cslib.Communication.Protocol.leaves {X : Type u_1} {Y : Type u_2} {Z : Type u_3} : Protocol X Y Z → ℕ

The number of leaves.

@[simp]

theorem Cslib.Communication.Protocol.run_output {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (z : Z) (x : X) (y : Y) : (output z).run x y = z

@[simp]

theorem Cslib.Communication.Protocol.run_alice {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (send : X → Bool) (p₀ p₁ : Protocol X Y Z) (x : X) (y : Y) : (alice send p₀ p₁).run x y = bif send x then p₁.run x y else p₀.run x y

@[simp]

theorem Cslib.Communication.Protocol.run_bob {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (send : Y → Bool) (p₀ p₁ : Protocol X Y Z) (x : X) (y : Y) : (bob send p₀ p₁).run x y = bif send y then p₁.run x y else p₀.run x y

@[simp]

theorem Cslib.Communication.Protocol.depth_output {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (z : Z) : (output z).depth = 0

@[simp]

theorem Cslib.Communication.Protocol.depth_alice {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (send : X → Bool) (p₀ p₁ : Protocol X Y Z) : (alice send p₀ p₁).depth = max p₀.depth p₁.depth + 1

@[simp]

theorem Cslib.Communication.Protocol.depth_bob {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (send : Y → Bool) (p₀ p₁ : Protocol X Y Z) : (bob send p₀ p₁).depth = max p₀.depth p₁.depth + 1

@[simp]

theorem Cslib.Communication.Protocol.leaves_output {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (z : Z) : (output z).leaves = 1

@[simp]

theorem Cslib.Communication.Protocol.leaves_alice {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (send : X → Bool) (p₀ p₁ : Protocol X Y Z) : (alice send p₀ p₁).leaves = p₀.leaves + p₁.leaves

@[simp]

theorem Cslib.Communication.Protocol.leaves_bob {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (send : Y → Bool) (p₀ p₁ : Protocol X Y Z) : (bob send p₀ p₁).leaves = p₀.leaves + p₁.leaves

theorem Cslib.Communication.Protocol.leaves_le_two_pow_depth {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (p : Protocol X Y Z) : p.leaves ≤ 2 ^ p.depth

A protocol sending d bits has at most 2 ^ d leaves.

def Cslib.Communication.Protocol.Solves {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (p : Protocol X Y Z) (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.

noncomputable def Cslib.Communication.Protocol.ecomplexity {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (R : X → Y → Z → Prop) (A : Set X) (B : Set Y) : ℕ∞

The communication complexity of R on A × B: the least depth of a protocol solving it, or ⊤ if there is none.

theorem Cslib.Communication.Protocol.ecomplexity_le_depth {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {p : Protocol X Y Z} {R : X → Y → Z → Prop} {A : Set X} {B : Set Y} (hp : p.Solves R A B) : ecomplexity R A B ≤ ↑p.depth

theorem Cslib.Communication.Protocol.ecomplexity_ne_top_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {R : X → Y → Z → Prop} {A : Set X} {B : Set Y} : ecomplexity R A B ≠ ⊤ ↔ ∃ (p : Protocol X Y Z), p.Solves R A B

theorem Cslib.Communication.Protocol.exists_solves_depth_eq_ecomplexity {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {R : X → Y → Z → Prop} {A : Set X} {B : Set Y} (h : ∃ (p : Protocol X Y Z), p.Solves R A B) : ∃ (p : Protocol X Y Z), p.Solves R A B ∧ ↑p.depth = ecomplexity R A B

When some protocol solves R, the least depth is attained.

theorem Cslib.Communication.Protocol.ecomplexity_le_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {R : X → Y → Z → Prop} {A : Set X} {B : Set Y} {k : ℕ} : ecomplexity R A B ≤ ↑k ↔ ∃ (p : Protocol X Y Z), p.Solves R A B ∧ p.depth ≤ k

Upper bounds on communication complexity: R has communication complexity at most k on A × B exactly when some protocol of depth at most k solves it.

theorem Cslib.Communication.Protocol.le_ecomplexity_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {R : X → Y → Z → Prop} {A : Set X} {B : Set Y} {k : ℕ∞} : k ≤ ecomplexity R A B ↔ ∀ (p : Protocol X Y Z), p.Solves R A B → k ≤ ↑p.depth

Lower bounds on communication complexity are lower bounds on the depth of every protocol solving the relation, including when there is none.

theorem Cslib.Communication.Protocol.ecomplexity_mono {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {R : X → Y → Z → Prop} {A A' : Set X} {B B' : Set Y} (hA : A' ⊆ A) (hB : B' ⊆ B) : ecomplexity R A' B' ≤ ecomplexity R A B

Solving a relation on larger sets is harder.

Computing a function

noncomputable def Cslib.Communication.Protocol.ecomplexityFun {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (f : X → Y → Z) : ℕ∞

The communication complexity of computing f on all inputs: the least depth of a protocol whose output is f x y on every x and y, or ⊤ if there is none. It is ecomplexity of the relation f x y = z on all inputs.

theorem Cslib.Communication.Protocol.solves_univ_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {p : Protocol X Y Z} {f : X → Y → Z} : p.Solves (fun (x : X) (y : Y) (z : Z) => f x y = z) Set.univ Set.univ ↔ p.run = f

A protocol solves the relation f x y = z on all inputs when it computes f.

theorem Cslib.Communication.Protocol.ecomplexityFun_le_depth {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {p : Protocol X Y Z} {f : X → Y → Z} (hp : p.run = f) : ecomplexityFun f ≤ ↑p.depth

theorem Cslib.Communication.Protocol.ecomplexityFun_le_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y → Z} {k : ℕ} : ecomplexityFun f ≤ ↑k ↔ ∃ (p : Protocol X Y Z), p.run = f ∧ p.depth ≤ k

Computing f has communication complexity at most k exactly when some protocol of depth at most k computes f.

theorem Cslib.Communication.Protocol.le_ecomplexityFun_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y → Z} {k : ℕ∞} : k ≤ ecomplexityFun f ↔ ∀ (p : Protocol X Y Z), p.run = f → k ≤ ↑p.depth

Lower bounds on the communication complexity of f are lower bounds on the depth of every protocol computing f, including when there is none.

Changing the inputs

def Cslib.Communication.Protocol.comap {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {X' : Type u_4} {Y' : Type u_5} (f : X' → X) (g : Y' → Y) : Protocol X Y Z → Protocol X' Y' Z

The protocol p run on f x' and g y': Alice computes her bits from f x' and Bob his from g y'.

@[simp]

theorem Cslib.Communication.Protocol.run_comap {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {X' : Type u_4} {Y' : Type u_5} (f : X' → X) (g : Y' → Y) (p : Protocol X Y Z) (x : X') (y : Y') : (comap f g p).run x y = p.run (f x) (g y)

@[simp]

theorem Cslib.Communication.Protocol.depth_comap {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {X' : Type u_4} {Y' : Type u_5} (f : X' → X) (g : Y' → Y) (p : Protocol X Y Z) : (comap f g p).depth = p.depth

@[simp]

theorem Cslib.Communication.Protocol.leaves_comap {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {X' : Type u_4} {Y' : Type u_5} (f : X' → X) (g : Y' → Y) (p : Protocol X Y Z) : (comap f g p).leaves = p.leaves

Sending a bit string

def Cslib.Communication.Protocol.aliceSend {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (n : ℕ) : (X → BitString n) → (BitString n → Protocol X Y Z) → Protocol X Y Z

Alice sends the n bits of msg x, first bit first, after which the protocol continues with cont of the bits sent.

@[simp]

theorem Cslib.Communication.Protocol.run_aliceSend {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (n : ℕ) (msg : X → BitString n) (cont : BitString n → Protocol X Y Z) (x : X) (y : Y) : (aliceSend n msg cont).run x y = (cont (msg x)).run x y

theorem Cslib.Communication.Protocol.depth_aliceSend_le {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {n d : ℕ} {msg : X → BitString n} {cont : BitString n → Protocol X Y Z} (h : ∀ (m : BitString n), (cont m).depth ≤ d) : (aliceSend n msg cont).depth ≤ n + d

Sending n bits adds at most n to the depth.

theorem Cslib.Communication.Protocol.ecomplexityFun_le_succ {Y : Type u_2} {n : ℕ} (f : BitString n → Y → Bool) : ecomplexityFun f ≤ ↑n + 1

The trivial protocol. Every Boolean function of Alice's n bits and Bob's input has a protocol with n + 1 bits: Alice sends her input and Bob announces the value.