A public-coin protocol over shared randomness \(\Omega \), with Alice’s private input in \(X\) and Bob’s in \(Y\) producing an output in \(\alpha \), is a deterministic protocol whose combined input types are \(\Omega \times X\) (for Alice) and \(\Omega \times Y\) (for Bob). In other words, both players observe the same random string \(\omega \in \Omega \) alongside their private inputs.

The leaf node of a public-coin protocol that returns the constant value \(a \in \alpha \), constructed by lifting the corresponding deterministic output node.

Constructs a public-coin protocol node at which Alice sends a single bit: given a function \(f : X \to \Omega \to \mathrm{Bool}\), Alice transmits \(f\, x\, \omega \) and the protocol continues according to \(P : \mathrm{Bool} \to \mathrm{Protocol}\).

Constructs a public-coin protocol node at which Bob sends a single bit: given a function \(f : Y \to \Omega \to \mathrm{Bool}\), Bob transmits \(f\, y\, \omega \) and the protocol continues according to \(P : \mathrm{Bool} \to \mathrm{Protocol}\).

Given a public-coin protocol \(p\), private inputs \(x \in X\), \(y \in Y\), and a shared random string \(\omega \in \Omega \), \(\texttt{rrun}\, p\, x\, y\, \omega \) executes the underlying deterministic protocol on the paired inputs \((\omega , x)\) and \((\omega , y)\) and returns the resulting output.

A public-coin protocol \(p\) \(\varepsilon \)-satisfies a predicate \(Q : X \to Y \to \alpha \to \mathrm{Prop}\) if for every input pair \((x, y)\),

A public-coin protocol \(p\) \(\varepsilon \)-computes a function \(f : X \to Y \to \alpha \) if for every input pair \((x, y)\),

Here the volume is taken with respect to the measure on \(\Omega \) given by the MeasureSpace instance.