66 Communication Complexity — Private Coin Finite Message
66.1 Overview
This module defines private-coin finite-message protocols as a thin wrapper around deterministic finite-message protocols, where Alice’s input type is augmented with her private randomness space \(\Omega _X\) and Bob’s with \(\Omega _Y\). It provides constructors for Alice and Bob sending steps, an execution function rrun that separates public inputs from private coins, approximate-correctness predicates CommunicationComplexity.PrivateCoin.FiniteMessage.Protocol.ApproxSatisfies and CommunicationComplexity.PrivateCoin.FiniteMessage.Protocol.ApproxComputes, and conversions to and from the binary private-coin protocol type.
66.2 Declarations
A private-coin finite-message protocol over input types \(X\), \(Y\) with private randomness types \(\Omega _X\), \(\Omega _Y\) and output type \(\alpha \) is defined as a deterministic finite-message protocol whose effective input for Alice is \(\Omega _X \times X\) and for Bob is \(\Omega _Y \times Y\).
The leaf node of a private-coin finite-message protocol that produces the constant output \(a : \alpha \), constructed by delegating to the corresponding output constructor of the underlying deterministic finite-message protocol.
Given a function \(f : X \to \Omega _X \to \beta \) (Alice’s message function depending on her public input and private randomness) and a continuation \(P : \beta \to \mathsf{Protocol}\), constructs a protocol node at which Alice sends a \(\beta \)-valued message and execution branches on it.
Given a function \(f : Y \to \Omega _Y \to \beta \) (Bob’s message function depending on his public input and private randomness) and a continuation \(P : \beta \to \mathsf{Protocol}\), constructs a protocol node at which Bob sends a \(\beta \)-valued message and execution branches on it.
\(\texttt{rrun}\, p\, x\, y\, \omega _x\, \omega _y\) executes the protocol \(p\) on public inputs \(x : X\), \(y : Y\) with Alice’s private coin \(\omega _x : \Omega _X\) and Bob’s private coin \(\omega _y : \Omega _Y\), returning an element of \(\alpha \). It is defined by running the underlying deterministic protocol on the paired inputs \((\omega _x, x)\) and \((\omega _y, y)\).
For any protocol \(p\) and inputs \(x\), \(y\), \(\omega _x\), \(\omega _y\), we have \(p.\texttt{rrun}\, x\, y\, \omega _x\, \omega _y = p.\texttt{run}\, (\omega _x, x)\, (\omega _y, y)\). This is a definitional equality exposed 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 \(\varepsilon \in \mathbb {R}\), \(p.\texttt{ApproxComputes}\, f\, \varepsilon = p.\texttt{ApproxSatisfies}\, (\lambda \, x\, y\, a \Rightarrow a = f\, x\, y)\, \varepsilon \). That is, \(\varepsilon \)-computing \(f\) is exactly \(\varepsilon \)-satisfying the pointwise equality predicate.
Converts a private-coin finite-message protocol into a binary-tree private-coin protocol by delegating to CommunicationComplexity.Deterministic.FiniteMessage.Protocol.toProtocol.
For any protocol \(p\) and inputs \(x\), \(y\), \(\omega _x\), \(\omega _y\), \((p.\texttt{toProtocol}).\texttt{rrun}\, x\, y\, \omega _x\, \omega _y = p.\texttt{rrun}\, x\, y\, \omega _x\, \omega _y\).
For any protocol \(p\), \((p.\texttt{toProtocol}).\texttt{complexity} = p.\texttt{complexity}\).
Embeds a binary private-coin protocol into a private-coin finite-message protocol by delegating to Deterministic.FiniteMessage.Protocol.ofProtocol.
For any binary private-coin protocol \(p\) and inputs \(x\), \(y\), \(\omega _x\), \(\omega _y\), \((\texttt{ofProtocol}\, p).\texttt{rrun}\, x\, y\, \omega _x\, \omega _y = p.\texttt{rrun}\, x\, y\, \omega _x\, \omega _y\).
For any binary private-coin protocol \(p\), \((\texttt{ofProtocol}\, p).\texttt{complexity} = p.\texttt{complexity}\).
For every binary private-coin protocol \(p\), there exists a finite-message protocol \(P\) such that \(P.\texttt{rrun}\, x\, y\, \omega _x\, \omega _y = p.\texttt{rrun}\, x\, y\, \omega _x\, \omega _y\) for all inputs and coins, and \(P.\texttt{complexity} = p.\texttt{complexity}\). The witness is \(P = \texttt{ofProtocol}\, p\).