Randomized communication protocols

In a public-coin protocol the players share random bits, which they use to draw a deterministic protocol from a distribution and run it; so a public-coin protocol is a distribution over deterministic protocols (PublicCoin). In a private-coin protocol Alice and Bob hold separate uniformly random bit strings of a and b bits, and a deterministic protocol computes the bits sent from each player's input and random bits (PrivateCoin) Kushilevitz and Nisan, Chapter 3.

A randomized protocol solves a relation R on A × B with error ε when, on every pair of inputs from A × B, its output is not related to the inputs with probability at most ε (PublicCoin.Solves, PrivateCoin.Solves). Its cost is the number of bits sent in the worst case over the inputs and the random bits (PublicCoin.depth, Protocol.depth). The public- and private-coin communication complexities are the least costs (PublicCoin.ecomplexity, PrivateCoin.ecomplexity).

Deterministic protocols are both (PublicCoin.ecomplexity_le_protocol, PrivateCoin.ecomplexity_le_protocol), and the players of a private-coin protocol can draw their random bits from public coins (PrivateCoin.toPublicCoin, PublicCoin.ecomplexity_le_privateCoin). Newman's theorem bounds the converse (PrivateCoin.ecomplexity_le_add).

If a public-coin protocol has error at most ε on every pair of inputs from A × B, then for every distribution ν on A × B some protocol it can draw has error at most ε on inputs drawn from ν (PublicCoin.Solves.exists_distributionalError_le). This averaging argument (Probability.PMF.exists_mem_support_toOuterMeasure_le) is the easy direction of Yao's principle [Yao77], and turns lower bounds on deterministic protocols over a distribution into lower bounds on randomized ones.

Main definitions

• Cslib.Communication.PublicCoin: public-coin protocols, as distributions over deterministic protocols, with PublicCoin.depth, PublicCoin.errorProb, PublicCoin.Solves and PublicCoin.ecomplexity.
• Cslib.Communication.PrivateCoin: private-coin protocols, with PrivateCoin.errorProb, PrivateCoin.Solves and PrivateCoin.ecomplexity.
• Cslib.Communication.PrivateCoin.toPublicCoin: drawing the private random bits publicly.
• Cslib.Communication.Protocol.distributionalError: the error of a deterministic protocol on inputs drawn from a distribution.

Main results

• Cslib.Communication.PublicCoin.ecomplexity_le_protocol, Cslib.Communication.PrivateCoin.ecomplexity_le_protocol: randomness does not hurt.
• Cslib.Communication.PublicCoin.ecomplexity_le_privateCoin: public coins can replace private coins.
• Cslib.Communication.PublicCoin.Solves.exists_distributionalError_le: the averaging argument.

References

• E. Kushilevitz and N. Nisan, Communication Complexity
• A. C.-C. Yao, Probabilistic computations: toward a unified measure of complexity

@[reducible, inline]

abbrev Cslib.Communication.PublicCoin (X : Type u_4) (Y : Type u_5) (Z : Type u_6) : Type (max (max u_6 u_5) u_4)

A public-coin protocol between Alice, holding x : X, and Bob, holding y : Y: the players use shared random bits to draw a deterministic protocol from this distribution, and run it.

