52 Communication Complexity — Subprotocol
52.1 Overview
This module develops the theory of subprotocol embeddings for deterministic communication protocols. It introduces an inductive predicate IsSubprotocol asserting that one protocol tree is a rooted subtree of another, proves that every protocol with more than one leaf contains a balanced subprotocol (with a \(\frac{1}{3}\)–\(\frac{2}{3}\) fraction of the leaves), and provides operations for erasing, pruning, and routing inputs through subprotocols, culminating in the two-bit testSubprotocol construction.
52.2 Declarations
The inductive proposition \(\texttt{IsSubprotocol}\; s\; p\) asserts that protocol \(s\) is a rooted subtree of protocol \(p\). It is generated by: reflexivity (\(s\) is a subtree of itself), and three step cases recording that \(s\) is a subtree of one of the two children of an Alice-node or the false-child of a Bob-node, and hence a subtree of the parent.
If \(s\) is a subprotocol of \(t\) and \(t\) is a subprotocol of \(u\), then \(s\) is a subprotocol of \(u\). That is, the subprotocol relation is transitive.
Given a protocol \(p\) with \(3 \cdot p.\mathrm{numLeaves} \ge 2n\) and \(n \gt 1\), there exists a subprotocol \(s\) of \(p\) satisfying \(n \le 3 \cdot s.\mathrm{numLeaves} \lt 2n\). This is the inductive step used to prove the balanced subprotocol theorem.
If a protocol \(p\) has more than one leaf (i.e. \(p.\mathrm{numLeaves} \gt 1\)), then there exists a subprotocol \(s\) of \(p\) satisfying
In other words, \(s\) contains between one-third and two-thirds of \(p\)’s leaves.
The inductive type \(\texttt{SubprotocolPath}\; s\; p\) is a data-carrying witness that \(s\) is a rooted subtree of \(p\), recording the sequence of left/right choices made from the root of \(p\) down to the root of \(s\). It mirrors the constructors of IsSubprotocol but lives in Type rather than Prop, enabling structural recursion over the path.
Every SubprotocolPath \(s\; p\) can be mapped to a proof that \(s\) is a subprotocol of \(p\): the function SubprotocolPath.toIsSubprotocol performs this conversion by structural recursion on the path.
If \(s\) is a subprotocol of \(p\) (i.e. IsSubprotocol \(s\; p\) holds), then the type CommunicationComplexity.Deterministic.Protocol.SubprotocolPath \(s\; p\) is nonempty. That is, every propositional subprotocol embedding has at least one data-carrying path witness.
Given a proof that \(s\) is a subprotocol of \(p\), choosePath uses classical choice to extract a definite SubprotocolPath \(s\; p\) witness. The resulting function is noncomputable.
If hsp is a SubprotocolPath from \(s\) to \(p\), then \(s.\mathrm{numLeaves} \le p.\mathrm{numLeaves}\). A subtree cannot have more leaves than its parent.
Given a subprotocol path hsp from \(s\) to \(p\), reachXPath hsp is the set of Alice’s inputs \(x \in X\) that are consistent with all of Alice’s choices along the path from the root of \(p\) to the root of \(s\).
Given a subprotocol path hsp from \(s\) to \(p\), reachYPath hsp is the set of Bob’s inputs \(y \in Y\) that are consistent with all of Bob’s choices along the path from the root of \(p\) to the root of \(s\).
\(\texttt{reachesPath}\; \texttt{hsp}\; x\; y\) is the proposition that the input pair \((x, y)\) causes protocol \(p\) to reach the subprotocol \(s\) indicated by the path hsp; that is, \(x \in \texttt{reachXPath}\; \texttt{hsp}\) and \(y \in \texttt{reachYPath}\; \texttt{hsp}\).
Given a proof hsp that \(s\) is a subprotocol of \(p\), reachX hsp is the set of Alice’s inputs that reach the subprotocol, defined by applying reachXPath to the classically chosen path.
Given a proof hsp that \(s\) is a subprotocol of \(p\), reachY hsp is the set of Bob’s inputs that reach the subprotocol, defined by applying reachYPath to the classically chosen path.
\(\texttt{reaches}\; \texttt{hsp}\; x\; y\) is the proposition that input \((x, y)\) causes \(p\) to reach the subprotocol \(s\); equivalently, \(x \in \texttt{reachX}\; \texttt{hsp}\) and \(y \in \texttt{reachY}\; \texttt{hsp}\).
If the input pair \((x, y)\) reaches the subprotocol \(s\) of \(p\) via path hsp, then running \(p\) and running \(s\) on \((x, y)\) produce the same output: \(p.\texttt{run}\; x\; y = s.\texttt{run}\; x\; y\).
If hsp witnesses that \(s\) is a subprotocol of \(p\) and \((x, y)\) reaches \(s\), then \(p.\texttt{run}\; x\; y = s.\texttt{run}\; x\; y\).
chooseOutput p returns a canonical output value from protocol \(p\) by always following the false (left) branch at every Alice-node; it yields the value at the leftmost leaf.
Given a subprotocol path hsp from \(s\) to \(p\), erasePath hsp produces a new protocol that is \(p\) with the subtree \(s\) collapsed to a single leaf whose value is \(\texttt{chooseOutput}\; s\) (the leftmost leaf of \(s\)).
After erasing subprotocol \(s\) from \(p\) via path hsp, the resulting protocol has \(p.\mathrm{numLeaves} - s.\mathrm{numLeaves} + 1\) leaves.
If \((x, y)\) does not reach the subprotocol path hsp, then running the erased protocol erasePath hsp on \((x, y)\) gives the same output as running \(p\).
The noncomputable variant of erasePath that takes an IsSubprotocol proof instead of a path: erase hsp applies erasePath to the classically chosen path for hsp.
If hsp witnesses that \(s\) is a subprotocol of \(p\), then \((\texttt{erase}\; \texttt{hsp}).\mathrm{numLeaves} = p.\mathrm{numLeaves} - s.\mathrm{numLeaves} + 1\).
If \((x, y)\) does not reach the subprotocol \(s\) of \(p\), then \((\texttt{erase}\; \texttt{hsp}).\texttt{run}\; x\; y = p.\texttt{run}\; x\; y\).
deletePath hsp removes the subtree \(s\) from \(p\) by splicing out the branch leading to \(s\); the result is none if \(s = p\) (the root case) and some q otherwise, where \(q\) is \(p\) with the branch to \(s\) deleted.
If \(s.\mathrm{numLeaves} \lt p.\mathrm{numLeaves}\) (i.e. \(s\) is a proper subtree), then \(\texttt{deletePath}\; \texttt{hsp} \ne \texttt{none}\).
If \(s.\mathrm{numLeaves} \lt p.\mathrm{numLeaves}\), then there exists a protocol \(q\) such that \(\texttt{deletePath}\; \texttt{hsp} = \texttt{some}\; q\).
Given a path hsp from \(s\) to \(p\) with \(s.\mathrm{numLeaves} \lt p.\mathrm{numLeaves}\), prunePath hsp hlt is the protocol obtained by classically extracting the some value from deletePath hsp.
Under the hypothesis \(s.\mathrm{numLeaves} \lt p.\mathrm{numLeaves}\), we have \(\texttt{deletePath}\; \texttt{hsp} = \texttt{some}\; (\texttt{prunePath}\; \texttt{hsp}\; \texttt{hlt})\).
If \(\texttt{deletePath}\; \texttt{hsp} = \texttt{none}\), then \(s = p\). That is, deletion returns none only when \(s\) is the entire protocol \(p\).
If \(\texttt{deletePath}\; \texttt{hsp} = \texttt{some}\; q\), then \(q.\mathrm{numLeaves} = p.\mathrm{numLeaves} - s.\mathrm{numLeaves}\).
If \(s.\mathrm{numLeaves} \lt p.\mathrm{numLeaves}\), then \((\texttt{prunePath}\; \texttt{hsp}\; \texttt{hlt}).\mathrm{numLeaves} = p.\mathrm{numLeaves} - s.\mathrm{numLeaves}\).
If \(\texttt{deletePath}\; \texttt{hsp} = \texttt{none}\) (meaning \(s = p\)), then every input pair \((x, y)\) satisfies \(\texttt{reachesPath}\; \texttt{hsp}\; x\; y\).
If \(\texttt{deletePath}\; \texttt{hsp} = \texttt{some}\; q\) and \((x, y)\) does not reach the subprotocol path, then \(q.\texttt{run}\; x\; y = p.\texttt{run}\; x\; y\).
If \(s.\mathrm{numLeaves} \lt p.\mathrm{numLeaves}\) and \((x, y)\) does not reach the path, then \((\texttt{prunePath}\; \texttt{hsp}\; \texttt{hlt}).\texttt{run}\; x\; y = p.\texttt{run}\; x\; y\).
The noncomputable variant of prunePath taking an IsSubprotocol proof: prune hsp hlt applies CommunicationComplexity.Deterministic.Protocol.prunePath to the classically chosen path for hsp, given the strictness condition \(s.\mathrm{numLeaves} \lt p.\mathrm{numLeaves}\).
If \(s.\mathrm{numLeaves} \lt p.\mathrm{numLeaves}\), then \((\texttt{prune}\; \texttt{hsp}\; \texttt{hlt}).\mathrm{numLeaves} = p.\mathrm{numLeaves} - s.\mathrm{numLeaves}\).
If \(s.\mathrm{numLeaves} \lt p.\mathrm{numLeaves}\) and \((x, y)\) does not reach \(s\), then \((\texttt{prune}\; \texttt{hsp}\; \texttt{hlt}).\texttt{run}\; x\; y = p.\texttt{run}\; x\; y\).
Given that \(s\) is a subprotocol of \(p\) and two protocols qIn and qOut, testSubprotocol hsp qIn qOut is a noncomputable protocol that uses two bits of communication to determine whether the input reaches \(s\), then routes to qIn if it does and to qOut otherwise.
The communication complexity of testSubprotocol hsp qIn qOut equals \(2 + \max (\texttt{qIn}.\texttt{complexity},\; \texttt{qOut}.\texttt{complexity})\).
If \((x, y)\) reaches the subprotocol \(s\) of \(p\), then \((\texttt{testSubprotocol}\; \texttt{hsp}\; \texttt{qIn}\; \texttt{qOut}).\texttt{run}\; x\; y = \texttt{qIn}.\texttt{run}\; x\; y\).
If \((x, y)\) does not reach the subprotocol \(s\) of \(p\), then \((\texttt{testSubprotocol}\; \texttt{hsp}\; \texttt{qIn}\; \texttt{qOut}).\texttt{run}\; x\; y = \texttt{qOut}.\texttt{run}\; x\; y\).