44 Communication Complexity — Det Complexity
44.1 Overview
This module defines the deterministic communication complexity of a two-party function \(f : X \to Y \to \alpha \) as the infimum of the complexity (number of bits exchanged) over all deterministic protocols that compute \(f\). It also establishes the key characterizations of when this complexity is at most a given natural number \(n\), both in terms of general protocols and in terms of finite-message protocols.
44.2 Declarations
Let \(\iota \) be a type and \(f : \iota \to \mathbb {N}_\infty \) an \(\mathbb {N}_\infty \)-valued family. Then \(\inf _{i} f(i) \le n\) if and only if there exists an index \(i\) such that \(f(i) \le n\). Here \(n : \mathbb {N}\) is coerced into \(\mathbb {N}_\infty = \mathrm{ENat}\).
The deterministic communication complexity of \(f : X \to Y \to \alpha \) is defined as
The infimum is taken over all deterministic protocols \(p\) that compute \(f\), and the result lives in \(\mathrm{ENat}\) to accommodate the case where no finite protocol exists.
For \(f : X \to Y \to \alpha \) and \(n : \mathbb {N}\), we have \(D(f) \le n\) if and only if there exists a protocol \(p : \mathrm{Protocol}\; X\; Y\; \alpha \) such that \(p\) computes \(f\) and \(p.\mathrm{complexity} \le n\).
For \(f : X \to Y \to \alpha \) and \(n : \mathbb {N}\), we have \(D(f) \le n\) if and only if there exists a finite-message protocol \(p : \mathrm{FiniteMessage.Protocol}\; X\; Y\; \alpha \) such that \(p.\mathrm{run} = f\) and \(p.\mathrm{complexity} \le n\). This equivalence follows from the mutual simulation between general protocols and their finite-message counterparts.
For \(f : X \to Y \to \alpha \) and \(n : \mathbb {N}\), we have \(n \le D(f)\) (in \(\mathbb {N}_\infty \)) if and only if every protocol \(p : \mathrm{Protocol}\; X\; Y\; \alpha \) that computes \(f\) satisfies \(n \le p.\mathrm{complexity}\).