Chapter 175Optional

Inference as Semantics-Preserving Program Transformation

Prerequisites. Direct starred prerequisites: chapter 174. No later core chapter depends on this route.

Take the model $obs = H \leftarrow coin (1 / 2); score (if H then 3 else 1); return H .$ Its unnormalized meaning is the finite measure ${tt \mapsto 3 / 2, ff \mapsto 1 / 2}$ , of total mass $2$ , and its posterior is ${tt \mapsto 3 / 4, ff \mapsto 1 / 4}$ .

Now run an inference procedure on it. Draw two particles from the prior, weigh them by the score, and resample: with luck both particles are $tt$ , and the procedure reports $tt$ with frequency $1$ . With other luck it reports $3 / 4$ . The output is a random object, and no single run refutes or confirms anything. The question the chapter answers is not whether a run looks plausible but whether the procedure, as a transformation of representations, preserves the measure that the model denotes.

The obstruction is that the object preserved is not the one the procedure manipulates. A procedure manipulates particles, weights, and suspended computations; the model denotes a measure. A correctness statement must therefore say what measure a pile of weighted particles means, and then require every step of the procedure to leave that measure unchanged. Once meaning is a function from representations to measures, correctness becomes an equation that composes, and a large algorithm becomes a composite of small steps each of which satisfies it. This chapter builds the meaning functions, proves the equation for each step of a sequential Monte Carlo algorithm, and assembles them.

Convention 175.1 — Imported interface and what is not imported ¶

From chapter 174 this chapter uses the quasi-Borel category, its cartesian closed structure (proposition 174.8, proposition 174.10), and the probability monad $P$ with its laws (theorem 174.16, proposition 174.17); through it, the kernel interface $PMK$ -bind of convention 172.27. No theorem about SFPC, its operational semantics, or the statistical powerdomain $T$ of convention 174.20 is used or transported: the system of this chapter is Ścibior et al.’s inference representations, a separate card, and no statement crosses between the two without a proved translation. The measures manipulated here are unnormalized finite measures, not probability measures, because scoring changes total mass.

Referenced from 2 locations

Inference as Semantics-Preserving Program Transformation

What a representation must mean

Definition 175.2 — Mass functions ¶

For a countable set $X$ let $Mass X$ be the set of finitely supported functions $X \to R^{+}$ , the finite measures with finite support. Its operations are $\begin{matrix} {return}^{Mass} x = δ_{x}, \\ (m ≫ =^{Mass} f) (y) = \sum_{x} m (x) f (x) (y), \\ {flip}^{Mass} = {ff \mapsto \frac{1}{2}, tt \mapsto \frac{1}{2}}, \\ {score}^{Mass} (r) = r \cdot δ_{*} . \end{matrix}$ The total mass is $| m | = \sum_{x} m (x)$ .

Referenced from 4 locations

Inference as Semantics-Preserving Program Transformation

The three monad laws for $Mass$ are the discrete instance of theorem 172.20, with the counting measure in place of a general measure and finite sums in place of integrals; example 172.21 carried out the identification.

Example 175.3 — The model's meaning, computed once ¶

Reading $obs$ through definition 175.2, $\begin{aligned} [[obs]] \\ = {flip}^{Mass} ≫ = λ H . ({score}^{Mass} (if H then 3 else 1) ≫ = λ * . δ_{H}) \\ = \frac{1}{2} \cdot 3 δ_{tt} + \frac{1}{2} \cdot 1 δ_{ff} \\ = {tt \mapsto \frac{3}{2}, ff \mapsto \frac{1}{2}} . \end{aligned}$ Total mass $2$ ; normalizing gives ${tt \mapsto 3 / 4, ff \mapsto 1 / 4}$ . Every claim below about an inference procedure applied to $obs$ is checked against these three exact rationals.

Referenced from 7 locations

Inference as Semantics-Preserving Program Transformation

Definition 175.4 — Inference representation ¶

A discrete inference representation is a sextuple $T = (T, {return}^{T}, ≫ =^{T}, {flip}^{T}, {score}^{T}, m^{T})$ consisting of a monadic interface $(T, {return}^{T}, ≫ =^{T})$ on sets, elements ${flip}^{T} \in T 2$ and ${score}^{T} : R^{+} \to T 1$ , and a family of meaning functions $m_{X}^{T} : T X \to Mass X$ such that for all $x \in X$ , $a \in T X$ , $r \in R^{+}$ and $f : X \to T Y$ , $\begin{matrix} m^{T} ({return}^{T} x) = δ_{x}, \\ m^{T} (a ≫ =^{T} f) = m^{T} (a) ≫ =^{Mass} λ x . m^{T} (f x), \\ m^{T} ({flip}^{T}) = {flip}^{Mass}, \\ m^{T} ({score}^{T} r) = r \cdot δ_{*} . \end{matrix}$ The monadic interface is not required to satisfy the monad laws, and $m^{T}$ is not required to be natural.

