40 Communication Complexity — Det Basic
40.1 Overview
This module formalizes deterministic two-party communication protocols in which Alice holds an input \(x : X\) and Bob holds an input \(y : Y\). It defines the inductive type CommunicationComplexity.Deterministic.Protocol together with its execution semantics, worst-case bit complexity, equivalence and correctness predicates, and structural operations (role-swap and input pull-back).
40.2 Declarations
A deterministic two-party communication protocol over input types \(X\) (Alice) and \(Y\) (Bob) producing a value of type \(\alpha \) is an inductive type with three constructors: an output node carrying the final value, an alice node in which Alice applies a function \(f : X \to \mathrm{Bool}\) to her input and branches on the resulting bit, and a bob node in which Bob does the same with a function \(g : Y \to \mathrm{Bool}\).
Given a protocol \(p\), run evaluates \(p\) on inputs \(x : X\) and \(y : Y\) by recursively following the bit-branching structure until an output node is reached, returning the stored value of type \(\alpha \).
The communication complexity of a protocol \(p\) is the worst-case total number of bits exchanged: an output node costs \(0\), while an alice or bob node costs \(1\) plus the maximum complexity of the two sub-protocols reached by the bit \(\mathtt{false}\) and the bit \(\mathtt{true}\).
Two protocols \(p\) and \(q\) over the same input and output types are equivalent if \(\texttt{run}\, p = \texttt{run}\, q\), i.e. they produce identical outputs on every pair of inputs \((x, y)\).
A protocol \(p\) computes a two-argument function \(f : X \to Y \to \alpha \) if \(p.\texttt{run}\, x\, y = f\, x\, y\) for all inputs \(x : X\) and \(y : Y\).
Given a protocol \(p\) over \(X \times Y\), swap produces a protocol over \(Y \times X\) by exchanging the roles of Alice and Bob throughout: every alice node becomes a bob node and vice versa, while output nodes are left unchanged.
Let \(p\) be a deterministic two-party communication protocol with Alice’s inputs drawn from \(X\), Bob’s inputs drawn from \(Y\), and outputs in \(\alpha \), and let \(x : X\) and \(y : Y\) be inputs. Then executing the role-swapped protocol on the input pair \((y, x)\) returns the same value as executing \(p\) on \((x, y)\).
Let \(p\) be a deterministic two-party communication protocol with Alice’s inputs drawn from a type \(X\), Bob’s from a type \(Y\), and outputs in a type \(\alpha \). Let \(p^{\mathrm{swap}}\) be the protocol obtained by interchanging the roles of Alice and Bob throughout — turning every Alice node into a Bob node and vice versa while leaving output nodes unchanged. Then \(p^{\mathrm{swap}}\) has the same communication complexity as \(p\): the worst-case number of bits exchanged is unaffected by the swap.
Let \(p\) be a deterministic two-party communication protocol with Alice’s inputs drawn from a type \(X\), Bob’s from a type \(Y\), and outputs in a type \(\alpha \). Applying the role swap twice — first exchanging the roles of Alice and Bob throughout \(p\), then exchanging them again — returns the original protocol \(p\) unchanged.
Let \(X\), \(Y\), and \(\alpha \) be types, let \(f : X \to \mathrm{Bool}\), and let \(P\) assign to each bit \(b \in \mathrm{Bool}\) a deterministic communication protocol \(P(b)\) over input types \(X\) (Alice) and \(Y\) (Bob) with output type \(\alpha \). Consider the protocol whose root is an Alice node: on inputs \(x\) and \(y\) it applies \(f\) to \(x\) and continues with \(P(f(x))\). Then there exists a protocol \(q\) over input types \(Y\) (Alice) and \(X\) (Bob) with output type \(\alpha \) such that, for all \(x \in X\) and \(y \in Y\), executing \(q\) on inputs \(y\) and \(x\) returns the same value of \(\alpha \) as executing the original Alice-rooted protocol on inputs \(x\) and \(y\), and moreover \(q\) has the same communication complexity as that protocol.
Let \(X\) and \(Y\) be the input types of Alice and Bob and let \(\alpha \) be the output type. Fix a function \(f : Y \to \mathrm{Bool}\) together with a family of deterministic communication protocols \(P(\mathtt{false})\) and \(P(\mathtt{true})\), and let \(R\) be the protocol whose root is a bob node: on inputs \(x\) (Alice) and \(y\) (Bob) it computes the bit \(f(y)\) and then runs \(P(f(y))\). Then there is a deterministic communication protocol \(q\) with the roles of Alice and Bob interchanged — Alice’s input drawn from \(Y\) and Bob’s from \(X\) — such that for all \(x\) and \(y\), running \(q\) on Alice-input \(y\) and Bob-input \(x\) yields the same output value as running \(R\) on Alice-input \(x\) and Bob-input \(y\), and moreover \(q\) has the same communication complexity as \(R\).
Given functions \(f_X : X' \to X\) and \(f_Y : Y' \to Y\), comap pulls back a protocol \(p\) over \(X \times Y\) to a protocol over \(X' \times Y'\) by pre-composing every message function with \(f_X\) or \(f_Y\) as appropriate, leaving output nodes unchanged.
Let \(p\) be a deterministic two-party communication protocol with Alice’s inputs drawn from \(X\) and Bob’s from \(Y\), producing values in \(\alpha \), and let \(f_X : X' \to X\) and \(f_Y : Y' \to Y\) be arbitrary maps of input types. Then for all \(x' \in X'\) and \(y' \in Y'\), running the pull-back of \(p\) along \(f_X\) and \(f_Y\) on the inputs \(x'\) and \(y'\) yields the same output as running \(p\) itself on the transported inputs \(f_X(x')\) and \(f_Y(y')\).
Let \(p\) be a deterministic two-party communication protocol with Alice’s inputs drawn from \(X\), Bob’s inputs from \(Y\), and outputs in \(\alpha \), and let \(f_X : X' \to X\) and \(f_Y : Y' \to Y\) be maps re-indexing the two input types. Then the pull-back protocol over \(X'\) and \(Y'\) obtained by pre-composing each of Alice’s message functions with \(f_X\) and each of Bob’s message functions with \(f_Y\) has the same communication complexity as \(p\).