Chapter 172Core route

Probability, Measure, Kernels, and Computable Sampling

Run the program $xor 2 = b_{1} \leftarrow coin; b_{2} \leftarrow coin; return (b_{1} \oplus b_{2})$ in two different ways. Enumerate: there are four equiprobable assignments to $(b_{1}, b_{2})$ , of which two make $b_{1} \oplus b_{2}$ true, so the program denotes the table ${ff \mapsto 1 / 2, tt \mapsto 1 / 2}$ . Execute: feed the program a stream of fair bits, let the first $coin$ consume the first bit and the second $coin$ the second; on the stream beginning $0, 1$ the run performs $draw 0$ , $draw 1$ , $return tt$ . The two answers agree, and for this program the agreement can be checked by inspecting four cases.

Now replace $coin$ by a draw from the uniform distribution on $[0, 1]$ . The enumeration has no finite table to produce, and the two descriptions come apart: on one side a measure on an uncountable space, on the other a program that turns a bit stream into a real number. Neither side is automatically the other. A measure is a set function with no computational content; a sampler is a partial function on bit streams whose output distribution must be proved to be the intended measure.

This chapter builds the measure-theoretic vocabulary that the rest of the volume uses — measurable spaces, measures, integration, products, and kernels, each law calculated on finite distributions before it is proved at the general signature — and then proves the exact correspondence between the two descriptions for the class of spaces where both make sense. The organizing object is the kernel: it is what a probabilistic program of one argument denotes, its bind operation is what sequencing denotes, and every law exported by this chapter is a law of kernels or of the integrals that define them. Conditioning is not in this chapter. Conditioning asks for a family of measures indexed by an observed value, determined only up to a null set of those values, and neither its construction nor its computability is settled by anything proved here.

Finite distributions, exactly

Definition 172.1 — Finite distribution ¶

Let $A$ be a set. A finite subdistribution on $A$ is a function $m : A \to Q \cap [0, 1]$ with finite support $supp (m) = {a ∣ m (a) > 0}$ and $| m | = \sum_{a} m (a) \leq 1$ ; it is a distribution when $| m | = 1$ . Write $δ_{a}$ for the distribution with $δ_{a} (a) = 1$ , and for a family $(m_{a})_{a \in A}$ of subdistributions on $B$ write $(m ≫ = k) (b) = \sum_{a \in supp (m)} m (a) k (a) (b) .$

Referenced from 4 locations

Probability, Measure, Kernels, and Computable Sampling

The fragment used throughout this section has terms $t : : = coin ∣ return v ∣ x \leftarrow t; t,$ where $v$ ranges over Boolean expressions in the bound variables. Its exact denotation is the finite subdistribution $E (t)$ defined by $\begin{matrix} E (coin) = {ff \mapsto \frac{1}{2}, tt \mapsto \frac{1}{2}}, \\ E (return v) = δ_{v}, \\ E (x \leftarrow t_{1}; t_{2}) = E (t_{1}) ≫ = (a \mapsto E (t_{2} [a / x])) . \end{matrix}$

Example 172.2 — The enumerated table ¶

For $xor 2$ , $\begin{aligned} E (xor 2) & \overset{b i n d}{=} \sum_{b_{1}} \frac{1}{2} (\sum_{b_{2}} \frac{1}{2} δ_{b_{1} \oplus b_{2}}) \\ = \frac{1}{4} (δ_{ff} + δ_{tt} + δ_{tt} + δ_{ff}) = {ff \mapsto \frac{1}{2}, tt \mapsto \frac{1}{2}} . \end{aligned}$ Every step is an exact rational computation; no approximation and no sampling occurs.

Referenced from 4 locations

Probability, Measure, Kernels, and Computable Sampling

Definition 172.3 — Bit-stream sampler for the fragment ¶

Let $u \in 2^{ω}$ . Define $S (t) (u)$ , a pair of a value and the unconsumed suffix of $u$ , by $\begin{matrix} S (coin) (b u^{'}) = (b, u^{'}), \\ S (return v) (u) = (v, u), \\ S (x \leftarrow t_{1}; t_{2}) (u) = S (t_{2} [a / x]) (u^{'}) where (a, u^{'}) = S (t_{1}) (u) . \end{matrix}$ The trace of a run is the sequence of events $draw b$ , one per consumed bit, followed by $return v$ .

Referenced from 3 locations

Probability, Measure, Kernels, and Computable Sampling

Example 172.4 — The executed trace ¶

On the stream beginning $0, 1$ the run of $xor 2$ is $draw 0$ ; $draw 1$ ; $return tt$ , because $S (coin) (0 1 u^{″}) = (0, 1 u^{″})$ , then $S (coin) (1 u^{″}) = (1, u^{″})$ , and $0 \oplus 1 = tt$ . On the stream beginning $1, 1$ the trace is $draw 1$ ; $draw 1$ ; $return ff$ .

Referenced from 2 locations

Probability, Measure, Kernels, and Computable Sampling

Proposition 172.5 — The two executions agree on the fragment ¶

