Exchanging the players, relabelling outputs, and trivial upper bounds

Exchanging the roles of Alice and Bob in a protocol (Protocol.swapPlayers) computes the function with its arguments exchanged, and relabelling the leaves by g (Protocol.map) computes g of the function; neither changes the depth. So the communication complexity of a function is invariant under exchanging the arguments (Protocol.ecomplexityFun_swap), does not increase under relabelling the outputs or transforming the inputs (Protocol.ecomplexityFun_map_le, Protocol.ecomplexityFun_comap_le), and is unchanged by an injective (left-invertible) relabelling such as negation (Protocol.ecomplexityFun_map_of_leftInverse, Protocol.ecomplexityFun_not). All of these follow from Protocol.ecomplexityFun_le_of_forall: a function is no harder than another if every protocol for the latter yields one of no greater depth for the former.

Protocols can also be run one after another: Protocol.bind replaces each leaf of a protocol by a protocol chosen by its output, sending at most the bits of both (Protocol.depth_bind_le), and Protocol.runAll runs a tuple of protocols in turn and combines their outputs (Protocol.run_runAll, Protocol.depth_runAll_le). Relabelling is a special case of sequencing (Protocol.map_eq_bind).

Together with the trivial protocol Protocol.ecomplexityFun_le_succ, in which Alice sends her n bits and Bob announces the value, this gives the other trivial upper bounds Kushilevitz and Nisan, Chapter 1: n + 1 bits when Bob holds n bits (Protocol.ecomplexityFun_le_succ_right), min n m + 1 bits for inputs of n and m bits (Protocol.ecomplexityFun_le_min_succ), and ⌈log₂ |X|⌉ + 1 bits when Alice's input ranges over a finite type X, which she encodes in ⌈log₂ |X|⌉ bits (Protocol.ecomplexityFun_le_clog_card_succ, and Protocol.ecomplexityFun_le_clog_card_succ_right for Bob).

Main definitions

• Cslib.Communication.Protocol.swapPlayers: exchanging the roles of Alice and Bob.
• Cslib.Communication.Protocol.map: relabelling the outputs of a protocol.
• Cslib.Communication.Protocol.bind, Cslib.Communication.Protocol.runAll: running protocols one after another.

Main results

• Cslib.Communication.Protocol.ecomplexityFun_le_of_forall: comparing communication complexities through a transformation of protocols.
• Cslib.Communication.Protocol.ecomplexityFun_swap: exchanging the arguments.
• Cslib.Communication.Protocol.ecomplexityFun_map_le, Cslib.Communication.Protocol.ecomplexityFun_map_of_leftInverse, Cslib.Communication.Protocol.ecomplexityFun_not: relabelling the outputs.
• Cslib.Communication.Protocol.ecomplexityFun_comap_le: transforming the inputs.
• Cslib.Communication.Protocol.ecomplexityFun_le_succ_right, Cslib.Communication.Protocol.ecomplexityFun_le_min_succ, Cslib.Communication.Protocol.ecomplexityFun_le_clog_card_succ, Cslib.Communication.Protocol.ecomplexityFun_le_clog_card_succ_right: trivial upper bounds.

References

• E. Kushilevitz and N. Nisan, Communication Complexity

Exchanging the players

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

The protocol p with the roles of Alice and Bob exchanged: Bob sends the bits Alice sent in p, and conversely.

@[simp]

