The rank bound and the log-rank conjecture

The communication matrix of a Boolean function f : X → Y → Bool over a ring R has rows indexed by Alice's inputs, columns indexed by Bob's inputs, and entry 1 where f is true and 0 elsewhere (communicationMatrix). A protocol computing f writes it as the sum, over the leaves labelled true, of the indicator matrices of their rectangles, each of rank at most one. So over any commutative ring with the strong rank condition, such as a field, the rank of the communication matrix is at most the number of leaves labelled true (Protocol.rank_communicationMatrix_le), and the ranks of the matrices of f and of its negation add up to at most the number of leaves (Protocol.rank_add_rank_not_le_leaves). This is the rank bound ⌈log₂ rank M_f⌉ ≤ D(f) (clog_rank_le_ecomplexity) Mehlhorn and Schmidt, Kushilevitz and Nisan, Chapter 1.

More generally, any matrix whose entry at x and y depends only on f x y, through a relabelling g of the outputs, is the sum over the leaves of matrices of rank at most one, so its rank is at most the number of leaves whose labels g does not send to zero (Protocol.rank_comp_run_le), and at most 2 ^ d for a protocol sending d bits (Protocol.rank_comp_le_two_pow). This applies in particular to the sign matrix of a Boolean function, with entries -1 where f is true and 1 elsewhere (signMatrix). Its rank exceeds that of the communication matrix by at most one (rank_signMatrix_le); when 2 ≠ 0 in the field the converse holds too, so the two ranks differ by at most one (rank_communicationMatrix_le_rank_signMatrix). In characteristic two the converse fails: the sign matrix is the all-ones matrix.

When f is false somewhere, some leaf is labelled false, so the rank of the communication matrix is less than the number of leaves (Protocol.rank_communicationMatrix_lt_leaves) and less than 2 ^ d (Protocol.rank_communicationMatrix_lt_two_pow). A protocol that is only correct on a rectangle A × B bounds the rank of the corresponding submatrix (Protocol.Solves.rank_communicationMatrix_le).

The log-rank conjecture of Lovász and Saks asserts the converse up to a polynomial: the communication complexity of every Boolean function is at most polynomial in the logarithm of the rank of its communication matrix over the reals (LogRankConjecture) [LS88]. It is open.

Main definitions

• Cslib.Communication.communicationMatrix: the communication matrix of a Boolean function.
• Cslib.Communication.signMatrix: the ±1 sign matrix of a Boolean function.
• Cslib.Communication.LogRankConjecture: the log-rank conjecture, as a proposition.

Main results

• Cslib.Communication.Protocol.rank_communicationMatrix_le: the rank of the communication matrix is at most the number of leaves labelled true.
• Cslib.Communication.Protocol.rank_add_rank_not_le_leaves: the ranks of the matrices of f and of !f add up to at most the number of leaves.
• Cslib.Communication.clog_rank_le_ecomplexity: the rank bound.
• Cslib.Communication.Protocol.rank_comp_run_le, Cslib.Communication.Protocol.rank_comp_le_leaves: the rank bound for any relabelling of the outputs.
• Cslib.Communication.Protocol.Solves.rank_communicationMatrix_le: the rank bound on a rectangle.
• Cslib.Communication.Protocol.rank_communicationMatrix_lt_leaves, Cslib.Communication.Protocol.rank_communicationMatrix_lt_two_pow: the strict rank bound for functions that are false somewhere.
• Cslib.Communication.rank_signMatrix_le, Cslib.Communication.rank_communicationMatrix_le_rank_signMatrix: the sign matrix has rank at most one more than the communication matrix, and when 2 ≠ 0 the two ranks differ by at most one.
• Cslib.Communication.Protocol.rank_signMatrix_le_leaves: the rank bound for sign matrices.

References

• K. Mehlhorn and E. M. Schmidt, Las Vegas is better than determinism in VLSI and distributed computing
• L. Lovász and M. Saks, Lattices, Möbius functions and communication complexity
• E. Kushilevitz and N. Nisan, Communication Complexity

def Cslib.Communication.communicationMatrix {X : Type u_1} {Y : Type u_2} (R : Type u_4) [Zero R] [One R] (f : X → Y → Bool) : Matrix X Y R

The communication matrix of a Boolean function f over R: rows are indexed by Alice's inputs, columns by Bob's inputs, and the entry at x and y is 1 if f x y and 0 otherwise.

@[simp]

theorem Cslib.Communication.communicationMatrix_apply {X : Type u_1} {Y : Type u_2} (R : Type u_4) [Zero R] [One R] (f : X → Y → Bool) (x : X) (y : Y) : communicationMatrix R f x y = if f x y = true then 1 else 0