For every term $t$ of the fragment there is $n \in N$ such that $S (t) (u)$ depends only on the first $n$ bits of $u$ , and for every value $v$ , $E (t) (v) = \frac{# {w \in 2^{n} ∣ S (t) (w u^{'}) returns v}}{2^{n}},$ the right-hand side being independent of the suffix $u^{'}$ .

Referenced from 6 locations

Probability, Measure, Kernels, and Computable Sampling

Proof of Proposition 172.5 — The two executions agree on the fragment

Proof. Induction on $t$ . For $coin$ , take $n = 1$ ; the two words $0$ and $1$ return $ff$ and $tt$ , giving $1 / 2$ each. For $return v$ , take $n = 0$ . For $x \leftarrow t_{1}; t_{2}$ , let $n_{1}$ work for $t_{1}$ and, for each value $a$ in the finite range of $t_{1}$ , let $n_{2} (a)$ work for $t_{2} [a / x]$ ; take $n = n_{1} + max_{a} n_{2} (a)$ . Splitting a word $w \in 2^{n}$ as $w_{1} w_{2}$ with $| w_{1} | = n_{1}$ , the run of the bind on $w$ first runs $t_{1}$ on $w_{1}$ , producing some $a$ , and then runs $t_{2} [a / x]$ on $w_{2}$ . Counting words by this decomposition, $\begin{aligned} \frac{# {w ∣ bind returns v}}{2^{n}} & = \sum_{a} \frac{# {w_{1} ∣ t_{1} returns a}}{2^{n_{1}}} \\ \cdot \frac{# {w_{2} ∣ t_{2} [a / x] returns v}}{2^{n - n_{1}}} \\ \overset{I H}{=} (E (t_{1}) ≫ = E (t_{2} [\cdot / x])) (v) . \end{aligned}$ The decomposition is legitimate because the run of $t_{2} [a / x]$ begins at the suffix left by $t_{1}$ , which is exactly $w_{2} u^{'}$ , and because $E (t_{1})$ is a distribution supported on the finitely many values $a$ . ◻

Proposition 172.5 is the whole sampler/measure correspondence in the one case where counting works. It fails to be a definition of anything beyond the fragment for two reasons: the count $2^{n}$ presupposes that a fixed finite number of bits suffices, and the sum over values presupposes countably many outcomes. A draw from the uniform distribution on $[0, 1]$ violates both. The rest of the chapter replaces counting by measure and integration, and only then returns to samplers.

Exercise 172.1 ¶

★☆☆ Compute $E (t)$ as an exact rational table for $t = (b \leftarrow coin; if b then coin else return ff),$ and give the trace of $S (t)$ on the stream beginning $1, 0$ .

Referenced from 2 locations

Probability, Measure, Kernels, and Computable Sampling

Exercise 172.2 ¶

★★☆ Give a term of a fragment extended by $while$ whose sampler consumes an unbounded number of bits with positive probability, and explain which step of the proof of proposition 172.5 fails for it.

Referenced from 2 locations

Probability, Measure, Kernels, and Computable Sampling

Measurable spaces and measures

Definition 172.6 — Measurable space and measurable map ¶

A $σ$ -algebra on a set $X$ is a family $Σ_{X} \subseteq P (X)$ containing $X$ and closed under complement and countable union. A measurable space is a pair $(X, Σ_{X})$ , written $X$ when the $σ$ -algebra is clear. A map $g : X \to Y$ is measurable when $g^{- 1} (B) \in Σ_{X}$ for every $B \in Σ_{Y}$ .

Referenced from 5 locations

Probability, Measure, Kernels, and Computable Sampling

Lemma 172.7 — Identity and composition ¶

The identity ${id}_{X}$ is measurable, and if $g : X \to Y$ and $h : Y \to Z$ are measurable then so is $h \circ g$ .

Referenced from 3 locations

Probability, Measure, Kernels, and Computable Sampling

Proof of Lemma 172.7 — Identity and composition

Proof. ${id}_{X}^{- 1} (A) = A$ . For the composite, $(h \circ g)^{- 1} (C) = g^{- 1} (h^{- 1} (C))$ , and $h^{- 1} (C) \in Σ_{Y}$ by measurability of $h$ , so its $g$ -preimage lies in $Σ_{X}$ . ◻

Lemma 172.8 — Measurability from a generating family ¶

Let $G \subseteq P (Y)$ and let $σ (G)$ be the least $σ$ -algebra containing $G$ , which exists because the intersection of any family of $σ$ -algebras is one. If $g^{- 1} (B) \in Σ_{X}$ for every $B \in G$ , then $g$ is measurable with respect to $σ (G)$ .

Referenced from 4 locations

Probability, Measure, Kernels, and Computable Sampling

Proof of Lemma 172.8 — Measurability from a generating family

Proof. The family ${B \subseteq Y ∣ g^{- 1} (B) \in Σ_{X}}$ contains $G$ and is a $σ$ -algebra, because preimage commutes with complement and countable union. Hence it contains $σ (G)$ . ◻

Three examples are used throughout. A countable set $A$ carries the discrete $σ$ -algebra $P (A)$ , and every map out of it is measurable. The real line carries the Borel $σ$ -algebra generated by the open intervals. Given $X$ and $Y$ , the product $X \times Y$ carries $Σ_{X} \otimes Σ_{Y} = σ ({A \times B ∣ A \in Σ_{X}, B \in Σ_{Y}})$ ; the two projections are measurable, and by lemma 172.8 a map $⟨ g, h ⟩$ into a product is measurable as soon as $g$ and $h$ are.

Definition 172.9 — Measure, subprobability, Dirac ¶

A measure on $X$ is a function $μ : Σ_{X} \to [0, \infty]$ with $μ (\emptyset) = 0$ that is countably additive: $μ (⋃_{n} A_{n}) = \sum_{n} μ (A_{n})$ for pairwise disjoint $A_{n}$ . It is a subprobability measure when $μ (X) \leq 1$ and a probability measure when $μ (X) = 1$ . For $x \in X$ the Dirac measure is $δ_{x} (A) = 1_{A} (x)$ , which is a probability measure.

Referenced from 4 locations

Probability, Measure, Kernels, and Computable Sampling

Definition 172.10 — Pushforward ¶

For measurable $g : X \to Y$ and a measure $μ$ on $X$ , define $g_{*} μ (B) = μ (g^{- 1} (B))$ .

Referenced from 3 locations

Probability, Measure, Kernels, and Computable Sampling

Lemma 172.11 — Pushforward is functorial ¶

$g_{*} μ$ is a measure, of the same total mass as $μ$ ; $({id}_{X})_{*} μ = μ$ ; and $(h \circ g)_{*} μ = h_{*} (g_{*} μ)$ .

Referenced from 4 locations

Proof of Lemma 172.11 — Pushforward is functorial

Proof. $g^{- 1}$ preserves $\emptyset$ , disjointness, and countable unions, so countable additivity transfers; $g_{*} μ (Y) = μ (g^{- 1} Y) = μ (X)$ . The two equations are ${id}^{- 1} (A) = A$ and $(h \circ g)^{- 1} (C) = g^{- 1} (h^{- 1} (C))$ . ◻

Convention 172.12 — The imported integration toolkit ¶

For a measurable $f : X \to [0, \infty]$ and a measure $μ$ , the integral is $\begin{aligned} \int f d μ = sup {\sum_{i = 1}^{k} c_{i} μ (A_{i}) | & k \in N, c_{i} \in [0, \infty), \\ A_{i} \in Σ_{X} disjoint, \sum_{i} c_{i} 1_{A_{i}} \leq f} . \end{aligned}$ The following four facts about this integral are imported from Tao, An Introduction to Measure Theory, at the stated signatures, and are used with no further appeal to the construction of the integral: additivity $\int (f + g) d μ = \int f d μ + \int g d μ$ and homogeneity $\int a f d μ = a \int f d μ$ for measurable $f, g : X \to [0, \infty]$ and $a \in [0, \infty)$ (Tao, §1.4); the monotone convergence theorem, that $\int lim_{n} f_{n} d μ = lim_{n} \int f_{n} d μ$ for a pointwise nondecreasing sequence of measurable $f_{n} : X \to [0, \infty]$ (Tao, Theorem 1.4.44); the existence and uniqueness of the product measure $μ \otimes ν$ on $Σ_{X} \otimes Σ_{Y}$ with $(μ \otimes ν) (A \times B) = μ (A) ν (B)$ for $σ$ -finite $μ, ν$ (Tao, §1.7); and Tonelli’s theorem, that for $σ$ -finite $μ, ν$ and measurable $f : X \times Y \to [0, \infty]$ the functions $x \mapsto \int f (x, y) d ν (y)$ and $y \mapsto \int f (x, y) d μ (x)$ are measurable and $\int f d (μ \otimes ν) = \int \int f (x, y) d ν (y) d μ (x) = \int \int f (x, y) d μ (x) d ν (y)$ (Tao, Theorem 1.7.15). Every subprobability measure is finite, hence $σ$ -finite, so the last two apply to all measures exported by this chapter. Monotonicity of the integral and the identity $\int 1_{A} d μ = μ (A)$ are immediate from the displayed definition and are proved below rather than imported.

Referenced from 14 locations

Lemma 172.13 — Monotonicity and indicators ¶

If $f \leq g$ pointwise then $\int f d μ \leq \int g d μ$ , and $\int 1_{A} d μ = μ (A)$ for $A \in Σ_{X}$ .

Referenced from 9 locations

Proof of Lemma 172.13 — Monotonicity and indicators

Proof. Every competitor $\sum_{i} c_{i} 1_{A_{i}} \leq f$ in the supremum defining $\int f d μ$ also satisfies $\sum_{i} c_{i} 1_{A_{i}} \leq g$ , so the supremum for $f$ is over a subset of the competitors for $g$ . For the indicator, the competitor $1 \cdot 1_{A}$ gives $μ (A) \leq \int 1_{A} d μ$ ; conversely any competitor $\sum_{i} c_{i} 1_{A_{i}} \leq 1_{A}$ has $c_{i} \leq 1$ and $A_{i} \subseteq A$ whenever $c_{i} > 0$ , so $\sum_{i} c_{i} μ (A_{i}) \leq μ (A)$ by additivity and monotonicity of $μ$ . ◻

Theorem 172.14 — Change of variables ¶

Let $g : X \to Y$ be measurable, $μ$ a measure on $X$ , and $f : Y \to [0, \infty]$ measurable. Then $\int f d (g_{*} μ) = \int (f \circ g) d μ .$

Referenced from 15 locations

Proof of Theorem 172.14 — Change of variables

Proof. The proof is the standard three-stage ascent, and each stage is used again in section 172.3.

Indicators. For $f = 1_{B}$ with $B \in Σ_{Y}$ , the composite $1_{B} \circ g$ is $1_{g^{- 1} (B)}$ , so $\begin{aligned} \int 1_{B} d (g_{*} μ) \overset{l e m m a 172.13}{=} g_{*} μ (B) \\ \overset{d e f i n i t i o n 172.10}{=} μ (g^{- 1} B) \\ \overset{l e m m a 172.13}{=} \int 1_{g^{- 1} B} d μ = \int (1_{B} \circ g) d μ . \end{aligned}$

Simple functions. For $f = \sum_{i = 1}^{k} c_{i} 1_{B_{i}}$ , apply additivity and homogeneity (convention 172.12) on both sides and the indicator case to each summand.

General $f$ . Every measurable $f : Y \to [0, \infty]$ is the pointwise limit of the nondecreasing sequence of simple functions $f_{n} = \sum_{j = 1}^{n 2^{n}} \frac{j - 1}{2^{n}} 1_{f^{- 1} [\frac{j - 1}{2^{n}}, \frac{j}{2^{n}})} + n 1_{f^{- 1} [n, \infty]},$ and $f_{n} \circ g$ is then a nondecreasing sequence of simple functions with pointwise limit $f \circ g$ . Monotone convergence applied on each side gives the claim from the simple case. ◻

Lemma 172.15 — Dirac and products ¶

For $x \in X$ and measurable $f : X \to [0, \infty]$ , $\int f d δ_{x} = f (x)$ ; for $x \in X$ , $y \in Y$ , $δ_{x} \otimes δ_{y} = δ_{(x, y)}$ ; and for a subprobability $μ$ on $X$ and the one-point probability space $1 = ({*}, {\emptyset, {*}})$ , the projection $π_{X}$ satisfies $(π_{X})_{*} (μ \otimes δ_{*}) = μ$ .

Referenced from 4 locations

Proof of Lemma 172.15 — Dirac and products

Proof. For the first claim, $\int 1_{A} d δ_{x} = δ_{x} (A) = 1_{A} (x)$ , and the ascent of theorem 172.14 carries this to simple and then to all measurable $f$ . For the second, the two measures agree on the generating rectangles, $(δ_{x} \otimes δ_{y}) (A \times B) = 1_{A} (x) 1_{B} (y) = 1_{A \times B} (x, y) = δ_{(x, y)} (A \times B)$ , and by the uniqueness clause of convention 172.12 agreement on rectangles determines the product measure. For the third, $(π_{X})_{*} (μ \otimes δ_{*}) (A) = (μ \otimes δ_{*}) (A \times {*}) = μ (A) \cdot 1$ . ◻

Exercise 172.3 ¶

★☆☆ Show that the family of finite and cofinite subsets of an uncountable set is not a $σ$ -algebra, and identify which clause of definition 172.6 fails.

Referenced from 2 locations

Probability, Measure, Kernels, and Computable Sampling

Exercise 172.4 ¶

★☆☆ Let $A, B$ be countable with the discrete $σ$ -algebras and let $g : A \to B$ . Show that $g_{*} μ ({b}) = \sum_{a \in g^{- 1} (b)} μ ({a})$ , and compute $g_{*} E (xor 2)$ for $g$ the negation map.

Referenced from 2 locations

Probability, Measure, Kernels, and Computable Sampling

Exercise 172.5 ¶

★★☆ Exhibit a set map $g : X \to Y$ that is not measurable and a measure $μ$ for which the formula of theorem 172.14 has an undefined left-hand side. State precisely which stage of the proof uses measurability of $g$ .

Referenced from 2 locations

Probability, Measure, Kernels, and Computable Sampling

Kernels and their monad laws

A closed probabilistic program of type $τ$ denotes a measure on $[[τ]]$ . A program with one free variable denotes a family of measures indexed by the value of that variable, and sequencing composes two such families. The composition is an integral, so the family must be measurable in its index; that requirement is the definition of a kernel.

Definition 172.16 — Kernel ¶

Let $X, Y$ be measurable spaces. A kernel $k : X ⇝ Y$ is a function assigning to each $x \in X$ a subprobability measure $k (x)$ on $Y$ such that $x \mapsto k (x) (B)$ is measurable for every $B \in Σ_{Y}$ . The return kernel is ${ret}_{X} (x) = δ_{x}$ , and for a subprobability measure $μ$ on $X$ and a kernel $k : X ⇝ Y$ the bind is $(μ ≫ = k) (B) = \int k (x) (B) d μ (x) (B \in Σ_{Y}) .$ For kernels $k : X ⇝ Y$ and $l : Y ⇝ Z$ , the composite is $(k ≫ = l) (x) = k (x) ≫ = l$ .

Referenced from 7 locations

Lemma 172.17 — The return kernel is a kernel ¶

${ret}_{X}$ is a kernel, and for measurable $g : X \to Y$ the assignment $x \mapsto δ_{g (x)}$ is a kernel.

Referenced from 3 locations

Probability, Measure, Kernels, and Computable Sampling

Proof of Lemma 172.17 — The return kernel is a kernel

Proof. $δ_{x} (B) = 1_{B} (x)$ is measurable in $x$ because $1_{B}^{- 1} ({1}) = B \in Σ_{X}$ . For the second claim, $δ_{g (x)} (B) = 1_{g^{- 1} (B)} (x)$ , and $g^{- 1} (B) \in Σ_{X}$ . ◻

Proposition 172.18 — Bind is well defined ¶

Let $μ$ be a subprobability measure on $X$ and $k : X ⇝ Y$ a kernel. Then $μ ≫ = k$ is a subprobability measure on $Y$ , with $(μ ≫ = k) (Y) \leq μ (X) \leq 1$ . If moreover $l : W ⇝ X$ is a kernel then $w \mapsto (l (w) ≫ = k) (B)$ is measurable, so $l ≫ = k$ is a kernel.

Referenced from 5 locations

Proof of Proposition 172.18 — Bind is well defined

Proof. Measure. $(μ ≫ = k) (\emptyset) = \int 0 d μ = 0$ . For pairwise disjoint $(B_{n})_{n}$ , countable additivity of each $k (x)$ gives $k (x) (⋃_{n} B_{n}) = \sum_{n} k (x) (B_{n}) = lim_{N} \sum_{n \leq N} k (x) (B_{n})$ , a pointwise nondecreasing limit of measurable functions of $x$ ; so $\begin{aligned} (μ ≫ = k) (⋃_{n} B_{n}) \\ \overset{m o n o t o n e c o n v e r g e n c e}{=} lim_{N} \int \sum_{n \leq N} k (x) (B_{n}) d μ (x) \\ \overset{a d d i t i v i t y}{=} lim_{N} \sum_{n \leq N} (μ ≫ = k) (B_{n}) = \sum_{n} (μ ≫ = k) (B_{n}) . \end{aligned}$ Mass. $k (x) (Y) \leq 1$ pointwise, so $(μ ≫ = k) (Y) \leq \int 1 d μ = μ (X)$ by lemma 172.13.

Measurability of the composite. Fix $B$ . The function $(w, x) \mapsto k (x) (B)$ is measurable in $x$ by assumption, and $w \mapsto \int k (x) (B) d l (w) (x)$ is measurable by the following instance of the three-stage ascent: for $k (\cdot) (B) = 1_{A}$ it is $w \mapsto l (w) (A)$ , measurable because $l$ is a kernel; for a simple function it is a finite nonnegative combination of such maps; and in general it is the pointwise limit of a nondecreasing sequence of those, hence measurable. ◻

Lemma 172.19 — Integration against a bind ¶

For a subprobability $μ$ on $X$ , a kernel $k : X ⇝ Y$ , and a measurable $f : Y \to [0, \infty]$ , $\int f d (μ ≫ = k) = \int (\int f d k (x)) d μ (x) .$

Referenced from 7 locations

Proof of Lemma 172.19 — Integration against a bind

Proof. For $f = 1_{B}$ both sides are $\int k (x) (B) d μ (x)$ , by lemma 172.13 on the left and inside the outer integral on the right. Additivity and homogeneity extend this to simple $f$ . For general $f$ , take the nondecreasing simple approximants $f_{n}$ of theorem 172.14; monotone convergence applies to the outer integral on the left, and on the right the inner integrals $\int f_{n} d k (x)$ form a nondecreasing sequence in $n$ for each $x$ , so monotone convergence applies twice. ◻

Theorem 172.20 — Monad laws for kernels ¶

Let $μ$ be a subprobability measure on $X$ , let $k : X ⇝ Y$ and $l : Y ⇝ Z$ be kernels, and let $x \in X$ . Then $\begin{matrix} δ_{x} ≫ = k = k (x), \\ μ ≫ = {ret}_{X} = μ, \\ (μ ≫ = k) ≫ = l = μ ≫ = (x \mapsto k (x) ≫ = l) . \end{matrix}$

Referenced from 9 locations

Proof of Theorem 172.20 — Monad laws for kernels

Proof. Each equation is an equality of measures, so it suffices to evaluate both sides at an arbitrary measurable set.

Left unit. $(δ_{x} ≫ = k) (B) = \int k (\cdot) (B) d δ_{x} \overset{l e m m a 172.15}{=} k (x) (B)$ .

Right unit. $(μ ≫ = {ret}_{X}) (A) = \int δ_{x} (A) d μ (x) = \int 1_{A} d μ \overset{l e m m a 172.13}{=} μ (A)$ .

Associativity. For $C \in Σ_{Z}$ , $\begin{aligned} ((μ ≫ = k) ≫ = l) (C) \\ \overset{d e f i n i t i o n 172.16}{=} \int l (y) (C) d (μ ≫ = k) (y) \\ \overset{l e m m a 172.19}{=} \int (\int l (y) (C) d k (x) (y)) d μ (x) \\ \overset{d e f i n i t i o n 172.16}{=} \int (k (x) ≫ = l) (C) d μ (x), \end{aligned}$ and the last expression is $(μ ≫ = (x \mapsto k (x) ≫ = l)) (C)$ ; the family $x \mapsto k (x) ≫ = l$ is a kernel by proposition 172.18, so the outer integral is defined. ◻

Example 172.21 — The laws on the finite fragment ¶

On a countable space with the discrete $σ$ -algebra, a subprobability measure is a family $(μ ({a}))_{a}$ summing to at most $1$ , the integral is the sum $\int f d μ = \sum_{a} f (a) μ ({a})$ , and bind is the operation of definition 172.1. Associativity becomes the interchange $\sum_{y} (\sum_{x} μ (x) k (x) (y)) l (y) (z) = \sum_{x} μ (x) (\sum_{y} k (x) (y) l (y) (z)),$ which is Tonelli’s theorem for counting measure. The general proof above is the same computation with sums replaced by integrals; the finite case is where the reader should first check the bracketing.

Referenced from 3 locations

Lemma 172.22 — Pushforward as a bind, and the mass bound ¶

For measurable $g : X \to Y$ and a subprobability $μ$ on $X$ , $g_{*} μ = μ ≫ = (x \mapsto δ_{g (x)})$ . Consequently $(μ ≫ = k) (Y) = μ (X)$ whenever every $k (x)$ is a probability measure, and the total mass of a bind is otherwise strictly smaller.

Referenced from 5 locations

Proof of Lemma 172.22 — Pushforward as a bind, and the mass bound

Proof. $(μ ≫ = (x \mapsto δ_{g (x)})) (B) = \int 1_{g^{- 1} (B)} d μ = μ (g^{- 1} B) = g_{*} μ (B)$ . For the mass, if $k (x) (Y) = 1$ for all $x$ then $\int k (x) (Y) d μ (x) = μ (X)$ ; and if $k (x) (Y) < 1$ on a set of positive $μ$ -measure then monotonicity of the integral makes the value strictly smaller. ◻

Limits of subprobability measures

Recursive programs are interpreted as suprema of the finite unfoldings of their bodies, so the exported interface must say that such suprema exist and that sequencing preserves them.

Definition 172.23 — Pointwise order ¶

For subprobability measures $μ, ν$ on $X$ write $μ \leq ν$ when $μ (A) \leq ν (A)$ for every $A \in Σ_{X}$ .

Referenced from 4 locations

Probability, Measure, Kernels, and Computable Sampling

Proposition 172.24 — Increasing chains ¶

Let $μ_{0} \leq μ_{1} \leq \dots$ be subprobability measures on $X$ . Then $A \mapsto sup_{n} μ_{n} (A)$ is a subprobability measure, written $sup_{n} μ_{n}$ , it is the least upper bound of the chain in the order of definition 172.23, and for every measurable $f : X \to [0, \infty]$ , $\int f d (sup_{n} μ_{n}) = sup_{n} \int f d μ_{n}$ .

Referenced from 10 locations

Proof of Proposition 172.24 — Increasing chains

Proof. Write $μ (A) = sup_{n} μ_{n} (A) \leq 1$ . Then $μ (\emptyset) = 0$ , and for pairwise disjoint $(A_{k})_{k}$ , $\begin{aligned} μ (⋃_{k} A_{k}) = sup_{n} \sum_{k} μ_{n} (A_{k}) \\ \overset{m o n o t o n e c o n v e r g e n c e f o r s e r i e s}{=} \sum_{k} sup_{n} μ_{n} (A_{k}) \\ = \sum_{k} μ (A_{k}), \end{aligned}$ the middle step because the double family $μ_{n} (A_{k})$ is nondecreasing in $n$ for each $k$ , so the supremum over $n$ of the sums equals the sum of the suprema. That $μ$ is the least upper bound is immediate from the pointwise definition. For the integral, both sides are suprema of the same set of numbers when $f$ is an indicator, additivity extends this to simple functions, and the approximants of theorem 172.14 together with monotone convergence give the general case. ◻

Proposition 172.25 — Bind preserves increasing suprema ¶

Let $μ_{0} \leq μ_{1} \leq \dots$ be subprobability measures on $X$ , let $k : X ⇝ Y$ be a kernel, and let $k_{0} \leq k_{1} \leq \dots$ be kernels with $k_{m} (x)$ increasing in $m$ for each $x$ . Then $\begin{matrix} (sup_{n} μ_{n}) ≫ = k = sup_{n} (μ_{n} ≫ = k), \\ μ ≫ = (sup_{m} k_{m}) = sup_{m} (μ ≫ = k_{m}) . \end{matrix}$

Referenced from 6 locations

Proof of Proposition 172.25 — Bind preserves increasing suprema

Proof. For the first, evaluate at $B$ and apply proposition 172.24 to the function $x \mapsto k (x) (B)$ . For the second, evaluate at $B$ ; the integrands $x \mapsto k_{m} (x) (B)$ form a pointwise nondecreasing sequence whose supremum is a subprobability measure in $B$ by proposition 172.24 and is measurable in $x$ as a pointwise supremum of measurable functions; monotone convergence gives the equality. ◻

Example 172.26 — Expectation of a finite rational mixture ¶

Let $μ = \sum_{i = 1}^{k} p_{i} μ_{i}$ with rational $p_{i} \geq 0$ , $\sum_{i} p_{i} \leq 1$ , and subprobability measures $μ_{i}$ . Then $μ$ is a subprobability measure and $\int f d μ = \sum_{i} p_{i} \int f d μ_{i}$ for measurable $f \geq 0$ : both claims hold for indicators by definition, and extend by additivity, homogeneity and monotone convergence. For $E (xor 2)$ of example 172.2 and $f = 1_{{tt}}$ this reads $\int f d E (xor 2) = 1 / 2$ .

Referenced from 10 locations

Convention 172.27 — The frozen export PMKPMK ¶

The interface exported by this chapter to later chapters consists of exactly the following, in three groups.

$PMK$ -map: definition 172.6, definition 172.9, definition 172.10; lemma 172.7, lemma 172.8, lemma 172.11; theorem 172.14; lemma 172.15; the product measure and Tonelli statements of convention 172.12.

$PMK$ -bind: definition 172.16; lemma 172.17; proposition 172.18; lemma 172.19; theorem 172.20; lemma 172.22.

$PMK$ -lim: lemma 172.13; the additivity, homogeneity and monotone convergence statements of convention 172.12; definition 172.23; proposition 172.24; proposition 172.25; example 172.26.

Nothing else is exported. In particular the export contains no conditioning or disintegration theorem, no computable metric space structure, no effective topology, no density or Radon–Nikodym statement, no s-finite kernel, no quasi-Borel exponential, and no domain-theoretic fixed point. The sampler-and-valuation development of section 172.5 is a separate system card and is not part of $PMK$ .

Referenced from 9 locations

Exercise 172.6 ¶

★★☆ Give a family $(k (x))_{x \in R}$ of probability measures on ${0, 1}$ that is not a kernel, and show that $μ ≫ = k$ is then undefined for Lebesgue measure restricted to $[0, 1]$ . (Use a non-measurable subset of $[0, 1]$ as the set on which $k (x) = δ_{1}$ .)

Referenced from 2 locations

Probability, Measure, Kernels, and Computable Sampling

Exercise 172.7 ¶

★☆☆ Verify the associativity law of theorem 172.20 by direct computation on the three-point discrete example $μ = {a \mapsto 1 / 3, b \mapsto 2 / 3}$ , $k (a) = {c \mapsto 1}$ , $k (b) = {c \mapsto 1 / 2, d \mapsto 1 / 2}$ , $l (c) = δ_{0}$ , $l (d) = δ_{1}$ .

Referenced from 2 locations

Probability, Measure, Kernels, and Computable Sampling

Exercise 172.8 ¶

★★☆ Give an increasing chain of subprobability measures on $N$ whose supremum has total mass $1 / 2$ although each member has mass strictly less than $1 / 2$ , and compute $\int f d (sup_{n} μ_{n})$ for $f (n) = n$ . State which hypothesis of proposition 172.24 would fail for a chain that is not nondecreasing.

Referenced from 2 locations

Probability, Measure, Kernels, and Computable Sampling

Samplers, valuations, and computable distributions

The finite fragment of section 172.1 had two descriptions and one proof relating them. For distributions on a complete separable metric space the two descriptions are a point of a space of measures and a program that consumes fair bits. This section states both precisely, proves the correspondence that the chapter owns, and marks exactly where the imported computability result is used.

Definition 172.28 — The fair-bit measure and its splitting ¶

Let $2^{ω}$ carry the $σ$ -algebra generated by the cylinders $[w] = {u ∣ u begins with w}$ for $w \in 2^{*}$ . The fair-bit measure $μ_{iid}$ is the unique measure with $μ_{iid} ([w]) = 2^{- | w |}$ . Define $split : 2^{ω} \to 2^{ω} \times 2^{ω}$ by $split (u) = (u_{e}, u_{o})$ , the subsequences of even and odd indices.

Referenced from 2 locations

Probability, Measure, Kernels, and Computable Sampling

Lemma 172.29 — Uniqueness on a generating algebra ¶

Let $μ, ν$ be subprobability measures on $X$ that agree on a Boolean algebra $A \subseteq Σ_{X}$ with $σ (A) = Σ_{X}$ and $μ (X) = ν (X)$ . Then $μ = ν$ .

Referenced from 6 locations

Proof of Lemma 172.29 — Uniqueness on a generating algebra

Proof. Let $C = {A \in Σ_{X} ∣ μ (A) = ν (A)}$ . It contains $A$ . It is closed under increasing unions, because $μ (⋃_{n} A_{n}) = sup_{n} μ (A_{n})$ for an increasing sequence, by countable additivity applied to the disjoint differences; and under decreasing intersections, because $μ (X) < \infty$ allows the same computation on complements. So $C$ is a monotone class containing $A$ , and by the monotone class lemma (Tao, Lemma 1.7.14) it contains $σ (A) = Σ_{X}$ . ◻

Lemma 172.30 — Splitting produces an independent pair ¶

${split}_{*} μ_{iid} = μ_{iid} \otimes μ_{iid}$ .

Referenced from 4 locations

Probability, Measure, Kernels, and Computable Sampling

Proof of Lemma 172.30 — Splitting produces an independent pair

Proof. Both sides are probability measures on $2^{ω} \times 2^{ω}$ . On a rectangle of cylinders, ${split}^{- 1} ([w_{1}] \times [w_{2}])$ is the set of streams whose even positions begin with $w_{1}$ and whose odd positions begin with $w_{2}$ ; this is the disjoint union of the cylinders $[w]$ of length $2 max (| w_{1} |, | w_{2} |)$ that meet those constraints, and counting them gives $μ_{iid} ({split}^{- 1} ([w_{1}] \times [w_{2}])) = 2^{- | w_{1} |} 2^{- | w_{2} |} = (μ_{iid} \otimes μ_{iid}) ([w_{1}] \times [w_{2}]) .$ Finite unions of such rectangles form a Boolean algebra generating the product $σ$ -algebra, and the two measures agree on it by finite additivity, so lemma 172.29 applies. ◻

Definition 172.31 — Sampler and its pushforward measure ¶

Let $X$ be a measurable space. A sampler for $X$ is a measurable partial function $s : 2^{ω} ⇀ X$ whose domain has $μ_{iid}$ -measure $1$ . Its pushforward measure is $psh (s) = s_{*} μ_{iid}$ , a probability measure on $X$ . The constant sampler is $\det (x) (u) = x$ , and for a sampler $s$ for $X$ and a family $f$ assigning to each $x \in X$ a sampler $f (x)$ for $Y$ , the sequenced sampler is $samp (s, f) (u) = f (s (u_{e})) (u_{o}) .$

Referenced from 5 locations

Probability, Measure, Kernels, and Computable Sampling

Theorem 172.32 — Pushforward correspondence ¶

Let $s$ be a sampler for $X$ and let $f$ assign to each $x \in X$ a sampler $f (x)$ for $Y$ such that $(x, u) \mapsto f (x) (u)$ is measurable on its domain and $x \mapsto psh (f (x)) (B)$ is measurable for every $B \in Σ_{Y}$ . Then $psh (\det (x)) = δ_{x}, psh (samp (s, f)) = psh (s) ≫ = (x \mapsto psh (f (x))) .$

Referenced from 8 locations

Probability, Measure, Kernels, and Computable Sampling

Proof of Theorem 172.32 — Pushforward correspondence

Proof. For the first equation, $psh (\det (x)) (A) = μ_{iid} ({u ∣ x \in A}) = 1_{A} (x) = δ_{x} (A)$ .

For the second, fix $B \in Σ_{Y}$ and compute $\begin{aligned} psh (samp (s, f)) (B) & \overset{d e f i n i t i o n 172.31}{=} μ_{iid} ({u ∣ f (s (u_{e})) (u_{o}) \in B}) \\ \overset{l e m m a 172.30}{=} (μ_{iid} \otimes μ_{iid}) ({(u_{1}, u_{2}) ∣ f (s (u_{1})) (u_{2}) \in B}) \\ \overset{T o n e l l i}{=} \int \int 1_{B} (f (s (u_{1})) (u_{2})) d μ_{iid} (u_{2}) d μ_{iid} (u_{1}) \\ \overset{d e f i n i t i o n 172.31}{=} \int psh (f (s (u_{1}))) (B) d μ_{iid} (u_{1}) \\ \overset{t h e o r e m 172.14}{=} \int psh (f (x)) (B) d psh (s) (x) \\ \overset{d e f i n i t i o n 172.16}{=} (psh (s) ≫ = (x \mapsto psh (f (x)))) (B) . \end{aligned}$ The second step uses lemma 172.30 through theorem 172.14 applied to the measurable map $split$ ; Tonelli applies because both measures are probability measures, hence $σ$ -finite, and because the displayed set is measurable by the hypothesis on $f$ . The last change of variables is theorem 172.14 for the measurable $s$ and the function $x \mapsto psh (f (x)) (B)$ , measurable by hypothesis. Both sides are defined off a $μ_{iid}$ -null set, which does not affect any of the integrals. ◻

Remark 172.33 — What thm:pmk-push is, and is not ¶

Theorem 172.32 is the measure-theoretic content of Huang–Morrisett–Spitters’ Proposition 5.1, restated in the vocabulary of convention 172.27 and proved here: the pushforward of a constant sampler is a Dirac measure, and the pushforward of a sequenced sampler is the bind of the pushforwards. Their statement is about topological domains — for countably based topological predomains $D, E$ , ${psh}_{D}$ is a continuous map $S (D) \Rightarrow P (D)$ into valuations, and the second clause is proved for their $samp$ , whose splitting must produce an independent stream — and the independence requirement is exactly lemma 172.30. It is a correspondence between two representations of the same distribution. It is not an operational adequacy theorem: it compares two denotations, and says nothing about the traces of a running implementation. A statement about traces belongs to proposition 172.5 and to the practical project below, both of which are confined to the finite fragment.

Referenced from 2 locations

Probability, Measure, Kernels, and Computable Sampling

Convention 172.34 — The Huang–Morrisett–Spitters system card ¶

The following interface is frozen and is not part of $PMK$ . A computable metric space is a triple $(X, d, S)$ with $(X, d)$ a complete metric space, $S \subseteq X$ countable, enumerable and dense, and $d (s_{i}, s_{j})$ a computable real uniformly in $i, j$ . The space $M (X)$ of Borel probability measures on $X$ , equipped with the Prokhorov metric $d_{ρ} (μ, ν) = inf {ε > 0 ∣ μ (A) \leq ν (A^{ε}) + ε for all Borel A}$ and the ideal points $D (S)$ of finitely supported rational-mass distributions on $S$ , is again a computable metric space; $μ$ is a computable distribution when it is a computable point of it. A distribution $μ \in M (X)$ is samplable when there is a computable $s : (2^{ω}, μ_{iid}) ⇀ (X, μ)$ , computable on a domain of full measure, with $μ = s_{*} μ_{iid}$ . The language $λ_{C D}$ has types $τ : : = Nat ∣ Real ∣ τ ⟶ τ ∣ τ \times τ ∣ Dist τ$ , a judgment $⊢_{D} τ$ admitting $Nat$ , $Real$ and products of admissible types, PCF terms with pairs, real constants and primitive real operations, primitive distributions $dist$ , $return M$ and $x \leftarrow M_{1}; M_{2}$ , and the typing rules

Ψ (dist) = Dist τ

⊢_{D} τ

Γ ⊢ dist : Dist τ

Dist

Γ ⊢ M : τ

⊢_{D} τ

Γ ⊢ return M : Dist τ

Ret

Γ ⊢ M_{1} : Dist τ_{1}

Γ, x : τ_{1} ⊢ M_{2} : Dist τ_{2}

⊢_{D} τ_{1}, τ_{2}

Γ ⊢ x \leftarrow M_{1}; M_{2} : Dist τ_{2}

Bind

Types denote topological domains, with $[[Dist τ]] = {(s, {psh}_{[[τ]]} (s)) ∣ s \in S ([[τ]])}$ for the sampler functor $S (D) = 2^{ω} \Rightarrow D_{⟂}$ ; a valuation on a topological space is a strict, monotone and modular map $O (X) \to [0, 1]$ , it is $ω$ -continuous when it preserves suprema of increasing sequences of opens, and $P$ is the resulting probability monad with $η (x) (U) = 1_{U} (x)$ and $(μ ⪰^{♭} f) (U) = \int f_{U} d μ$ .

Referenced from 5 locations

Probability, Measure, Kernels, and Computable Sampling

Convention 172.35 — Imported computability and well-definedness ¶

Two statements of convention 172.34 are imported at exactly their source signatures and are used nowhere else in this book without being restated.

First, Huang–Morrisett–Spitters’ Proposition 2.11, attributed there to Freer and Roy (2010, Lemmas 2 and 3): a distribution $μ \in M (X)$ on a computable metric space $(X, d, S)$ is computable if and only if it is samplable. What it supplies is the passage between the two descriptions of a distribution on a complete separable metric space, in both directions, and nothing about conditioning.

Second, their Proposition 5.2: for every well-typed $Γ ⊢ M : τ$ of $λ_{C D}$ and every global environment with $Ψ ⊢ Υ$ , the expression denotation $[[M {]]}_{Γ}$ is a well-defined morphism $[[Γ]] \Rightarrow [[τ]]$ of topological domains. Its interesting cases are $return$ and bind, where the sampler component must be shown to realize the valuation component; that is exactly the content of theorem 172.32, transported to their setting.

Referenced from 4 locations

Probability, Measure, Kernels, and Computable Sampling

Example 172.36 — Uniform draws are computable, and the correspondence is not free ¶

The bisection sampler $unif (u) = lim_{n} bisect (u, n)$ , which maintains an interval and halves it according to the next bit, is a sampler for $[0, 1]$ in the sense of definition 172.31, and $psh (unif)$ is Lebesgue measure on $[0, 1]$ : on a dyadic interval $[j 2^{- n}, (j + 1) 2^{- n}]$ the preimage is a single cylinder of length $n$ , of measure $2^{- n}$ , and lemma 172.29 extends the agreement from the algebra generated by dyadic intervals to all Borel sets. By convention 172.35 the same distribution is a computable point of $(M ([0, 1]), d_{ρ}, D (Q))$ . Neither description follows from the other by unfolding definitions: the first is a statement about a measurable map on $2^{ω}$ , the second about a computable Cauchy sequence in the Prokhorov metric, and Proposition 2.11 is the theorem that they coincide.

Referenced from 2 locations

Probability, Measure, Kernels, and Computable Sampling

Remark 172.37 — Two representations, compared by translations ¶

Three descriptions of a distribution have appeared: a subprobability measure (definition 172.9), an $ω$ -continuous valuation (convention 172.34), and a sampler (definition 172.31). They are related by explicit translations and are not identified: a Borel measure restricts to an $ω$ -continuous valuation on the open sets, and is determined by that restriction when the space is countably based, by lemma 172.29 applied to the algebra generated by a countable base; a sampler maps to a measure by $psh$ ; and convention 172.35 maps a computable distribution back to a sampler. Each translation has hypotheses — countable base, completeness, computability of the metric — and a claim proved for one representation transfers to another only through a translation whose hypotheses have been checked. Park’s typed language for probabilistic computation is used in this book only as a pedagogical comparison for the sampling view; it owns no theorem here, and no statement crosses from its syntax to convention 172.34 without a proved translation.

Referenced from 2 locations

Probability, Measure, Kernels, and Computable Sampling

Remark 172.38 — The chapter's boundary ¶

Nothing above conditions on an observation. Conditioning asks for a family $x \mapsto μ (\cdot ∣ Y = x)$ satisfying an integral equation, and such a family is determined only up to a null set of $x$ ; both its existence and its computability are outside this chapter, and neither follows from the exported interface. Densities and Radon–Nikodym derivatives are likewise absent: no statement above produces a density for a measure, and the export contains none. Finally, definition 172.6 provides no function space: there is no measurable structure here on the maps between two measurable spaces, and the chapter proves nothing about higher-order probabilistic programs.

Referenced from 2 locations

Probability, Measure, Kernels, and Computable Sampling

Exercise 172.9 ¶

★☆☆ Write a sampler for the geometric distribution $n \mapsto 2^{- (n + 1)}$ on $N$ and compute $psh$ of it directly from definition 172.31, using cylinders.

Referenced from 3 locations

Probability, Measure, Kernels, and Computable Sampling

Exercise 172.10 ¶

★★☆ Replace $samp (s, f) (u) = f (s (u_{e})) (u_{o})$ by $f (s (u)) (u)$ , which feeds the same stream to both stages. Exhibit a sampler $s$ and a family $f$ for which the conclusion of theorem 172.32 then fails, and identify the step of the proof that breaks.

Referenced from 2 locations

Probability, Measure, Kernels, and Computable Sampling

Exercise 172.11 ¶

★★☆ Let $X$ be a countable discrete space. Show that every $ω$ -continuous valuation on $X$ with $ν (X) \leq 1$ is the restriction of a unique subprobability measure, and give the two directions of the translation explicitly.

Referenced from 2 locations

Probability, Measure, Kernels, and Computable Sampling

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 172.12, then exercise 172.13, then the practical project exercise 172.16.

Exercise 172.12 ¶

★☆☆ Verify the three laws of theorem 172.20 on the discrete two-point space by direct rational computation, and then locate in the general proof the exact step that replaces each finite sum.

Referenced from 3 locations

Probability, Measure, Kernels, and Computable Sampling

Exercise 172.13 ¶

★★☆ Write out the proof of theorem 172.32 for $X = Y = {0, 1}$ with $s$ reading one bit and $f (x)$ reading one bit, replacing every integral by a finite sum, and check the result against example 172.2.

Referenced from 3 locations

Probability, Measure, Kernels, and Computable Sampling

Exercise 172.14 ¶

★★☆ Give two subprobability measures and a nonnegative function for which the iterated integrals of convention 172.12 differ when the $σ$ -finiteness hypothesis is dropped, and state where theorem 172.32 would use the hypothesis.

Referenced from 2 locations

Probability, Measure, Kernels, and Computable Sampling

Exercise 172.15 ¶

★★☆ Let $k_{m}$ be the kernel on $N$ that halts within $m$ steps in the geometric program of exercise 172.9 and returns the empty measure otherwise. Prove that $(k_{m})_{m}$ is an increasing chain of kernels, compute $sup_{m} k_{m}$ , and check proposition 172.25 on this chain with $k (n) = δ_{n + 1}$ .

Referenced from 2 locations

Probability, Measure, Kernels, and Computable Sampling

Exercise 172.16 ¶

★★★ Practical project.pmk-enumerator-sampler Build an interpreter with two back ends for the fragment of section 172.1 extended with $xor$ , $if$ , and biased $coin (p)$ for reduced rational $p$ . The first back end is the exact enumerator $E$ of definition 172.1: it returns a finite map from values to reduced rationals, computed by the bind of that definition. The second is the bit-stream sampler $S$ of definition 172.3: it consumes an explicit finite list of bits and emits one trace line per event, $draw b$ or $return v$ , reporting exhaustion of the list as a distinct outcome from a returned value.

The invariant to maintain is that the enumerator’s table has total mass exactly $1$ for every term of the fragment and that every rational is kept in reduced form with no floating-point arithmetic anywhere; the sampler must consume exactly one bit per $coin$ , in evaluation order.

The concrete result is the pair of outputs for the fixture $xor 2 = b_{1} \leftarrow coin; b_{2} \leftarrow coin; return (b_{1} \oplus b_{2})$ . The acceptance test is decidable: the enumerator must print the table ${ff \mapsto 1 / 2, tt \mapsto 1 / 2}$ ; the sampler on the bit list $0, 1$ must print exactly $draw 0$ ; $draw 1$ ; $return tt$ , and on $1, 1$ exactly $draw 1$ ; $draw 1$ ; $return ff$ ; the enumerator must print ${ff \mapsto 2 / 3, tt \mapsto 1 / 3}$ for $b \leftarrow coin (1 / 3); return b$ with $tt$ the outcome of probability $1 / 3$ ; and the checker must confirm, by exhausting the four bit lists of length two, the equality of proposition 172.5 for $xor 2$ . Observed frequencies from repeated sampling may be displayed but are not an accepted answer, and the finite agreement checked here illustrates theorem 172.32 without proving it.

Referenced from 3 locations