51 Communication Complexity — Trees
51.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.
51.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).
Let \(s\), \(t\), and \(u\) be binary trees with node labels in a type \(\alpha \). If \(s\) is a subtree of \(t\) and \(t\) is a subtree of \(u\), then \(s\) is a subtree of \(u\).
Let \(t\) be a binary tree, and write \(\ell (t)\) for its number of leaves. Let \(n\) be a natural number with \(n \gt 1\), and suppose that \(3\, \ell (t) \ge 2n\). Then \(t\) has a subtree \(s\) whose number of leaves satisfies
Let \(t\) be a binary tree with more than one leaf, and write \(\left\lvert u\right\rvert \) for the number of leaves of a tree \(u\). Then \(t\) has a subtree \(s\) whose leaf count satisfies
Equivalently, \(s\) contains at least one third and strictly fewer than two thirds of the leaves of \(t\).