54 Communication Complexity — Trees
54.1 Overview
This module develops the binary-tree structure underlying deterministic communication protocols. It introduces the shape of a protocol as a Tree Unit, counts the leaves of that tree, defines a subtree relation on binary trees, and proves the key combinatorial fact that every binary tree with more than one leaf contains a balanced subtree holding between one third and two thirds of all leaves.
54.2 Declarations
Given a deterministic communication protocol \(p\) over input types \(X\) and \(Y\) with output type \(\alpha \), shape maps \(p\) to its underlying binary tree of type Tree Unit. An output node becomes a leaf (Tree.nil), while an Alice or Bob branching node becomes an internal node (Tree.node) whose two children are the shapes of the two sub-protocols reached by the bit \(\mathtt{false}\) and \(\mathtt{true}\), respectively.
The number of leaves (output nodes) of a protocol \(p\) is defined as \(\texttt{numLeaves}(p) = \texttt{shape}(p).\texttt{numLeaves}\), i.e. the count of Tree.nil nodes in the tree shape of \(p\).
TreeIsSubtree s t is an inductively defined proposition asserting that \(s\) is a subtree of \(t\). It has two constructors: reflexivity (\(s\) is a subtree of itself) and a descent rule (\(s\) is a subtree of the left child \(\ell \) of \(\texttt{node}(v,\ell ,r)\), hence a subtree of the whole node; an analogous right rule also exists in the implementation).
If \(s\) is a subtree of \(t\) and \(t\) is a subtree of \(u\), then \(s\) is a subtree of \(u\). That is, TreeIsSubtree is transitive.
Let \(t\) be a binary tree and \(n\) a natural number with \(n \gt 1\) and \(3 \cdot \lvert t \rvert \ge 2n\), where \(\lvert t \rvert \) denotes the number of leaves of \(t\). Then there exists a subtree \(s\) of \(t\) such that \(n \le 3\lvert s \rvert \lt 2n\).
Every binary tree \(t\) with more than one leaf has a subtree \(s\) satisfying
where \(\lvert \cdot \rvert \) denotes the leaf count. Equivalently, \(s\) contains at least one third and strictly fewer than two thirds of the total leaves of \(t\).