Referenced from 6 locations

Inference as Semantics-Preserving Program Transformation

Example 175.5 — Enumeration ¶

Let $Enum X = List (R^{+} \times X)$ , with $\begin{matrix} return x = [(1, x)], \\ a s ≫ = f = concat [scale (r, f x) ∣ (r, x) \in a s], \\ flip = [(\frac{1}{2}, ff), (\frac{1}{2}, tt)], \\ score r = [(r, *)], \end{matrix}$ where $scale (r, b s)$ multiplies every weight in $b s$ by $r$ , and $m^{Enum} (a s) (x) = \sum {r ∣ (r, x) \in a s}$ . The four laws hold. For $return$ and $flip$ and $score$ read the definitions. For bind, first note $m (scale (r, b s)) = r \cdot m (b s)$ , by summing the scaled weights, and then $\begin{aligned} m (a s ≫ = f) (y) \\ \overset{d e f i n i t i o n}{=} \sum_{(r, x) \in a s} m (scale (r, f x)) (y) \\ \overset{s c a l i n g}{=} \sum_{(r, x) \in a s} r \cdot m (f x) (y) \\ \overset{d e f i n i t i o n 175.2}{=} (m (a s) ≫ =^{Mass} λ x . m (f x)) (y), \end{aligned}$ the last step because the inner sum groups the elements of $a s$ by their value component, which is exactly what $m (a s)$ records.

Referenced from 2 locations

Inference as Semantics-Preserving Program Transformation

Example 175.6 — Weighted sampler terms ¶

Let $Term X$ be the binary trees generated by $Return (r, x)$ with $r \in R^{+}$ and $Flip (t_{ff}, t_{tt})$ . Put $\begin{matrix} return x = Return (1, x), score r = Return (r, *), \\ flip = Flip (Return (1, ff), Return (1, tt)), \end{matrix}$ and let $t ≫ = f$ graft $scale (r, f x)$ at each leaf $Return (r, x)$ . The meaning function is $\begin{matrix} m (Return (r, x)) = r \cdot δ_{x}, \\ m (Flip (t_{0}, t_{1})) = \frac{1}{2} m (t_{0}) + \frac{1}{2} m (t_{1}) . \end{matrix}$ The bind law is proved by structural induction on $t$ , using the auxiliary equation $m (scale (r, t)) = r \cdot m (t)$ , itself an induction: at a leaf it is the definition, and at a node it is the linearity of the half-sum. At a leaf, $m (Return (r, x) ≫ = f) = m (scale (r, f x)) = r \cdot m (f x) = (r δ_{x}) ≫ =^{Mass} λ x . m (f x)$ ; at a node, both sides split into halves and the induction hypothesis applies to each.

Referenced from 3 locations

Inference as Semantics-Preserving Program Transformation

Definition 175.7 — Inference transformation ¶

Let $T$ and $S$ be inference representations. A discrete inference transformation $t : T \to S$ assigns to each set $X$ a function $t_{X} : T X \to S X$ with $m^{T} (a) = m^{S} (t_{X} (a)) for every a \in T X .$

Referenced from 5 locations

Inference as Semantics-Preserving Program Transformation

Lemma 175.8 — Transformations compose ¶

Identities are inference transformations, and if $t : T \to S$ and $u : S \to U$ are inference transformations then so is $x \mapsto u_{X} (t_{X} (x))$ .

Referenced from 3 locations

Inference as Semantics-Preserving Program Transformation

Proof of Lemma 175.8 — Transformations compose

Proof. $m^{T} (a) = m^{S} (t_{X} a) = m^{U} (u_{X} (t_{X} a))$ . ◻

Example 175.9 — Aggregation, and a transformation that is not natural ¶

