Equality on a finite set

Equality of n-bit strings needs n + 1 bits for 0 < n (ecomplexity_equality) Kushilevitz and Nisan, Chapter 1. More generally, equality on a finite type X with at least two elements has communication complexity exactly ⌈log₂ |X|⌉ + 1 (ecomplexityFun_equality), which is n + 1 for the n-bit strings. The upper bound is the trivial protocol (Protocol.ecomplexityFun_le_clog_card_succ). The fooling-set bound only gives |X| < 2 ^ d for a protocol sending d bits (card_lt_two_pow_of_run_eq_equality), which is weaker when |X| is not a power of two. The lower bound instead follows the protocol tree: if a protocol computes equality on a rectangle A × B that contains a pair of distinct elements, then 2 |A ∩ B| ≤ 2 ^ d (two_mul_card_inter_le_two_pow_of_solves_equality). Indeed, the first bit splits A (or B) in two; a part meeting B (or A) only in pairs of equal elements contains at most one element of A ∩ B, and the other part carries the induction.

Counting leaves, a protocol computing equality on X has at least |X| leaves labelled true, one for each diagonal pair, and at least two labelled false, since the pairs (a, b) and (b, a) for a ≠ b cannot share a leaf (card_add_two_le_leaves_of_run_eq_equality). Since negating the output does not change the communication complexity, non-equality costs as much as equality (ecomplexityFun_not_equality).

Main results

• Cslib.Communication.two_mul_card_inter_le_two_pow_of_solves_equality: the lower bound for equality on a rectangle.
• Cslib.Communication.ecomplexityFun_equality: equality on a finite type X costs exactly ⌈log₂ |X|⌉ + 1 bits.
• Cslib.Communication.ecomplexityFun_not_equality: so does non-equality.
• Cslib.Communication.card_add_two_le_leaves_of_run_eq_equality: a protocol computing equality on X has at least |X| + 2 leaves.

References

• E. Kushilevitz and N. Nisan, Communication Complexity

theorem Cslib.Communication.two_mul_card_inter_le_two_pow_of_solves_equality {X : Type u_1} [DecidableEq X] {p : Protocol X X Bool} {A B : Finset X} (hp : p.Solves (fun (x y : X) (b : Bool) => equality x y = b) ↑A ↑B) (hne : ∃ x ∈ A, ∃ y ∈ B, x ≠ y) : 2 * (A ∩ B).card ≤ 2 ^ p.depth

Equality on a rectangle. If a protocol computes equality on A × B, and A × B contains a pair of distinct elements, then 2 |A ∩ B| ≤ 2 ^ d for the number d of bits it sends.

theorem Cslib.Communication.ecomplexityFun_equality {X : Type u_1} [DecidableEq X] [Fintype X] (hX : 1 < Fintype.card X) : Protocol.ecomplexityFun equality = ↑(Nat.clog 2 (Fintype.card X)) + 1

Equality on a finite set: equality on a finite type X with at least two elements has communication complexity exactly ⌈log₂ |X|⌉ + 1.

theorem Cslib.Communication.ecomplexityFun_not_equality {X : Type u_1} [DecidableEq X] [Fintype X] (hX : 1 < Fintype.card X) : (Protocol.ecomplexityFun fun (x y : X) => !equality x y) = ↑(Nat.clog 2 (Fintype.card X)) + 1

Non-equality on a finite set: on a finite type X with at least two elements, deciding whether the inputs differ has communication complexity exactly ⌈log₂ |X|⌉ + 1.

theorem Cslib.Communication.card_add_two_le_leaves_of_run_eq_equality {X : Type u_1} [DecidableEq X] [Fintype X] (hX : 1 < Fintype.card X) {p : Protocol X X Bool} (hp : p.run = equality) : Fintype.card X + 2 ≤ p.leaves

A protocol computing equality on a finite type X with at least two elements has at least |X| + 2 leaves: |X| labelled true, one for each diagonal pair, and two labelled false, reached by (a, b) and (b, a) for any a ≠ b.