71 Communication Complexity — Public Coin Finite Message
71.1 Overview
This module defines public-coin finite-message protocols, in which Alice and Bob each receive a shared random string \(\omega \in \Omega \) alongside their private inputs. It introduces the notions of approximate satisfaction of a predicate and approximate computation of a function, and establishes equivalences between the finite-message and binary public-coin protocol representations, preserving both run behavior and complexity.
71.2 Declarations
A public-coin finite-message protocol over shared-randomness space \(\Omega \), private input sets \(X\) and \(Y\), and output type \(\alpha \) is a deterministic finite-message protocol in which Alice’s effective input is \(\Omega \times X\) and Bob’s effective input is \(\Omega \times Y\).
The terminal (output) node of a public-coin finite-message protocol returning the constant value \(a : \alpha \).
Given a message function \(f : X \to \Omega \to \beta \) and a continuation \(P : \beta \to \mathrm{Protocol}\), this constructs the protocol node in which Alice sends a \(\beta \)-valued message determined by her private input \(x\) and the shared randomness \(\omega \), then continues with \(P\).
Given a message function \(f : Y \to \Omega \to \beta \) and a continuation \(P : \beta \to \mathrm{Protocol}\), this constructs the protocol node in which Bob sends a \(\beta \)-valued message determined by his private input \(y\) and the shared randomness \(\omega \), then continues with \(P\).
\(\mathrm{rrun}(p, x, y, \omega )\) executes the protocol \(p\) on private inputs \(x\) and \(y\) with shared randomness \(\omega \), defined as \(p.\mathrm{run}(\omega , x)\, (\omega , y)\).
For any protocol \(p\), inputs \(x\), \(y\), and shared randomness \(\omega \), \(p.\mathrm{rrun}\, x\, y\, \omega = p.\mathrm{run}\, (\omega , x)\, (\omega , y)\). This is a definitional unfolding used as a simp lemma.
A protocol \(p\) \(\varepsilon \)-satisfies a predicate \(Q : X \to Y \to \alpha \to \mathrm{Prop}\) if for every input pair \((x, y)\),
A protocol \(p\) \(\varepsilon \)-computes a function \(f : X \to Y \to \alpha \) if for every input pair \((x, y)\),
For any protocol \(p\), function \(f\), and error bound \(\varepsilon \), \(p.\mathrm{ApproxComputes}\, f\, \varepsilon = p.\mathrm{ApproxSatisfies}\, (\lambda \, x\, y\, a,\; a = f\, x\, y)\, \varepsilon \). Thus approximate computation is a special case of approximate predicate satisfaction.
Converts a public-coin finite-message protocol to a binary public-coin protocol by delegating to CommunicationComplexity.Deterministic.FiniteMessage.Protocol.toProtocol.
For any protocol \(p\), inputs \(x\), \(y\), and shared randomness \(\omega \), \((p.\mathrm{toProtocol}).\mathrm{rrun}\, x\, y\, \omega = p.\mathrm{rrun}\, x\, y\, \omega \).
For any protocol \(p\), \((p.\mathrm{toProtocol}).\mathrm{complexity} = p.\mathrm{complexity}\).
Embeds a binary public-coin protocol into a finite-message protocol by delegating to CommunicationComplexity.Deterministic.FiniteMessage.Protocol.ofProtocol.
For any binary public-coin protocol \(p\), inputs \(x\), \(y\), and shared randomness \(\omega \), \((\mathrm{ofProtocol}\, p).\mathrm{rrun}\, x\, y\, \omega = p.\mathrm{rrun}\, x\, y\, \omega \).
For any binary public-coin protocol \(p\), \((\mathrm{ofProtocol}\, p).\mathrm{complexity} = p.\mathrm{complexity}\).
For any binary public-coin protocol \(p\), there exists a finite-message protocol \(P\) such that \(P.\mathrm{rrun}\, x\, y\, \omega = p.\mathrm{rrun}\, x\, y\, \omega \) for all \(x\), \(y\), \(\omega \), and \(P.\mathrm{complexity} = p.\mathrm{complexity}\).