theorem Cslib.Communication.Protocol.run_swapPlayers {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (p : Protocol X Y Z) (y : Y) (x : X) : p.swapPlayers.run y x = p.run x y

The protocol with the players exchanged computes the function with its arguments exchanged.

@[simp]

theorem Cslib.Communication.Protocol.depth_swapPlayers {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (p : Protocol X Y Z) : p.swapPlayers.depth = p.depth

Exchanging the players does not change the depth.

@[simp]

theorem Cslib.Communication.Protocol.leaves_swapPlayers {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (p : Protocol X Y Z) : p.swapPlayers.leaves = p.leaves

Exchanging the players does not change the number of leaves.

@[simp]

theorem Cslib.Communication.Protocol.swapPlayers_swapPlayers {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (p : Protocol X Y Z) : p.swapPlayers.swapPlayers = p

Exchanging the players twice gives back the protocol.

Relabelling the outputs

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

The protocol p with every leaf label z replaced by g z.

@[simp]

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

The relabelled protocol outputs the relabelled value.

@[simp]

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

Relabelling the outputs does not change the depth.

@[simp]

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

Relabelling the outputs does not change the number of leaves.

Sequencing protocols

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

Run p, then the protocol q z for the output z of p: each leaf of p labelled z is replaced by q z.

@[simp]

theorem Cslib.Communication.Protocol.run_bind {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {Z' : Type u_4} (p : Protocol X Y Z) (q : Z → Protocol X Y Z') (x : X) (y : Y) : (p.bind q).run x y = (q (p.run x y)).run x y

Sequencing outputs the value of the second protocol, chosen by the output of the first.

theorem Cslib.Communication.Protocol.depth_bind_le {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {Z' : Type u_4} {p : Protocol X Y Z} {q : Z → Protocol X Y Z'} {d : ℕ} (hq : ∀ (z : Z), (q z).depth ≤ d) : (p.bind q).depth ≤ p.depth + d

Sequencing sends at most the bits of the first protocol and then those of the second.

theorem Cslib.Communication.Protocol.map_eq_bind {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {Z' : Type u_4} (g : Z → Z') (p : Protocol X Y Z) : map g p = p.bind fun (z : Z) => output (g z)

Relabelling the outputs is sequencing with protocols that only output.

def Cslib.Communication.Protocol.runAll {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {Z' : Type u_4} {k : ℕ} : (Fin k → Protocol X Y Z) → ((Fin k → Z) → Z') → Protocol X Y Z'

Run the protocols ps 0, …, ps (k - 1) one after another and output g of their outputs.

@[simp]

theorem Cslib.Communication.Protocol.run_runAll {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {Z' : Type u_4} {k : ℕ} (ps : Fin k → Protocol X Y Z) (g : (Fin k → Z) → Z') (x : X) (y : Y) : (runAll ps g).run x y = g fun (i : Fin k) => (ps i).run x y

Running the protocols one after another outputs g of their outputs.

theorem Cslib.Communication.Protocol.depth_runAll_le {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {Z' : Type u_4} {k : ℕ} {ps : Fin k → Protocol X Y Z} {g : (Fin k → Z) → Z'} {d : ℕ} (hps : ∀ (i : Fin k), (ps i).depth ≤ d) : (runAll ps g).depth ≤ k * d

Running k protocols of depth at most d one after another sends at most k d bits.

Communication complexity under these operations

theorem Cslib.Communication.Protocol.ecomplexityFun_le_of_forall {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {Z' : Type u_4} {X' : Type u_5} {Y' : Type u_6} {f : X → Y → Z} {f' : X' → Y' → Z'} (h : ∀ (p : Protocol X Y Z), p.run = f → ∃ (q : Protocol X' Y' Z'), q.run = f' ∧ q.depth ≤ p.depth) : ecomplexityFun f' ≤ ecomplexityFun f

If every protocol computing f yields one of no greater depth computing f', then f' is no harder than f.

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

Transforming the inputs does not make a function harder to compute: run a protocol for f on the transformed inputs (Protocol.comap).

theorem Cslib.Communication.Protocol.ecomplexityFun_map_le {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {Z' : Type u_4} (g : Z → Z') (f : X → Y → Z) : (ecomplexityFun fun (x : X) (y : Y) => g (f x y)) ≤ ecomplexityFun f

Relabelling the outputs does not make a function harder to compute.

theorem Cslib.Communication.Protocol.ecomplexityFun_map_of_leftInverse {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {Z' : Type u_4} {g : Z → Z'} {g' : Z' → Z} (hg : Function.LeftInverse g' g) (f : X → Y → Z) : (ecomplexityFun fun (x : X) (y : Y) => g (f x y)) = ecomplexityFun f

An injective relabelling g of the outputs, given with a left inverse g', does not change the communication complexity.

@[simp]

theorem Cslib.Communication.Protocol.ecomplexityFun_not {X : Type u_1} {Y : Type u_2} (f : X → Y → Bool) : (ecomplexityFun fun (x : X) (y : Y) => !f x y) = ecomplexityFun f

Negating the output does not change the communication complexity.

theorem Cslib.Communication.Protocol.ecomplexityFun_swap {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (f : X → Y → Z) : (ecomplexityFun fun (y : Y) (x : X) => f x y) = ecomplexityFun f

Exchanging the arguments, and so the roles of Alice and Bob, does not change the communication complexity.

Trivial upper bounds

theorem Cslib.Communication.Protocol.ecomplexityFun_le_succ_right {X : Type u_1} {n : ℕ} (f : X → BitString n → Bool) : ecomplexityFun f ≤ ↑n + 1

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

theorem Cslib.Communication.Protocol.ecomplexityFun_le_min_succ {n m : ℕ} (f : BitString n → BitString m → Bool) : ecomplexityFun f ≤ ↑(min n m) + 1

Every Boolean function of Alice's n bits and Bob's m bits has a protocol with min n m + 1 bits: the player with the shorter input sends it.

theorem Cslib.Communication.Protocol.ecomplexityFun_le_clog_card_succ {X : Type u_1} {Y : Type u_2} [Fintype X] (f : X → Y → Bool) : ecomplexityFun f ≤ ↑(Nat.clog 2 (Fintype.card X)) + 1

The trivial protocol for a finite input type. If Alice's input ranges over a finite type X, every Boolean function has a protocol with ⌈log₂ |X|⌉ + 1 bits: Alice sends an encoding of her input in ⌈log₂ |X|⌉ bits and Bob announces the value.

theorem Cslib.Communication.Protocol.ecomplexityFun_le_clog_card_succ_right {X : Type u_1} {Y : Type u_2} [Fintype Y] (f : X → Y → Bool) : ecomplexityFun f ≤ ↑(Nat.clog 2 (Fintype.card Y)) + 1

If Bob's input ranges over a finite type Y, every Boolean function has a protocol with ⌈log₂ |Y|⌉ + 1 bits.