43 Communication Complexity — Det Basic
43.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).
43.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.
For any protocol \(p\) over \(X \times Y\) and any inputs \(x : X\), \(y : Y\),
For any protocol \(p\) over \(X \times Y\),
Swapping Alice and Bob twice recovers the original protocol: for any \(p\) over \(X \times Y\), \(p.\texttt{swap}.\texttt{swap} = p\).
For any alice-rooted protocol \(\texttt{alice}\; f\; P\) over \(X \times Y\), there exists a protocol \(q\) over \(Y \times X\) such that \(q.\texttt{run}\; y\; x = (\texttt{alice}\; f\; P).\texttt{run}\; x\; y\) for all \(x, y\), and \(q.\texttt{complexity} = (\texttt{alice}\; f\; P).\texttt{complexity}\). This allows reducing the bob case to the alice case in inductive arguments.
For any bob-rooted protocol \(\texttt{bob}\; g\; P\) over \(X \times Y\), there exists a protocol \(q\) over \(Y \times X\) such that \(q.\texttt{run}\; y\; x = (\texttt{bob}\; g\; P).\texttt{run}\; x\; y\) for all \(x, y\), and \(q.\texttt{complexity} = (\texttt{bob}\; g\; P).\texttt{complexity}\). This allows reducing the alice case to the bob case in inductive arguments.
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.
For any protocol \(p\) over \(X \times Y\), input maps \(f_X : X' \to X\) and \(f_Y : Y' \to Y\), and inputs \(x' : X'\), \(y' : Y'\),
For any protocol \(p\) over \(X \times Y\) and input maps \(f_X : X' \to X\), \(f_Y : Y' \to Y\),