47 Communication Complexity — Finite Message
47.1 Overview
This module develops a generalized model of deterministic two-party communication protocols in which, at each step, a player sends an element of an arbitrary finite type \(\beta \) rather than a single bit. The central results establish that every such finite-message protocol can be converted to an equivalent binary protocol with the same run behavior and the same communication complexity, where each \(\beta \)-valued message is encoded using \(\lceil \log _2 |\beta | \rceil \) bits.
47.2 Declarations
A generalized deterministic two-party communication protocol over input types \(X\), \(Y\) and output type \(\alpha \). At each step a player sends an element of an arbitrary finite nonempty type \(\beta \): the alice constructor takes a function \(f : X \to \beta \) and a continuation \(P : \beta \to \mathrm{Protocol}\, X\, Y\, \alpha \), and dually for bob. The output constructor terminates the protocol with a value in \(\alpha \). This inductive type is equivalent to the binary Deterministic.Protocol up to complexity, where a \(\beta \)-valued message costs \(\lceil \log _2 |\beta | \rceil \) bits.
Given a finite-message protocol \(p\) and inputs \(x : X\), \(y : Y\), run executes \(p\) recursively: at an alice node it evaluates \(f(x)\) and follows the corresponding continuation, at a bob node it evaluates \(f(y)\), and at an output node it returns the stored value.
The worst-case communication cost of a finite-message protocol, measured in bits. An output node costs \(0\); an alice or bob node with message type \(\beta \) costs \(\lceil \log _2 |\beta | \rceil \) plus the maximum complexity over all continuations, i.e. \(\lceil \log _2 |\beta | \rceil + \sup _{b \in \beta } \mathrm{complexity}(P\, b)\).
An auxiliary construction: given \(d\) binary query functions \(\mathrm{query}_i : X \to \mathrm{Bool}\) and a family of binary protocols \(Q : (\mathrm{Fin}\, d \to \mathrm{Bool}) \to \mathrm{Protocol}\, X\, Y\, \alpha \), builds a single binary protocol that reads each query bit from Alice in sequence and then runs \(Q\) on the collected bit pattern.
For all inputs \(x : X\) and \(y : Y\), executing completeTreeAlice gives the same output as running \(Q\) applied to the bit pattern \(i \mapsto \mathrm{query}_i(x)\), i.e. \((\mathrm{completeTreeAlice}\, d\, \mathrm{query}\, Q).\mathrm{run}\, x\, y = (Q\, (\lambda i,\, \mathrm{query}_i\, x)).\mathrm{run}\, x\, y\).
The complexity of completeTreeAlice equals \(d\) plus the supremum of the complexities of all leaf protocols: \((\mathrm{completeTreeAlice}\, d\, \mathrm{query}\, Q).\mathrm{complexity} = d + \sup _{\mathrm{bits}} (Q\, \mathrm{bits}).\mathrm{complexity}\).
Given a finite nonempty type \(\beta \), a function \(f : X \to \beta \), and a family of binary protocols \(Q : \beta \to \mathrm{Protocol}\, X\, Y\, \alpha \), there exists a binary protocol \(R\) such that \(R.\mathrm{run}\, x\, y = (Q(f(x))).\mathrm{run}\, x\, y\) for all \(x,y\), and whose complexity satisfies \(R.\mathrm{complexity} = \lceil \log _2 |\beta | \rceil + \sup _{b \in \beta }(Q\, b).\mathrm{complexity}\), constructed via a complete binary tree encoding of \(\beta \).
For every finite-message protocol \(p\), there exists a binary protocol \(P\) such that \(P.\mathrm{run} = p.\mathrm{run}\) and \(P.\mathrm{complexity} = p.\mathrm{complexity}\). This is the key existence result underlying toProtocol.
A noncomputable function that converts a finite-message protocol \(p\) into a binary protocol CommunicationComplexity.Deterministic.FiniteMessage.Protocol.toProtocol \(p\) with the same run behavior and the same communication complexity, encoding each \(\beta \)-valued message as \(\lceil \log _2 |\beta | \rceil \) bits.
For every finite-message protocol \(p\), the converted binary protocol satisfies \((\texttt{toProtocol}\, p).\mathrm{run} = p.\mathrm{run}\) as functions \(X \to Y \to \alpha \).
For every finite-message protocol \(p\), the converted binary protocol satisfies \((\texttt{toProtocol}\, p).\mathrm{complexity} = p.\mathrm{complexity}\).
Embeds a binary protocol into the generalized finite-message framework by treating each Boolean message as an element of \(\beta = \mathrm{Bool}\), giving a CommunicationComplexity.Deterministic.Protocol \(X\, Y\, \alpha \) with the same tree structure.
For every binary protocol \(p\) and inputs \(x : X\), \(y : Y\), \((\texttt{ofProtocol}\, p).\mathrm{run}\, x\, y = p.\mathrm{run}\, x\, y\).
For every binary protocol \(p\), \((\texttt{ofProtocol}\, p).\mathrm{complexity} = p.\mathrm{complexity}\), using the fact that \(\lceil \log _2 |\mathrm{Bool}| \rceil = 1\).
For every binary protocol \(p\), there exists a finite-message protocol \(P\) with \(P.\mathrm{run} = p.\mathrm{run}\) and \(P.\mathrm{complexity} = p.\mathrm{complexity}\). Together with toProtocol_exists, this shows the two models are equivalent up to complexity.
Given maps \(f_X : X' \to X\) and \(f_Y : Y' \to Y\), the pullback \(p.\mathrm{comap}\, f_X\, f_Y\) is the finite-message protocol over \(X'\), \(Y'\) obtained by precomposing every message function with \(f_X\) or \(f_Y\) respectively, leaving the protocol tree structure unchanged.
For all \(x' : X'\) and \(y' : Y'\), \((p.\mathrm{comap}\, f_X\, f_Y).\mathrm{run}\, x'\, y' = p.\mathrm{run}\, (f_X\, x')\, (f_Y\, y')\).
The pullback does not change the communication complexity: \((p.\mathrm{comap}\, f_X\, f_Y).\mathrm{complexity} = p.\mathrm{complexity}\).