noncomputable def Cslib.Communication.Protocol.distributionalError {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (p : Protocol X Y Z) (ν : PMF (X × Y)) (R : X → Y → Z → Prop) : ℝ

The error of a deterministic protocol on inputs drawn from ν: the probability that its output on a pair of inputs drawn from ν is not related to them by R.

noncomputable def Cslib.Communication.PublicCoin.depth {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (μ : PublicCoin X Y Z) : ℕ∞

The number of bits sent in the worst case over the inputs and the random bits: the largest depth of a protocol that can be drawn.

noncomputable def Cslib.Communication.PublicCoin.errorProb {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (μ : PublicCoin X Y Z) (R : X → Y → Z → Prop) (x : X) (y : Y) : ℝ

The probability that the protocol drawn from μ gives an output on x and y that is not related to them by R.

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

A public-coin protocol μ solves R on A × B with error ε when on every pair of inputs from A × B its output is not related to them with probability at most ε.

noncomputable def Cslib.Communication.PublicCoin.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 public-coin communication complexity of R on A × B with error ε: the least cost of a public-coin protocol solving it with error ε, or ⊤ if there is none.

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

The public-coin communication complexity of computing f with error ε: ecomplexity of the relation f x y = z on all inputs.

theorem Cslib.Communication.PublicCoin.depth_le_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {μ : PublicCoin X Y Z} {c : ℕ∞} : μ.depth ≤ c ↔ ∀ p ∈ PMF.support μ, ↑p.depth ≤ c

theorem Cslib.Communication.PublicCoin.depth_le_depth {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {μ : PublicCoin X Y Z} {p : Protocol X Y Z} (hp : p ∈ PMF.support μ) : ↑p.depth ≤ μ.depth

@[simp]

theorem Cslib.Communication.PublicCoin.depth_pure {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (p : Protocol X Y Z) : depth (PMF.pure p) = ↑p.depth

theorem Cslib.Communication.PublicCoin.errorProb_nonneg {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {μ : PublicCoin X Y Z} {R : X → Y → Z → Prop} {x : X} {y : Y} : 0 ≤ μ.errorProb R x y

theorem Cslib.Communication.PublicCoin.errorProb_le_one {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {μ : PublicCoin X Y Z} {R : X → Y → Z → Prop} {x : X} {y : Y} : μ.errorProb R x y ≤ 1

theorem Cslib.Communication.PublicCoin.errorProb_pure {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (p : Protocol X Y Z) (R : X → Y → Z → Prop) (x : X) (y : Y) : errorProb (PMF.pure p) R x y = if R x y (p.run x y) then 0 else 1

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

theorem Cslib.Communication.PublicCoin.solves_pure {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) (hε : 0 ≤ ε) : Solves (PMF.pure p) ε R A B

A deterministic protocol solving R is a public-coin protocol solving it with any nonnegative error.

theorem Cslib.Communication.PublicCoin.Solves.exists_distributionalError_le {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {μ : PublicCoin X Y Z} {R : X → Y → Z → Prop} {A : Set X} {B : Set Y} {ε : ℝ} (h : μ.Solves ε R A B) (ν : PMF (X × Y)) (hν : ∀ q ∈ ν.support, q.1 ∈ A ∧ q.2 ∈ B) : ∃ p ∈ PMF.support μ, p.distributionalError ν R ≤ ε

The averaging argument, the easy direction of Yao's principle: if μ solves R on A × B with error ε, then for every distribution ν on A × B some protocol that μ can draw errs with probability at most ε on inputs drawn from ν.

theorem Cslib.Communication.PublicCoin.ecomplexity_le_depth {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {μ : PublicCoin X Y Z} {R : X → Y → Z → Prop} {A : Set X} {B : Set Y} {ε : ℝ} (h : μ.Solves ε R A B) : ecomplexity ε R A B ≤ μ.depth

theorem Cslib.Communication.PublicCoin.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 ↔ ∀ (μ : PublicCoin X Y Z), μ.Solves ε R A B → k ≤ μ.depth

theorem Cslib.Communication.PublicCoin.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 ↔ ∃ (μ : PublicCoin X Y Z), μ.Solves ε R A B ∧ μ.depth ≤ ↑k

theorem Cslib.Communication.PublicCoin.ecomplexity_anti {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {R : X → Y → Z → Prop} {A : Set X} {B : Set Y} {ε ε' : ℝ} (hε : ε ≤ ε') : ecomplexity ε' R A B ≤ ecomplexity ε R A B

Allowing more error makes a relation easier.

theorem Cslib.Communication.PublicCoin.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.

theorem Cslib.Communication.PublicCoin.ecomplexity_le_protocol {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {R : X → Y → Z → Prop} {A : Set X} {B : Set Y} {ε : ℝ} (hε : 0 ≤ ε) : ecomplexity ε R A B ≤ Protocol.ecomplexity R A B

Public-coin protocols with nonnegative error are at least as good as deterministic ones.

theorem Cslib.Communication.PublicCoin.ecomplexityFun_le_protocol {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {ε : ℝ} {f : X → Y → Z} (hε : 0 ≤ ε) : ecomplexityFun ε f ≤ Protocol.ecomplexityFun f

theorem Cslib.Communication.PublicCoin.ecomplexityFun_comap_le {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {ε : ℝ} {X' : Type u_4} {Y' : Type u_5} (f : X → Y → Z) (a : X' → X) (b : Y' → Y) : (ecomplexityFun ε fun (x : X') (y : Y') => f (a x) (b y)) ≤ ecomplexityFun ε f

Precomposing the inputs does not make a function harder: the players apply a and b to their inputs and run a protocol for f.

@[reducible, inline]

abbrev Cslib.Communication.PrivateCoin (a b : ℕ) (X : Type u_4) (Y : Type u_5) (Z : Type u_6) : Type (max (max u_6 u_5) u_4)

A private-coin protocol in which Alice, holding x : X, also holds a and Bob, holding y : Y, also holds b private uniformly random bits: a deterministic protocol whose inputs are each player's input together with their random bits.

def Cslib.Communication.PrivateCoin.fix {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {a b : ℕ} (P : PrivateCoin a b X Y Z) (r : BitString a × BitString b) : Protocol X Y Z

The deterministic protocol obtained by fixing Alice's random bits to r.1 and Bob's to r.2.

@[simp]

theorem Cslib.Communication.PrivateCoin.run_fix {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {a b : ℕ} (P : PrivateCoin a b X Y Z) (r : BitString a × BitString b) (x : X) (y : Y) : (P.fix r).run x y = Protocol.run P (x, r.1) (y, r.2)

@[simp]

theorem Cslib.Communication.PrivateCoin.depth_fix {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {a b : ℕ} (P : PrivateCoin a b X Y Z) (r : BitString a × BitString b) : (P.fix r).depth = Protocol.depth P

noncomputable def Cslib.Communication.PrivateCoin.errorProb {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {a b : ℕ} (P : PrivateCoin a b X Y Z) (R : X → Y → Z → Prop) (x : X) (y : Y) : ℝ

The probability, over both players' random bits, that the output of P on x and y is not related to them by R.

def Cslib.Communication.PrivateCoin.Solves {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {a b : ℕ} (P : PrivateCoin a b X Y Z) (ε : ℝ) (R : X → Y → Z → Prop) (A : Set X) (B : Set Y) : Prop

A private-coin protocol P solves R on A × B with error ε when on every pair of inputs from A × B its output is not related to them with probability at most ε.

noncomputable def Cslib.Communication.PrivateCoin.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 private-coin communication complexity of R on A × B with error ε: the least depth of a private-coin protocol solving it with error ε, with any numbers of random bits, or ⊤ if there is none.

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

The private-coin communication complexity of computing f with error ε: ecomplexity of the relation f x y = z on all inputs.

noncomputable def Cslib.Communication.PrivateCoin.toPublicCoin {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {a b : ℕ} (P : PrivateCoin a b X Y Z) : PublicCoin X Y Z

The public-coin protocol in which the players draw the random bits of P from shared coins: it draws P.fix r for uniformly random r.

@[simp]

theorem Cslib.Communication.PrivateCoin.errorProb_toPublicCoin {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {a b : ℕ} (P : PrivateCoin a b X Y Z) (R : X → Y → Z → Prop) (x : X) (y : Y) : P.toPublicCoin.errorProb R x y = P.errorProb R x y

theorem Cslib.Communication.PrivateCoin.depth_toPublicCoin_le {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {a b : ℕ} (P : PrivateCoin a b X Y Z) : P.toPublicCoin.depth ≤ ↑(Protocol.depth P)

theorem Cslib.Communication.PrivateCoin.Solves.toPublicCoin {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {a b : ℕ} {P : PrivateCoin a b X Y Z} {R : X → Y → Z → Prop} {A : Set X} {B : Set Y} {ε : ℝ} (h : P.Solves ε R A B) : P.toPublicCoin.Solves ε R A B

theorem Cslib.Communication.PrivateCoin.Solves.mono {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {a b : ℕ} {P : PrivateCoin a b X Y Z} {R : X → Y → Z → Prop} {A A' : Set X} {B B' : Set Y} {ε ε' : ℝ} (h : P.Solves ε R A B) (hε : ε ≤ ε') (hA : A' ⊆ A) (hB : B' ⊆ B) : P.Solves ε' R A' B'

theorem Cslib.Communication.PrivateCoin.solves_comap {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {a b : ℕ} {R : X → Y → Z → Prop} {A : Set X} {B : Set Y} {ε : ℝ} {p : Protocol X Y Z} (hp : p.Solves R A B) (hε : 0 ≤ ε) : Solves (Protocol.comap Prod.fst Prod.fst p) ε R A B

A deterministic protocol solving R, run while ignoring the random bits, solves it with any nonnegative error.

theorem Cslib.Communication.PrivateCoin.ecomplexity_le_depth {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {a b : ℕ} {P : PrivateCoin a b X Y Z} {R : X → Y → Z → Prop} {A : Set X} {B : Set Y} {ε : ℝ} (h : P.Solves ε R A B) : ecomplexity ε R A B ≤ ↑(Protocol.depth P)

theorem Cslib.Communication.PrivateCoin.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 ↔ ∀ (a b : ℕ) (P : PrivateCoin a b X Y Z), P.Solves ε R A B → k ≤ ↑(Protocol.depth P)

theorem Cslib.Communication.PrivateCoin.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 ↔ ∃ (a : ℕ) (b : ℕ) (P : PrivateCoin a b X Y Z), P.Solves ε R A B ∧ Protocol.depth P ≤ k

theorem Cslib.Communication.PrivateCoin.ecomplexity_anti {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {R : X → Y → Z → Prop} {A : Set X} {B : Set Y} {ε ε' : ℝ} (hε : ε ≤ ε') : ecomplexity ε' R A B ≤ ecomplexity ε R A B

Allowing more error makes a relation easier.

theorem Cslib.Communication.PrivateCoin.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.

theorem Cslib.Communication.PrivateCoin.ecomplexity_le_protocol {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {R : X → Y → Z → Prop} {A : Set X} {B : Set Y} {ε : ℝ} (hε : 0 ≤ ε) : ecomplexity ε R A B ≤ Protocol.ecomplexity R A B

Private-coin protocols with nonnegative error are at least as good as deterministic ones.

theorem Cslib.Communication.PrivateCoin.ecomplexityFun_le_protocol {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {ε : ℝ} {f : X → Y → Z} (hε : 0 ≤ ε) : ecomplexityFun ε f ≤ Protocol.ecomplexityFun f

theorem Cslib.Communication.PublicCoin.ecomplexity_le_privateCoin {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 ≤ PrivateCoin.ecomplexity ε R A B

Public coins can replace private coins.

theorem Cslib.Communication.PublicCoin.ecomplexityFun_le_privateCoin {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {ε : ℝ} {f : X → Y → Z} : ecomplexityFun ε f ≤ PrivateCoin.ecomplexityFun ε f