theorem Cslib.Communication.Protocol.rank_comp_run_le {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {R : Type u_4} [CommSemiring R] [StrongRankCondition R] {X' : Type u_5} {Y' : Type u_6} [Fintype Y'] (p : Protocol X Y Z) (a : X' → X) (b : Y' → Y) (g : Z → R) {T : Finset (Fin p.leaves)} (hT : ∀ i ∉ T, g (p.leafOutput i) = 0) : (Matrix.of fun (x : X') (y : Y') => g (p.run (a x) (b y))).rank ≤ T.card

The rank bound for relabelled outputs. For a protocol p, maps a and b into Alice's and Bob's inputs and a relabelling g of the outputs, the matrix with entry g (p.run (a x) (b y)) at x and y has rank at most the size of any set T of leaves outside which g vanishes on the labels: it is the sum, over the leaves in T, of rank-one matrices supported on their rectangles.

theorem Cslib.Communication.Protocol.Solves.rank_communicationMatrix_le {X : Type u_1} {Y : Type u_2} {R : Type u_4} [CommSemiring R] [StrongRankCondition R] {p : Protocol X Y Bool} {f : X → Y → Bool} {A : Set X} {B : Set Y} [Fintype ↑B] (hp : p.Solves (fun (x : X) (y : Y) (b : Bool) => f x y = b) A B) : (communicationMatrix R fun (x : ↑A) (y : ↑B) => f ↑x ↑y).rank ≤ {i : Fin p.leaves | p.leafOutput i = true}.card

The rank bound on a rectangle. If a protocol computes f on A × B, the rank of the communication matrix of f restricted to A × B is at most the number of leaves labelled true.

theorem Cslib.Communication.Protocol.rank_communicationMatrix_comp_le {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {R : Type u_4} [CommSemiring R] [StrongRankCondition R] [Fintype Y] {p : Protocol X Y Z} {f : X → Y → Z} (hp : p.run = f) (g : Z → Bool) : (communicationMatrix R fun (x : X) (y : Y) => g (f x y)).rank ≤ {i : Fin p.leaves | g (p.leafOutput i) = true}.card

If a protocol computes f, then for every set of outputs, given by its indicator g, the rank of the communication matrix of g ∘ f is at most the number of leaves labelled in the set.

theorem Cslib.Communication.Protocol.rank_comp_le_leaves {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {R : Type u_4} [CommSemiring R] [StrongRankCondition R] [Fintype Y] {f : X → Y → Z} {p : Protocol X Y Z} (hp : p.run = f) (g : Z → R) : (Matrix.of fun (x : X) (y : Y) => g (f x y)).rank ≤ p.leaves

If a protocol computes f, then for every relabelling g of the outputs, the matrix with entry g (f x y) at x and y has rank at most the number of leaves.

theorem Cslib.Communication.Protocol.rank_comp_le_two_pow {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {R : Type u_4} [CommSemiring R] [StrongRankCondition R] [Fintype Y] {f : X → Y → Z} {p : Protocol X Y Z} (hp : p.run = f) (g : Z → R) : (Matrix.of fun (x : X) (y : Y) => g (f x y)).rank ≤ 2 ^ p.depth

If a protocol computes f with d bits, then for every relabelling g of the outputs, the matrix with entry g (f x y) at x and y has rank at most 2 ^ d.

theorem Cslib.Communication.Protocol.rank_communicationMatrix_le {X : Type u_1} {Y : Type u_2} {R : Type u_4} [CommSemiring R] [StrongRankCondition R] [Fintype Y] {p : Protocol X Y Bool} {f : X → Y → Bool} (hp : p.run = f) : (communicationMatrix R f).rank ≤ {i : Fin p.leaves | p.leafOutput i = true}.card

The rank bound. The rank of the communication matrix of a function computed by a protocol is at most the number of leaves labelled true.

theorem Cslib.Communication.Protocol.rank_add_rank_not_le_leaves {X : Type u_1} {Y : Type u_2} {R : Type u_4} [CommSemiring R] [StrongRankCondition R] [Fintype Y] {p : Protocol X Y Bool} {f : X → Y → Bool} (hp : p.run = f) : (communicationMatrix R f).rank + (communicationMatrix R fun (x : X) (y : Y) => !f x y).rank ≤ p.leaves

The ranks of the communication matrices of f and of its negation add up to at most the number of leaves of a protocol computing f.

theorem Cslib.Communication.Protocol.rank_communicationMatrix_le_two_pow {X : Type u_1} {Y : Type u_2} {R : Type u_4} [CommSemiring R] [StrongRankCondition R] [Fintype Y] {p : Protocol X Y Bool} {f : X → Y → Bool} (hp : p.run = f) : (communicationMatrix R f).rank ≤ 2 ^ p.depth

A protocol computing f sends at least log₂ of the rank of its communication matrix bits.

theorem Cslib.Communication.Protocol.rank_communicationMatrix_lt_leaves {X : Type u_1} {Y : Type u_2} {R : Type u_4} [CommSemiring R] [StrongRankCondition R] [Fintype Y] {p : Protocol X Y Bool} {f : X → Y → Bool} (hp : p.run = f) (h : ∃ (x : X) (y : Y), f x y = false) : (communicationMatrix R f).rank < p.leaves

The strict rank bound. If a protocol computes a function f that is false somewhere, the rank of the communication matrix of f is less than the number of leaves.

theorem Cslib.Communication.Protocol.rank_communicationMatrix_lt_two_pow {X : Type u_1} {Y : Type u_2} {R : Type u_4} [CommSemiring R] [StrongRankCondition R] [Fintype Y] {p : Protocol X Y Bool} {f : X → Y → Bool} (hp : p.run = f) (h : ∃ (x : X) (y : Y), f x y = false) : (communicationMatrix R f).rank < 2 ^ p.depth

If a protocol sending d bits computes a function f that is false somewhere, the rank of the communication matrix of f is less than 2 ^ d.

theorem Cslib.Communication.clog_rank_le_ecomplexity {X : Type u_1} {Y : Type u_2} [Fintype Y] (R : Type u_4) [CommSemiring R] [StrongRankCondition R] (f : X → Y → Bool) : ↑(Nat.clog 2 (communicationMatrix R f).rank) ≤ Protocol.ecomplexity (fun (x : X) (y : Y) (b : Bool) => f x y = b) Set.univ Set.univ

The rank bound Mehlhorn and Schmidt: the communication complexity of a Boolean function is at least ⌈log₂ r⌉, for r the rank of its communication matrix over any commutative ring with the strong rank condition, such as ℝ.

def Cslib.Communication.LogRankConjecture : Prop

The log-rank conjecture [LS88]: for some constant c, every Boolean function f on finite sets has communication complexity at most c (⌊log₂ r⌋ + 1) ^ c, where r is the rank of its communication matrix over ℝ. The rank bound clog_rank_le_ecomplexity is the converse inequality up to rounding; the conjecture is open.

Sign matrices

def Cslib.Communication.signMatrix {X : Type u_1} {Y : Type u_2} (R : Type u_4) [One R] [Neg R] (f : X → Y → Bool) : Matrix X Y R

The sign matrix of a Boolean function f over R: rows are indexed by Alice's inputs, columns by Bob's inputs, and the entry at x and y is -1 if f x y and 1 otherwise.

@[simp]

theorem Cslib.Communication.signMatrix_apply {X : Type u_1} {Y : Type u_2} (R : Type u_4) [One R] [Neg R] (f : X → Y → Bool) (x : X) (y : Y) : signMatrix R f x y = if f x y = true then -1 else 1

The entries of the sign matrix.

theorem Cslib.Communication.signMatrix_apply_eq_signVal {X : Type u_1} {Y : Type u_2} (f : X → Y → Bool) (x : X) (y : Y) : signMatrix ℝ f x y = BitString.signVal (f x y)

Over ℝ, the entries of the sign matrix are the signs BitString.signVal of the values.

theorem Cslib.Communication.signMatrix_eq_sub {X : Type u_1} {Y : Type u_2} (R : Type u_4) [Ring R] (f : X → Y → Bool) : signMatrix R f = (Matrix.of fun (x : X) (x_1 : Y) => 1) - 2 • communicationMatrix R f

The sign matrix is J - 2 M_f, for the all-ones matrix J and the communication matrix M_f.

theorem Cslib.Communication.rank_signMatrix_le {X : Type u_1} {Y : Type u_2} [Fintype Y] {R : Type u_4} [Field R] (f : X → Y → Bool) : (signMatrix R f).rank ≤ (communicationMatrix R f).rank + 1

The rank of the sign matrix exceeds that of the communication matrix by at most one, over any field.

theorem Cslib.Communication.rank_communicationMatrix_le_rank_signMatrix {X : Type u_1} {Y : Type u_2} [Fintype Y] {R : Type u_4} [Field R] [NeZero 2] (f : X → Y → Bool) : (communicationMatrix R f).rank ≤ (signMatrix R f).rank + 1

When 2 ≠ 0, the rank of the communication matrix exceeds that of the sign matrix by at most one, since M_f = (J - S_f) / 2. In characteristic two this fails: the sign matrix is the all-ones matrix.

theorem Cslib.Communication.Protocol.rank_signMatrix_le_leaves {X : Type u_1} {Y : Type u_2} [Fintype Y] {R : Type u_4} [CommRing R] [StrongRankCondition R] {f : X → Y → Bool} {p : Protocol X Y Bool} (hp : p.run = f) : (signMatrix R f).rank ≤ p.leaves

The rank of the sign matrix of a function computed by a protocol is at most the number of leaves.

theorem Cslib.Communication.Protocol.rank_signMatrix_le_two_pow {X : Type u_1} {Y : Type u_2} [Fintype Y] {R : Type u_4} [CommRing R] [StrongRankCondition R] {f : X → Y → Bool} {p : Protocol X Y Bool} (hp : p.run = f) : (signMatrix R f).rank ≤ 2 ^ p.depth

The rank of the sign matrix of a function computed by a protocol sending d bits is at most 2 ^ d.