Let ${aggr}_{X}$ merge list entries with equal value components by summing their weights. Then $m^{Enum} ({aggr}_{X} (a s)) = m^{Enum} (a s)$ , by induction on $a s$ : merging two entries $(r, x)$ and $(s, x)$ into $(r + s, x)$ changes no value of the mass function. So $aggr$ is an inference transformation. It is not a natural transformation: for the map $g : {0, 1} \to {*}$ , aggregating before applying $g$ and after applying $g$ give lists of different lengths, and the square does not commute in $Enum$ , although both sides have the same meaning. Naturality is not part of definition 175.7, and this is why.

Referenced from 2 locations

Inference as Semantics-Preserving Program Transformation

Remark 175.10 — What the criterion does not promise ¶

Definition 175.7 requires preservation of the mass function and nothing else. A transformation may preserve meaning and yet be useless: it may increase variance, run slower, or produce a population concentrated on one particle. Those are separate claims about convergence or cost, established by other arguments; the theorem of this chapter is exactly that the algorithm does not change what the program means.

Referenced from 2 locations

Inference as Semantics-Preserving Program Transformation

Exercise 175.1 ¶

★☆☆ Represent $obs$ in $Enum$ , compute the resulting list, apply $m^{Enum}$ , and check the answer against example 175.3.

Referenced from 2 locations

Inference as Semantics-Preserving Program Transformation

Exercise 175.2 ¶

★☆☆ Do the same in $Term$ : display the tree and evaluate its meaning by the two clauses of example 175.6.

Referenced from 2 locations

Inference as Semantics-Preserving Program Transformation

Exercise 175.3 ¶

★★☆ Exhibit a function $Enum X \to Enum X$ that normalizes each list to total weight $1$ , and show that it is not an inference transformation by evaluating both sides of definition 175.7 on the list representing $obs$ . State which quantity it destroys.

Referenced from 2 locations

Inference as Semantics-Preserving Program Transformation

Importance weighting

Before assembling an algorithm, one step must be derived rather than postulated: why weights appear at all. They come from a change of measure on a one-step model.

Proposition 175.11 — Importance weighting on one step ¶

Let $μ$ and $ν$ be finite measures with finite support on a countable set $X$ with $μ (x) > 0$ whenever $ν (x) > 0$ , and let $w (x) = ν (x) / μ (x)$ for $μ (x) > 0$ . Then for every $f : X \to Mass Y$ , $ν ≫ =^{Mass} f = μ ≫ =^{Mass} λ x . (w (x) \cdot f (x)) .$ In particular, drawing from $μ$ and weighting each draw by $w$ represents $ν$ .

Referenced from 4 locations

Inference as Semantics-Preserving Program Transformation

Proof of Proposition 175.11 — Importance weighting on one step

Proof. Evaluate both sides at $y$ : $\sum_{x} ν (x) f (x) (y) = \sum_{x : μ (x) > 0} μ (x) \frac{ν (x)}{μ (x)} f (x) (y),$ and the omitted terms have $ν (x) = 0$ by hypothesis. ◻

Example 175.12 — The model, by importance weighting ¶

Take $μ = {flip}^{Mass}$ , the prior, and $ν$ the unnormalized posterior of example 175.3. Then $w (tt) = \frac{3 / 2}{1 / 2} = 3$ and $w (ff) = \frac{1 / 2}{1 / 2} = 1$ , which are the two scores of the model. Proposition 175.11 says that sampling $H$ from the fair coin and attaching the weight $3$ or $1$ represents $ν$ exactly; the weighted population $[(3 / 2, tt), (1 / 2, ff)]$ has $m^{Enum}$ equal to ${tt \mapsto 3 / 2, ff \mapsto 1 / 2}$ , which is example 175.3. The score construct of the model is the importance weight; nothing further is postulated.

Referenced from 4 locations

Inference as Semantics-Preserving Program Transformation

Transformers: weights, populations, suspensions

Sequential Monte Carlo is assembled from three constructions applied to a base representation, and each is introduced by the single obstruction it removes.

Definition 175.13 — Inference transformer ¶

An inference transformer $F$ assigns an inference representation $F T$ to every inference representation $T$ , an inference transformation ${tmap}_{F} t : F T \to F S$ to every inference transformation $t : T \to S$ , and an inference transformation ${lift}_{T} : T \to F T$ .

Referenced from 2 locations

Inference as Semantics-Preserving Program Transformation

Definition 175.14 — The three transformers ¶

Weighting. $W T X = T (R^{+} \times X)$ , with $return x = {return}^{T} (1, x)$ ; bind multiplies the accumulated weights; ${score}^{W T} r = {return}^{T} (r, *)$ ; $lift a = a ≫ =^{T} λ x . {return}^{T} (1, x)$ ; and $m^{W T} (a) (x) = \sum {r \cdot m^{T} (a) (r, x) ∣ r \in R^{+}}$ , the weighted mass.

