70 Communication Complexity — Public Coin Composition
70.1 Overview
This module defines composition operations on public-coin finite-message communication protocols: output mapping, sequential binding, randomness reindexing, pairwise and \(k\)-fold products, fresh-randomness binding, and mixed public-coin/deterministic products. For each combinator it establishes how running the composed protocol reduces to running the components, and how the communication complexity of the composed protocol relates to those of its parts.
70.2 Declarations
Given a function \(g : \alpha \to \beta \) and a public-coin protocol \(p : \mathrm{Protocol}\; \Omega \; X\; Y\; \alpha \), the protocol \(p.\mathrm{map}\; g\) is a \(\mathrm{Protocol}\; \Omega \; X\; Y\; \beta \) that applies \(g\) to the output of \(p\) after every run, without changing the communication structure.
For any \(g : \alpha \to \beta \), protocol \(p\), inputs \(x \in X\), \(y \in Y\), and randomness \(\omega \in \Omega \), running the mapped protocol satisfies \((p.\mathrm{map}\; g).\mathrm{rrun}\; x\; y\; \omega = g\, (p.\mathrm{rrun}\; x\; y\; \omega )\).
For any \(g : \alpha \to \beta \) and protocol \(p\), the communication complexity of \(p.\mathrm{map}\; g\) equals that of \(p\): \((p.\mathrm{map}\; g).\mathrm{complexity} = p.\mathrm{complexity}\).
Given a protocol \(p : \mathrm{Protocol}\; \Omega \; X\; Y\; \alpha \) and a family \(q : \alpha \to \mathrm{Protocol}\; \Omega \; X\; Y\; \beta \), the protocol \(p.\mathrm{bind}\; q\) replaces each output \(a\) of \(p\) with the protocol \(q\; a\), both sharing the same randomness \(\Omega \).
For any \(p\), \(q\), inputs \(x \in X\), \(y \in Y\), and shared randomness \(\omega \in \Omega \), running the bound protocol satisfies \((p.\mathrm{bind}\; q).\mathrm{rrun}\; x\; y\; \omega = (q\, (p.\mathrm{rrun}\; x\; y\; \omega )).\mathrm{rrun}\; x\; y\; \omega \).
Given \(h : \Omega ' \to \Omega \) and a protocol \(p : \mathrm{Protocol}\; \Omega \; X\; Y\; \alpha \), the protocol \(\mathrm{comapRandomness}\; h\; p\) is a \(\mathrm{Protocol}\; \Omega '\; X\; Y\; \alpha \) that runs \(p\) after pre-composing the shared randomness with \(h\).
For any \(h : \Omega ' \to \Omega \), protocol \(p\), inputs \(x \in X\), \(y \in Y\), and \(\omega \in \Omega '\), running the reindexed protocol satisfies \((\mathrm{comapRandomness}\; h\; p).\mathrm{rrun}\; x\; y\; \omega = p.\mathrm{rrun}\; x\; y\; (h\; \omega )\).
For any \(h : \Omega ' \to \Omega \) and protocol \(p\), reindexing the randomness does not change the complexity: \((\mathrm{comapRandomness}\; h\; p).\mathrm{complexity} = p.\mathrm{complexity}\).
Given protocols \(p_1 : \mathrm{Protocol}\; \Omega _1\; X\; Y\; \alpha _1\) and \(p_2 : \mathrm{Protocol}\; \Omega _2\; X\; Y\; \alpha _2\), the product protocol \(\mathrm{prod}\; p_1\; p_2\) is a \(\mathrm{Protocol}\; (\Omega _1 \times \Omega _2)\; X\; Y\; (\alpha _1 \times \alpha _2)\) that runs \(p_1\) and \(p_2\) independently on the same inputs, using the first and second components of the shared randomness pair respectively.
For protocols \(p_1\), \(p_2\), inputs \(x \in X\), \(y \in Y\), and randomness \(\omega \in \Omega _1 \times \Omega _2\), running the product satisfies \((\mathrm{prod}\; p_1\; p_2).\mathrm{rrun}\; x\; y\; \omega = (p_1.\mathrm{rrun}\; x\; y\; \omega _1,\; p_2.\mathrm{rrun}\; x\; y\; \omega _2)\).
The communication complexity of \(\mathrm{prod}\; p_1\; p_2\) equals the sum of the complexities of \(p_1\) and \(p_2\): \((\mathrm{prod}\; p_1\; p_2).\mathrm{complexity} = p_1.\mathrm{complexity} + p_2.\mathrm{complexity}\).
Given a family of protocols \(p : (i : \mathrm{Fin}\; k) \to \mathrm{Protocol}\; (\Omega _i)\; X\; Y\; (\alpha _i)\) with heterogeneous randomness and output types, the \(\pi \)-protocol \(\mathrm{pi}\; p\) is a \(\mathrm{Protocol}\; (\prod _i \Omega _i)\; X\; Y\; (\prod _i \alpha _i)\) that runs each \(p_i\) independently using its own component of the shared randomness tuple.
For a family \(p\), inputs \(x \in X\), \(y \in Y\), and randomness tuple \(\omega : (i : \mathrm{Fin}\; k) \to \Omega _i\), running the \(\pi \)-protocol satisfies \((\mathrm{pi}\; p).\mathrm{rrun}\; x\; y\; \omega = \lambda i,\; (p\; i).\mathrm{rrun}\; x\; y\; (\omega \; i)\).
The complexity of \(\mathrm{pi}\; p\) equals the sum of the complexities of all components: \((\mathrm{pi}\; p).\mathrm{complexity} = \sum _{i} (p\; i).\mathrm{complexity}\).
Given \(p : \mathrm{Protocol}\; \Omega \; X\; Y\; \alpha \) and \(q : \alpha \to \mathrm{Protocol}\; \Omega '\; X\; Y\; \beta \), the protocol \(\mathrm{rbind}\; p\; q\) is a \(\mathrm{Protocol}\; (\Omega \times \Omega ')\; X\; Y\; \beta \) that first runs \(p\) using the \(\Omega \)-component of the shared randomness, then runs \(q\) on the result using the independent \(\Omega '\)-component.
For any \(p\), \(q\), inputs \(x \in X\), \(y \in Y\), and randomness pair \(\omega \in \Omega \times \Omega '\), running the fresh-randomness bound protocol satisfies \((\mathrm{rbind}\; p\; q).\mathrm{rrun}\; x\; y\; \omega = (q\, (p.\mathrm{rrun}\; x\; y\; \omega _1)).\mathrm{rrun}\; x\; y\; \omega _2\).
If every branch \(q\; a\) has the same complexity \(c \in \mathbb {N}\), then \((\mathrm{rbind}\; p\; q).\mathrm{complexity} = p.\mathrm{complexity} + c\).
Given a public-coin protocol \(p_1 : \mathrm{Protocol}\; \Omega \; X\; Y\; \alpha _1\) and a deterministic protocol \(p_2 : \mathrm{Deterministic.FiniteMessage.Protocol}\; X\; Y\; \alpha _2\), the protocol \(\mathrm{prodDet}\; p_1\; p_2\) is a \(\mathrm{Protocol}\; \Omega \; X\; Y\; (\alpha _1 \times \alpha _2)\) that runs both protocols on the same inputs and pairs their outputs, reusing the same randomness \(\Omega \).
For any \(p_1\), \(p_2\), inputs \(x \in X\), \(y \in Y\), and randomness \(\omega \in \Omega \), running the mixed product satisfies \((\mathrm{prodDet}\; p_1\; p_2).\mathrm{rrun}\; x\; y\; \omega = (p_1.\mathrm{rrun}\; x\; y\; \omega ,\; p_2.\mathrm{run}\; x\; y)\).
The complexity of \(\mathrm{prodDet}\; p_1\; p_2\) equals the sum of the complexity of \(p_1\) and the complexity of \(p_2\): \((\mathrm{prodDet}\; p_1\; p_2).\mathrm{complexity} = p_1.\mathrm{complexity} + p_2.\mathrm{complexity}\).