Equality, greater-than, inner product and disjointness

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). Four classical functions of two n-bit strings need all n + 1 bits for 0 < n Kushilevitz and Nisan, Chapter 1:

• equality x = y (equality, ecomplexity_equality);
• greater-than y < x, reading bit strings as binary numerals (greaterThan, ecomplexity_greaterThan);
• the inner product x ⬝ᵥ y modulo two, the Hadamard code BitString.hadamardCode (ecomplexity_dotProduct);
• disjointness of the sets of positions where x and y are true (disjointness, ecomplexity_disjointness).

Equality, greater-than and disjointness have fooling sets of 2 ^ n pairs: the diagonal pairs (x, x) for equality and greater-than (isFoolingSet_equality, isFoolingSet_greaterThan) and the complementary pairs (x, !x) for disjointness (isFoolingSet_disjointness). For the inner product, a rectangle on which it is constant has at most 2 ^ n entries (BitString.card_mul_le_two_pow_of_hadamardCode_eq, from Lindsey's lemma), while it is false on 2 ^ (n - 1) (2 ^ n + 1) pairs and true on 2 ^ (n - 1) (2 ^ n - 1) pairs; the area bound then forces more than 2 ^ n leaves (two_pow_lt_leaves_of_run_eq_dotProduct).

Main definitions

• Cslib.Communication.equality, Cslib.Communication.greaterThan, Cslib.Communication.disjointness: equality, greater-than and disjointness.

Main results

• Cslib.Communication.ecomplexity_equality, Cslib.Communication.ecomplexity_greaterThan, Cslib.Communication.ecomplexity_dotProduct, Cslib.Communication.ecomplexity_disjointness: equality, greater-than, inner product and disjointness of n bits need n + 1 bits.

References

• E. Kushilevitz and N. Nisan, Communication Complexity

Equality and greater-than

def Cslib.Communication.equality {X : Type u_1} [DecidableEq X] (x y : X) : Bool

Equality: equality x y is true exactly when x = y.

def Cslib.Communication.greaterThan {X : Type u_1} [LinearOrder X] (x y : X) : Bool

Greater-than: greaterThan x y is true exactly when y < x.

theorem Cslib.Communication.isFoolingSet_equality {X : Type u_1} [DecidableEq X] (s : Finset X) : IsFoolingSet equality true (Finset.image (fun (x : X) => (x, x)) s)

The diagonal pairs form a fooling set for equality with value true.

theorem Cslib.Communication.isFoolingSet_greaterThan {X : Type u_1} {L : Type u_4} [LinearOrder L] [DecidableEq X] {e : X → L} (he : Function.Injective e) (s : Finset X) : IsFoolingSet (fun (x y : X) => greaterThan (e x) (e y)) false (Finset.image (fun (x : X) => (x, x)) s)

For an injective map e into a linear order, the diagonal pairs form a fooling set for greater-than after e, with value false.

theorem Cslib.Communication.isFoolingSet_le {X : Type u_1} [PartialOrder X] [DecidableLE X] [DecidableEq X] (s : Finset X) : IsFoolingSet (fun (x y : X) => decide (x ≤ y)) true (Finset.image (fun (x : X) => (x, x)) s)

In a partial order, the diagonal pairs form a fooling set for ≤ with value true, by antisymmetry.

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

Equality on a finite set needs more than log₂ of its size bits: a protocol computing equality on a set of at least two elements sends d bits with |X| < 2 ^ d. The exact cost, ⌈log₂ |X|⌉ + 1, is ecomplexityFun_equality.

theorem Cslib.Communication.card_lt_two_pow_of_run_eq_greaterThan {X : Type u_1} [Fintype X] [LinearOrder X] (hX : 1 < Fintype.card X) {p : Protocol X X Bool} (hp : p.run = greaterThan) : Fintype.card X < 2 ^ p.depth

Greater-than on a finite linear order needs more than log₂ of its size bits: a protocol computing greater-than on a linear order of at least two elements sends d bits with |X| < 2 ^ d.

theorem Cslib.Communication.ecomplexity_equality {n : ℕ} (hn : 0 < n) : Protocol.ecomplexity (fun (x y : BitString n) (b : Bool) => equality x y = b) Set.univ Set.univ = ↑n + 1

Equality of n bits needs n + 1 bits, for 0 < n. This is the case of bit strings of ecomplexityFun_equality, the exact cost of equality on any finite set.

theorem Cslib.Communication.ecomplexity_greaterThan {n : ℕ} (hn : 0 < n) : Protocol.ecomplexity (fun (x y : BitString n) (b : Bool) => greaterThan ((BitString.equivFin n) x) ((BitString.equivFin n) y) = b) Set.univ Set.univ = ↑n + 1

Greater-than of n-bit numbers needs n + 1 bits, for 0 < n: reading bit strings as binary numerals (BitString.equivFin), deciding whether Alice's number exceeds Bob's needs n + 1 bits.

Disjointness

def Cslib.Communication.disjointness {ι : Type u_4} [Fintype ι] (x y : ι → Bool) : Bool

Disjointness: disjointness x y is true exactly when no position is true in both x and y, that is, when the sets of positions where x and y are true are disjoint.

theorem Cslib.Communication.isFoolingSet_disjointness {ι : Type u_4} [Fintype ι] (s : Finset (ι → Bool)) : IsFoolingSet disjointness true (Finset.image (fun (x : ι → Bool) => (x, fun (i : ι) => !x i)) s)

The pairs (x, !x) form a fooling set for disjointness with value true.

theorem Cslib.Communication.ecomplexity_disjointness {n : ℕ} (hn : 0 < n) : Protocol.ecomplexity (fun (x y : BitString n) (b : Bool) => disjointness x y = b) Set.univ Set.univ = ↑n + 1

Disjointness of n bits needs n + 1 bits, for 0 < n.

Inner product

theorem Cslib.Communication.two_mul_card_dotProduct_eq_true_add {ι : Type u_4} [Fintype ι] [DecidableEq ι] (x : ι → Bool) : (2 * {y : ι → Bool | x ⬝ᵥ y = true}.card + if x = 0 then 2 ^ Fintype.card ι else 0) = 2 ^ Fintype.card ι

A nonzero bit string has inner product true with exactly half of all bit strings, and the zero string with none.

theorem Cslib.Communication.two_pow_lt_leaves_of_run_eq_dotProduct {ι : Type u_4} [Fintype ι] [Nonempty ι] {p : Protocol (ι → Bool) (ι → Bool) Bool} (hp : p.run = fun (x y : ι → Bool) => x ⬝ᵥ y) : 2 ^ Fintype.card ι < p.leaves

The inner product needs more than 2 ^ k leaves: a protocol computing the inner product modulo two of two k-bit strings, for 0 < k, has more than 2 ^ k leaves.

theorem Cslib.Communication.ecomplexity_dotProduct {n : ℕ} (hn : 0 < n) : Protocol.ecomplexity (fun (x y : BitString n) (b : Bool) => x ⬝ᵥ y = b) Set.univ Set.univ = ↑n + 1

The inner product of n bits needs n + 1 bits, for 0 < n.