Populations. ${List}_{T} X = T (List X)$ with $m^{{List}_{T}} (a) =$ the sum of the meanings of the entries, and ${Pop}_{T} = W \circ {List}_{T}$ , so that ${Pop}_{T} X = T (List (R^{+} \times X))$ : a computation in $T$ producing a list of weighted particles. Its meaning function is $m^{{Pop}_{T}} (a) = \sum_{particles} (weight) \cdot (value),$ the total measure of the population, summed over the randomness of $T$ .

Suspensions. Let ${Sus}_{T} X = T ({Return X} \cup {Yield ({Sus}_{T} X)})$ , with ${score}^{{Sus}_{T}} r = {return}^{T} (Yield (lift ({score}^{T} r))),$ so that a computation suspends after each score. Its two operations are $advance$ , which runs one suspended step, and $finish$ , which runs all of them; $m^{{Sus}_{T}} (a) = m^{T} (finish (a))$ .

Referenced from 3 locations

Inference as Semantics-Preserving Program Transformation

Lemma 175.15 — Suspension steps preserve meaning ¶

$advance : {Sus}_{T} \to {Sus}_{T}$ and $finish : {Sus}_{T} \to T$ are inference transformations, and ${tmap}_{Sus} t$ is one whenever $t$ is.

Referenced from 4 locations

Inference as Semantics-Preserving Program Transformation

Proof of Lemma 175.15 — Suspension steps preserve meaning

Proof. By definition 175.14 the meaning of a suspended computation is the meaning of the computation obtained by running it to completion, so $\begin{aligned} m^{{Sus}_{T}} (advance (a)) & = m^{T} (finish (advance (a))) \\ = m^{T} (finish (a)) = m^{{Sus}_{T}} (a), \end{aligned}$ the middle equality because $finish$ runs every remaining step, and running one step first leaves the same computation to run. For $finish$ itself, the required equation is its definition. For ${tmap}_{Sus} t$ , the meaning of the transformed computation is computed by folding $m^{S} \circ t$ over the suspension structure, and $m^{S} \circ t = m^{T}$ by hypothesis. ◻

Lemma 175.16 — Spawning preserves meaning ¶

For $n \geq 1$ , let $spark n \in {Pop}_{T} 1$ be the population of $n$ particles each carrying the value $*$ and the weight $1 / n$ , and let $spawn (n, a) = spark n ≫ = λ * . a$ . Then $m^{{Pop}_{T}} (spark n) = δ_{*}$ and $spawn (n, -) : {Pop}_{T} \to {Pop}_{T}$ is an inference transformation.

Referenced from 5 locations

Inference as Semantics-Preserving Program Transformation

Proof of Lemma 175.16 — Spawning preserves meaning

Proof. The total measure of $spark n$ is $n \cdot \frac{1}{n} δ_{*} = δ_{*}$ , of mass $1$ . Hence $m (spawn (n, a)) = δ_{*} ≫ =^{Mass} λ * . m (a) = m (a)$ by the left unit law of definition 175.2. ◻

Lemma 175.17 — The discrete weighted randomiser ¶

Let $x s$ be the finite weighted list $[(r_{1}, x_{1}), \dots, (r_{k}, x_{k})]$ , let $w = \sum_{i} r_{i}$ , and let $U$ be the uniform measure on $[0, 1)$ . When $w > 0$ , put $dwrand (x s, u) = Take x_{j}$ for the unique $j$ with $\frac{1}{w} \sum_{i < j} r_{i} \leq u < \frac{1}{w} \sum_{i \leq j} r_{i},$ and when $w = 0$ define $dwrand (x s, u) = Fail$ . Then $\begin{matrix} w = 0 \Rightarrow dwrand (x s, -)_{*} U = δ_{Fail}, \\ w > 0 \Rightarrow dwrand (x s, -)_{*} U = \sum_{i} \frac{r_{i}}{w} δ_{Take x_{i}} . \end{matrix}$ Consequently, for a representation $T$ with an element $fail$ of meaning $0$ , the discrete weighted sampler $dwsample (x s) = {score}^{T} (w) ≫ = λ * . (sample ≫ = λ u . case dwrand (x s, u))$ has $m^{T} (dwsample (x s)) = \sum_{i} r_{i} δ_{x_{i}}$ .

