42 Communication Complexity — Det Composition
42.1 Overview
This module develops the monadic structure of finite-message deterministic protocols: CommunicationComplexity.Deterministic.FiniteMessage.Protocol.map, CommunicationComplexity.Deterministic.FiniteMessage.Protocol.bind, binary CommunicationComplexity.Deterministic.FiniteMessage.Protocol.prod, and \(k\)-fold CommunicationComplexity.Deterministic.FiniteMessage.Protocol.pi constructors, together with their correctness and complexity accounting theorems.
42.2 Declarations
Given a function \(g : \alpha \to \beta \) and a protocol \(p : \mathrm{Protocol}\, X\, Y\, \alpha \), CommunicationComplexity.Deterministic.FiniteMessage.Protocol.map \(g\) \(p\) is the protocol that runs \(p\) and then applies \(g\) to the output, yielding a protocol of type \(\mathrm{Protocol}\, X\, Y\, \beta \) with the same communication structure as \(p\).
Let \(g : \alpha \to \beta \) be a function between output types, let \(p\) be a finite-message protocol with outputs in \(\alpha \), and let \(x \in X\) and \(y \in Y\) be inputs. Then
Let \(X\), \(Y\), \(\alpha \), and \(\beta \) be types, let \(g : \alpha \to \beta \) be any function, and let \(p\) be a finite-message deterministic two-party communication protocol with input types \(X\), \(Y\) and output type \(\alpha \). Applying \(g\) to the output of \(p\) — that is, running \(p\) and post-processing its result through \(g\) — yields a protocol whose communication complexity equals that of \(p\):
Given a protocol \(p : \mathrm{Protocol}\, X\, Y\, \alpha \) and a continuation \(q : \alpha \to \mathrm{Protocol}\, X\, Y\, \beta \), bind \(p\) \(q\) sequentially composes them: each output leaf \(a\) of \(p\) is replaced by the sub-protocol \(q\, a\), giving a protocol of type \(\mathrm{Protocol}\, X\, Y\, \beta \).
Let \(p\) be a finite-message protocol with input types \(X\), \(Y\) and output type \(\alpha \), and let \(q\) assign to each value \(a \in \alpha \) a finite-message protocol \(q(a)\) with the same input types and output type \(\beta \). For any inputs \(x \in X\) and \(y \in Y\), executing the sequential composition of \(p\) with \(q\) agrees with first running \(p\) on \((x,y)\) to obtain an output \(a\) and then running \(q(a)\) on the same inputs:
Let \(\iota \) be a finite, nonempty type, let \(f : \iota \to \mathbb {N}\) be a function, and let \(c \in \mathbb {N}\) be a natural number. Then
Let \(p\) be a finite-message protocol with inputs of types \(X\), \(Y\) and outputs in a type \(\alpha \), and let \(q\) assign to each output value \(a \in \alpha \) a finite-message protocol \(q\, a\) with inputs of types \(X\), \(Y\) and outputs in a type \(\beta \). Suppose there is a natural number \(c\) such that every continuation has the same communication complexity, that is, \(\mathrm{complexity}(q\, a) = c\) for all \(a \in \alpha \). Then the sequential composition of \(p\) with \(q\) has communication complexity \(\mathrm{complexity}(p) + c\).
Given \(p_1 : \mathrm{Protocol}\, X_1\, Y_1\, \alpha _1\) and \(p_2 : \mathrm{Protocol}\, X_2\, Y_2\, \alpha _2\), their product \(p_1.\texttt{prod}\; p_2 : \mathrm{Protocol}\, (X_1 \times X_2)\, (Y_1 \times Y_2)\, (\alpha _1 \times \alpha _2)\) runs \(p_1\) on the first components and \(p_2\) on the second components, pairing the outputs.
Let \(p_1\) be a finite-message protocol with input types \(X_1\), \(Y_1\) and output type \(\alpha _1\), and let \(p_2\) be a finite-message protocol with input types \(X_2\), \(Y_2\) and output type \(\alpha _2\). For every pair of inputs \(x = (x_1, x_2) \in X_1 \times X_2\) and \(y = (y_1, y_2) \in Y_1 \times Y_2\), running the product protocol of \(p_1\) and \(p_2\) on \((x, y)\) yields the pair of the two componentwise executions:
Let \(p_1\) be a finite-message protocol over inputs \(X_1\), \(Y_1\) with outputs in \(\alpha _1\), and let \(p_2\) be a finite-message protocol over inputs \(X_2\), \(Y_2\) with outputs in \(\alpha _2\). Then the communication complexity of their product protocol, which runs \(p_1\) on the first input components and \(p_2\) on the second and pairs the two outputs, equals the sum of their individual complexities:
Given a family of protocols \(p_i : \mathrm{Protocol}\, X_i\, Y_i\, \alpha _i\) for \(i \in \mathrm{Fin}\, k\), pi \(p\) is the protocol of type \(\mathrm{Protocol}\, (\Pi _i\, X_i)\, (\Pi _i\, Y_i)\, (\Pi _i\, \alpha _i)\) that runs each \(p_i\) on the \(i\)-th components and collects all outputs into a tuple. It is defined by induction on \(k\), using bind, comap, and map.
Let \(k \in \mathbb {N}\), and for each index \(i \in \mathrm{Fin}\, k\) let \(p_i\) be a finite-message protocol over input types \(X_i\), \(Y_i\) with output type \(\alpha _i\). Given input tuples \(x = (x_i)_{i}\) and \(y = (y_i)_{i}\), running the \(k\)-fold product protocol on \(x\) and \(y\) yields the tuple whose \(i\)-th coordinate is the result of running \(p_i\) on the components \(x_i\) and \(y_i\); that is,
Let \(k\) be a natural number, and for each index \(i \in \{ 0, 1, \dots , k-1\} \) let \(p_i\) be a finite-message protocol over input types \(X_i\), \(Y_i\) with output type \(\alpha _i\). The \(k\)-fold product protocol runs each \(p_i\) on the \(i\)-th coordinates of a pair of input tuples in \(\prod _i X_i\) and \(\prod _i Y_i\) and collects the outputs into a tuple in \(\prod _i \alpha _i\). Then the communication complexity of the \(k\)-fold product protocol equals the sum of the communication complexities of the factors: