45 Communication Complexity — Det Composition

45.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.

45.2 Declarations

Definition 45.1 Map over protocol output

✓

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\).

Theorem 45.2 Map commutes with run

✓

For any function \(g : \alpha \to \beta \), protocol \(p\), and inputs \(x \in X\), \(y \in Y\),

\[ (\texttt{map}\; g\; p).\texttt{run}\; x\; y \; =\; g\, (p.\texttt{run}\; x\; y). \]

Theorem 45.3 Map preserves complexity

✓

For any function \(g : \alpha \to \beta \) and protocol \(p\), \((\texttt{map}\; g\; p).\texttt{complexity} = p.\texttt{complexity}\). Mapping a post-processing function over the output does not change the number of bits communicated.

Definition 45.4 Monadic bind of protocols

✓

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 \).

Theorem 45.5 Bind commutes with run

✓

For any protocol \(p\), continuation \(q\), and inputs \(x \in X\), \(y \in Y\),

\[ (\texttt{bind}\; p\; q).\texttt{run}\; x\; y \; =\; (q\, (p.\texttt{run}\; x\; y)).\texttt{run}\; x\; y. \]

Theorem 45.6 Supremum distributes over adding a constant

✓

For any finite nonempty type \(\iota \), function \(f : \iota \to \mathbb {N}\), and constant \(c \in \mathbb {N}\),

\[ \sup _{i \in \iota } (f(i) + c) \; =\; \left(\sup _{i \in \iota } f(i)\right) + c. \]

This is a technical arithmetic lemma used in complexity calculations.

Theorem 45.7 Bind complexity when continuation is constant

✓

If \(q\, a\) has the same complexity \(c\) for every output \(a\) of \(p\), then

\[ (\texttt{bind}\; p\; q).\texttt{complexity} \; =\; p.\texttt{complexity} + c. \]

Definition 45.8 Product of two protocols

✓

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.

Theorem 45.9 Product run

✓

For protocols \(p_1\), \(p_2\) and inputs \(x = (x_1, x_2)\), \(y = (y_1, y_2)\),

\[ (p_1.\texttt{prod}\; p_2).\texttt{run}\; x\; y \; =\; (p_1.\texttt{run}\; x_1\; y_1,\; p_2.\texttt{run}\; x_2\; y_2). \]

Theorem 45.10 Product complexity is additive

✓

The complexity of the product protocol satisfies

\[ (p_1.\texttt{prod}\; p_2).\texttt{complexity} \; =\; p_1.\texttt{complexity} + p_2.\texttt{complexity}. \]

Definition 45.11 \(k\)-fold product of protocols

✓

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.

Theorem 45.12 \(k\)-fold product run

✓

For a family \(p\) and input tuples \(x\), \(y\),

\[ (\texttt{pi}\; p).\texttt{run}\; x\; y \; =\; \lambda i.\; (p_i).\texttt{run}\; (x\, i)\; (y\, i). \]

Theorem 45.13 \(k\)-fold product complexity is sum

✓

The complexity of the \(k\)-fold product satisfies

\[ (\texttt{pi}\; p).\texttt{complexity} \; =\; \sum _{i=0}^{k-1} (p_i).\texttt{complexity}. \]