Referenced from 6 locations

Inference as Semantics-Preserving Program Transformation

Proof of Lemma 175.17 — The discrete weighted randomiser

Proof. The intervals $[\frac{1}{w} \sum_{i < j} r_{i}, \frac{1}{w} \sum_{i \leq j} r_{i})$ for $j = 1, \dots, k$ partition $[0, 1)$ and have lengths $r_{j} / w$ , so the pushforward of $U$ assigns $r_{j} / w$ to $Take x_{j}$ ; when $w = 0$ the function is constantly $Fail$ . For the second claim, $m^{T} (dwsample (x s)) = w \cdot \sum_{i} \frac{r_{i}}{w} δ_{x_{i}} = \sum_{i} r_{i} δ_{x_{i}}$ , using the score law and the bind law of definition 175.4 and the first claim; the $Fail$ branch contributes $0$ because $m^{T} (fail) = 0$ . ◻

Proposition 175.18 — Resampling preserves meaning ¶

Let $resample (n, a) = a ≫ = λ x s . spawn (n, {dwsample}_{{Pop}_{T}} (x s))$ . Then $resample (n, -) : {Pop}_{T} \to {Pop}_{T}$ is an inference transformation.

Referenced from 6 locations

Inference as Semantics-Preserving Program Transformation

Proof of Proposition 175.18 — Resampling preserves meaning

Proof. Fix a population $x s$ of total weight $w$ . By lemma 175.17 the discrete weighted sampler on $x s$ has meaning $\sum_{i} r_{i} δ_{x_{i}}$ , which is the meaning of the population $x s$ ; by lemma 175.16, spawning $n$ copies of it leaves that meaning unchanged. The meaning function of ${Pop}_{T}$ satisfies the bind law of definition 175.4, so replacing the population inside $a$ by one of equal meaning leaves the meaning of the bind unchanged. ◻

Example 175.19 — Resampling the two particles ¶

Take the ordered population $[(3 / 2, tt), (1 / 2, ff)]$ of example 175.12, of total weight $2$ . The normalized cumulative bounds are $3 / 4$ and $1$ , so $dwrand$ sends $u < 3 / 4$ to $tt$ and $3 / 4 \leq u < 1$ to $ff$ . Feeding the two uniforms $1 / 8$ and $7 / 8$ produces the ordered unweighted population $[tt, ff]$ , each particle carrying weight $1 / 2$ after the spark, and total weight $2$ after the score in $dwsample$ . Its meaning is $2 \cdot (\frac{1}{2} δ_{tt} + \frac{1}{2} δ_{ff}) = δ_{tt} + δ_{ff}$ , of total mass $2$ — the same total mass as example 175.3, as proposition 175.18 requires, although the two measures differ: resampling preserves the mass function of the population as a random object, not the value of one draw.

Referenced from 3 locations

Inference as Semantics-Preserving Program Transformation

Theorem 175.20 — The sequential Monte Carlo composite ¶

Let $T$ be a sampling representation and let $n, k \geq 1$ . The composite $\begin{aligned} {smc}_{n, k} : (Sus \circ Pop)_{T} & \overset{{tmap}_{Sus} spawn (n, -)}{\to} (Sus \circ Pop)_{T} \\ \overset{(advance \circ {tmap}_{Sus} resample (n, -))^{\circ k}}{\to} (Sus \circ Pop)_{T} \\ \overset{finish}{\to} {Pop}_{T} \end{aligned}$ is an inference transformation.

Referenced from 5 locations

Inference as Semantics-Preserving Program Transformation

Proof of Theorem 175.20 — The sequential Monte Carlo composite

Proof. Each factor is an inference transformation: spawning by lemma 175.16 and resampling by proposition 175.18, hence their images under the suspension transformer by lemma 175.15, which also covers $advance$ and $finish$ . A $k$ -fold composite of inference transformations is one by lemma 175.8, and so is the whole composite. ◻

Remark 175.21 — Reading the theorem ¶

Theorem 175.20 says that running the particle filter with $n$ particles for $k$ steps returns a population whose mass function is the meaning of the original program. It does not say that the population is a good approximation for any particular $n$ — that is a convergence statement, not proved here — and it does not say that ${Pop}_{T}$ is a monad: when $T$ is a sampler representation, which is not commutative, the monad laws fail for ${Pop}_{T}$ , which is why definition 175.4 does not require them. The proof used only the meaning laws, and this is exactly the generality the failure forces.

Referenced from 2 locations

Inference as Semantics-Preserving Program Transformation

Remark 175.22 — Comparison cards, owning no theorem ¶

Three further algorithms are treated in this chapter as comparison cards and as sources of problems only: the Metropolis method with its Green generalization, its trace-based variant, and resample-move sequential Monte Carlo. A reconstruction of the source’s Theorems 7.1 to 7.3 would introduce densities with respect to a dominating measure, Markov kernels on trace spaces, and support conditions, none of which appears above; that reconstruction is a separate development and is not claimed here. The implementations named in the literature, monad-bayes and the systems built on it, are used as laboratories and as sources of fixtures; none of them is an interchangeable proof artifact for theorem 175.20.

Referenced from 2 locations

Inference as Semantics-Preserving Program Transformation

Exercise 175.4 ¶

★☆☆ Verify lemma 175.16 for $n = 3$ by computing the meaning of $spark 3$ directly, and state what goes wrong if the sparked weights are $1$ rather than $1 / n$ .

Referenced from 2 locations

Inference as Semantics-Preserving Program Transformation

Exercise 175.5 ¶

★★☆ In lemma 175.17, compute $dwrand (x s, u)$ for $u = 3 / 4$ exactly, and show that changing the half-open intervals to closed ones would make the pushforward assign mass to two outcomes at once.

Referenced from 2 locations

Inference as Semantics-Preserving Program Transformation

Exercise 175.6 ¶

★★☆ Let $x s$ have total weight $0$ . Compute $m^{T} (dwsample (x s))$ and show that proposition 175.18 still holds, identifying the hypothesis $m^{T} (fail) = 0$ where it is used.

Referenced from 2 locations

Inference as Semantics-Preserving Program Transformation

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 175.7, then exercise 175.8, then the practical project exercise 175.11.

Exercise 175.7 ¶

★☆☆ For $obs$ , compute the unnormalized measure and posterior by exact enumeration and by importance weighting from the prior, and check that the two agree with example 175.3 and example 175.12.

Referenced from 3 locations

Inference as Semantics-Preserving Program Transformation

Exercise 175.8 ¶

★★☆ Write the proof of proposition 175.18 for a population of two particles, displaying every use of the bind law of definition 175.4 and the exact rational weights at each stage.

Referenced from 3 locations

Inference as Semantics-Preserving Program Transformation

Exercise 175.9 ¶

★★☆ Modify $resample$ so that the score ${score}^{T} (w)$ inside $dwsample$ is omitted. Compute the meaning of the resulting population for example 175.19 and identify the exact factor by which it differs from the correct value. State which line of the proof of lemma 175.17 the modification invalidates.

Referenced from 2 locations

Inference as Semantics-Preserving Program Transformation

Exercise 175.10 ¶

★★☆ Give a two-score program in the fragment of section 175.1, display its representation in ${Sus}_{Enum}$ , and compute $advance$ once and $finish$ , checking lemma 175.15 on it.

Referenced from 2 locations

Inference as Semantics-Preserving Program Transformation

Exercise 175.11 ¶

★★★ Practical project.smc-meaning-checker Build a meaning-preservation checker for the finite fragment. It has three parts: an exact enumerator computing $m^{Enum}$ as a table of reduced rationals; an importance-weighting stage implementing proposition 175.11 from an explicitly supplied proposal; and a multinomial resampler implementing $dwrand$ of lemma 175.17 driven by an explicit list of rationals in $[0, 1)$ instead of a random source.

The invariant to maintain is that every stage records both the population and its total weight, and that the checker compares the complete rational representation of the mass function before and after each stage, not merely its normalization.

The concrete result is the sequence of exact tables for $obs = H \leftarrow coin (1 / 2); score (if H then 3 else 1); return H$ . The acceptance test is decidable and exact: exact enumeration and importance weighting must both print the unnormalized table ${tt \mapsto 3 / 2, ff \mapsto 1 / 2}$ and the posterior ${tt \mapsto 3 / 4, ff \mapsto 1 / 4}$ ; the resampler applied to the ordered particles $[(tt, 3 / 2), (ff, 1 / 2)]$ with the stream $[1 / 8, 7 / 8]$ must return the ordered unweighted population $[tt, ff]$ , compared as a list, in that order; and the checker must report the total weight $2$ unchanged across the resampling stage. A large-sample display of frequencies is commentary only. This checker exercises the finite instance of theorem 175.20 and proves no part of it.

Referenced from 3 locations