von_neumann below again has the same semantics $i[g \cdot \lambda]$ as expo and expo', as an exercise. We first define:

$$
\begin{align*}
\text{longest_decreasing_run} &\stackrel{\text{def}}{=} \text{rec}(\lambda f_{\text{real}} \to \text{int} \to \text{Dint} \cdot \lambda x_{\text{real}} \cdot \lambda n_{\text{int}}) \\
&\qquad \text{do } u \leftarrow \text{sample}[\lambda_1]; \\
&\qquad \text{if } (\underline{\text{pos}}(u - x)) \\
&\qquad \qquad \text{ret } n \\
&\qquad \qquad (f \ u \ (n + 1)))
\end{align*}
$$

Given any $x \in [0, 1]$, $[[longest_decreasing_run]] \rho(x)(0)$ returns the largest $n$ such that $x > u_1 > u_2 > \dots > u_n$
($\le u_{n+1}$) for randomly uniformly distributed real numbers $u_1, u_2, \dots$, in $[0, 1]$. It is a standard exercise to show that
$[[longest_decreasing_run]] \rho(x)(0)$ is the distribution on $\mathbb{Z}_\perp$ giving probability $\frac{x^n}{n!} - \frac{x^{n+1}}{(n+1)!}$ to each $n \in \mathbb{N}$, and
probability 0 to all other elements. Drawing a value $n$ at random with respect to that distribution, the probability that $n$
is even is $\sum_n \text{even}\left(\frac{x^n}{n!} - \frac{x^{n+1}}{(n+1)!}\right) = e^{-x}$. Assuming a term `odd`: `int` $\to$ `bool` testing whether its argument is odd, one
then defines:

$$
\begin{align*}
\text{von\_neumann} &\stackrel{\text{def}}{=} \text{do } x_{\text{real}} \leftarrow \text{sample}[\lambda_1]; \\
\text{rec}(\lambda f_{\text{real}} \to \text{Dreal} \cdot \lambda \ell_{\text{real}}) \\
&\qquad \text{do } b_{\text{bool}} \leftarrow \text{longest\_decreasing\_run } x \; 0; \\
&\qquad \text{if } b \\
&\qquad \qquad f(\ell + 1.0) \\
&\qquad \qquad \text{ret } \ell) x
\end{align*}
$$

The **rec** expression in the middle maps every real number $\ell$ to $\ell + m$, where $m$ is the average number of calls to
**longest_decreasing_run** $x \ 0$ it takes it to return an even number.

We direct the reader to [21] for an explanation and some faster algorithms based on the same principle. See also [24]
for a generalization to densities of the form $e^{-G(x)}$, including normal distributions.

A.4 Proofs omitted from Section 9.5 (distributions on higher-order objects)

**Lemma 9.1 (recap).** *The Scott topology of $[[\text{int} \to \text{real}]]$ has a subbase of open sets of the form $[n \in V] \stackrel{\text{def}}{=} \{f \in [\mathbb{Z}_\perp \to \mathbb{R}_\perp] | f(n) \in V\}$, where $n$ ranges over $\mathbb{Z}_\perp$ and $V$ ranges over the open subsets of $\mathbb{R}_\perp$.*

The map $j$ is a topological embedding of $\mathbb{R}^N$ into $[[\text{int} \to \text{real}}]]$.

PROOF. $\mathbb{Z}_\perp$ and $\mathbb{R}_\perp$ are bc-domains, and therefore the Scott topology on $[\mathbb{Z}_\perp \to \mathbb{R}_\perp]$ coincides with the topology of pointwise convergence [32, Proposition 11.2]. The latter is the topology generated by the indicated subbasic open sets $[n \in V]$, by definition. This can also be deduced from Proposition II-4.6 of [27].

The inverse image $j^{-1}([n \in V])$ is equal to the subbasic open set $\pi_n^{-1}(U) \stackrel{\text{def}}{=} \{\vec{x} \in \mathbb{R}^N \mid x_n \in U\}$ (where $U \stackrel{\text{def}}{=} i^{-1}(V)$) if $n \in \mathbb{N}$, is empty if $n \notin \mathbb{N}$ and $\perp \notin V$, and is the whole of $\mathbb{R}^N$ otherwise. Therefore $j$ is continuous.

Finally, every subbasic open set $\pi_n^{-1}(U)$ ($n \in \mathbb{N}$, $U$ open in $\mathbb{R}$) is equal to $j^{-1}([n \in V])$, where $V$ is any open subset of $\mathbb{R}_\perp$ such that $i^{-1}(V) = U$ (which exists since $i$ is an embedding). Hence $j$ is a topological embedding. $\square$

<figure><img src="image_5.png" /></figure>
**Lemma 9.2 (recap).** The function bin: $\mathbb{R} \to \{0, 1\}^N$ that maps every number in $[0, 1[$ to the string of bits in its binary expansion (namely, the ith bit in bin(x) is $\lfloor 2^i \cdot x \rfloor$, for any $i \ge 1$), every negative number to the all zero string $0^\omega$, and every number larger than or equal to 1 to the all one string $1^\omega$ is measurable. The image measure bin[$\lambda_1$] is the unique measure v on $[0, 1]$ such that $v(\{s \in \{0, 1\}^N | s_0 = b_0, \dots, s_{k-1} = b_{k-1}\}) = 1/2^k$ for all $k \in \mathbb{N}$ and elements $b_0, \dots, b_{k-1} \in \{0, 1\}$.

**PROOF.** For every finite string $b \stackrel{\text{def}}{=} (b_0, b_1, \dots, b_{k-1})$ of bits, let $U_b$ be the set of infinite strings of bits having $b$ as a prefix. The sets $U_b$ form a countable base of the topology on $\{0, 1\}^N$, and $\text{bin}^{-1}(U_b)$ is the interval $[\sum_{i=0}^{k-1} b_i/2^{i+1}, \sum_{i=0}^{k-1} b_i/2^{i+1} + 1/2^k[$ if not all bits $b_i$ are equal to 0 or to 1, $]-\infty, 1/2^k[$ if all the bits $b_i$ are equal to 0, and to $[1 - 1/2^k, +\infty[$ otherwise. Every interval is in the Borel $\sigma$-algebra, and every open subset of $\{0, 1\}^N$ is a countable union of sets $U_s$, so the inverse image of any open subset of $\{0, 1\}^N$ by bin is Borel. It follows that bin is measurable. Then $\text{bin}[\lambda_1](U_b) = \lambda_1(\text{bin}^{-1}(U_b)) = \lambda(\text{bin}^{-1}(U_s) \cap [0, 1])$ is equal to $1/2^k$. Finally, the sets $U_b$ form a $\pi$-system, whence the claim of uniqueness follows from the fact that any two probability measures that agree on a $\pi$-system generating the $\sigma$-algebra are equal [6, Theorem 3.3]. $\square$

**Lemma 9.3 (recap).** The map num: $\{0, 1\}^N \to \mathbb{R}$ that sends $s$ to $\sum_{i \in \mathbb{N}} s_i/2^{i+1}$ is continuous, and the image measure num[v] is equal to $\lambda_1$.

**PROOF.** Let $U$ be any open subset of $\mathbb{R}$, and $s \in \text{num}^{-1}(U)$. For some $\epsilon > 0$, the interval $\text{num}(s) - \epsilon, \text{num}(s) + \infty[$ is included in $U$. We pick $k \in \mathbb{N}$ so that $1/2^k < \epsilon$. Then the set of elements $t \in \{0, 1\}^N$ such that $t_0 = s_0, \dots, t_k = s_k$ is an open neighborhood of $s$ that is included in $\text{num}^{-1}(U)$, showing that $\text{num}^{-1}(U)$ is open. Therefore $\text{num}$ is continuous.

It is easy to see that $\text{num}(\text{bin}(x)) = x$ for every $x \in [0, 1]$, so that $(\text{num} \circ \text{bin})^{-1}(E)$ and $E$ have the same intersection with $[0, 1]$, for every subset $E$ of $\mathbb{R}$. Hence, for every Borel measurable subset $E$ of $\mathbb{R}$, and using Lemma 9.2, $\text{num}[v](E) = \text{num}[\text{bin}[\lambda_1]](E) = \lambda((\text{num} \circ \text{bin})^{-1}(E) \cap [0, 1]) = \lambda(E \cap [0, 1]) = \lambda_1(E)$. $\square$

**Lemma 9.4 (recap).** The map split: $s \mapsto (s[0], \uparrow s)$ is a homeomorphism of $\{0, 1\}^N$ onto $(\{0, 1\}^N)^2$. The image continuous valuation (resp., measure) split[v] is the product valuation (resp., product measure) $v \otimes v$.

**PROOF.** The first part is a direct consequence of the fact that the pairing map is bijective. For the second part, we reason on continuous valuations, since that will be slightly easier. For every pair of disjoint finite subsets $I$ and $J$ of $\mathbb{N}$, let $U_{I,J}$ be the set of elements $s$ of $\{0, 1\}^N$ such that $s_m = 0$ for every $m \in I$ and $s_n = 1$ for every $n \in J$. We see that those sets form a base of the topology on $\{0, 1\}^N$, and that $v(U_{I,J}) = 1/2^{|I|+|J|}$, where $|\cdot|$ denotes cardinality, using the last part of Lemma 9.2, A base of the product topology on $(\{0, 1\}^N)^2$ is given by the sets $U_{I,J} \times U_{I',J'}$, and:

$$ \begin{aligned} \text{split}[v](U_{I,J} \times U_{I',J'}) &= v(\text{split}^{-1}(U_{I,J} \times U_{I',J'})) \\ &= v(U_{I',J'}), \end{aligned} $$

where $I'' \stackrel{\text{def}}{=} \{\langle 0, k \rangle | k \in I\} \cup \{\langle m' + 1, k \rangle | m', k \in \mathbb{N}, \langle m', k \rangle \in I'\}$ and $J'' \stackrel{\text{def}}{=} \{\langle 0, k \rangle | k \in J\} \cup \{\langle n' + 1, k \rangle | n', k \in \mathbb{N}, \langle n', k \rangle \in J'\}$. Hence $\text{split}[v](U_{I,J} \times U_{I',J'}) = 1/2^{|I''|+|J''|} = 1/2^{|I|+|I'|+|J|+|J'|}$. We also have:

$$ (v \otimes v)(U_{I,J} \times U_{I',J'}) = v(U_{I,J}) \cdot v(U_{I',J'}) = 1/2^{|I|+|J|} \cdot 1/2^{|I'|+|J'|}, $$

so split[v] and $v \otimes v$ coincide on the basic open sets $U_{I,J}$. Using modularity, they must coincide on any finite disjoint union of basic open sets, and by Scott-continuity, they must coincide on any arbitrary disjoint union of basic open sets. (This is an argument we have sketched in the proof of Theorem 4.1 already.) Since any two basic open sets $U_{I,J}$ are either comparable or disjoint, every open subset of $\{0, 1\}^N$ is such a disjoint union, and this concludes the proof. $\square$
**Theorem 9.6 (recap).** For every environment $\rho$, $[[rand\_uniform\_seq]] \rho = j[\lambda_1^\infty]$.

**PROOF.** Let $\pi_N: [[int \to real]]$ map $f$ to $(f(0), f(1), \dots, f(N-1))$. We start by fixing $N$, and we compute the value of $\pi_N([rand\_uniform\_seq]) \rho$. This is the valuation that maps every open subset $U$ of $\mathbb{R}_\perp^N$ to the probability that a function $f$ drawn at random according to $[[rand\_uniform\_seq]] \rho$ produces a tuple $(f(0), f(1), \dots, f(N-1))$ that falls in $U$. Let us begin by noting that $[[rand\_uniform\_seq]] \rho = mux[i[\lambda_1]]$.

Let $g: \mathbb{R} \to \mathbb{R}^N$ map $x$ to $(\text{num}(\text{bin}(x)[m]))_{m \in \mathbb{N}}$. It is easy to see that $g$ is measurable. By definition, $g(x)_m = \text{mux}(i(x))(m)$ for every non-dyadic number $x$ in $[0, 1]$, namely for every $x \in \mathbb{R} \setminus E_0$ where the set $E_0$ was introduced in Remark 9.1, and for every $m \in \mathbb{N}$.

We claim that $j[g[\lambda_1]] = \text{mux}[i[\lambda_1]]$. This needs a reminder and a comment. We recall that $j$ is the canonical embedding of $\mathbb{R}^N$ into $[[int \to real]]$; and we have silently promoted $\lambda_1$ from a continuous valuation to a measure on $\mathbb{R}$, therefore working with image *measures* rather than image *valuations*.

The claim is proved as follows. For every Borel measurable subset $E$ of $[[int \to real]]$, $j[g[\lambda_1]](E) = \lambda_1((j \circ g)^{-1}(E))$, while $\text{mux}[i[\lambda_1]] = \lambda_1((\text{mux} \circ i)^{-1}(E))$. The symmetric difference of $(j \circ g)^{-1}(E)$ and of $(\text{mux} \circ i)^{-1}(E)$ is included in $E_0$, which has $\lambda_1$-measure zero, so $j[g[\lambda_1]](E) = \lambda_1((j \circ g)^{-1}(E))$.

Let us write $i^{(N)}$ for the $N$-fold product $i \times \dots \times i$, and similarly with $\text{num}^{(N)}$. For every $x \in \mathbb{R}$, $\pi_N(\text{mux}(i(x))) = (i(g(x)_0), \dots, i(g(x)_{N-1})) = (i(\text{num}(\text{bin}(x)[0])), \dots, i(\text{num}(\text{bin}(x)[N-1])) = (i^{(N)} \circ \text{num}^{(N)} \circ \omega_N \circ \text{bin})(x)$. It follows:

$$
\begin{align*}
\pi_N[\text{mux}[i[\lambda_1]]] &= i^{(N)}[\text{num}^{(N)}[\omega_N[\text{bin}[\lambda_1]]]] \\
&= i^{(N)}[\text{num}^{(N)}[\omega_N[v]]] \qquad \text{by Lemma 9.2} \\
&= i^{(N)}[\text{num}^{(N)}[v \otimes \dots \otimes v]] \qquad \text{by Corollary 9.5, item 3} \\
&= i[\text{num}[v]] \otimes \dots \otimes i[\text{num}[v]] \\
&= i[\lambda_1] \otimes \dots \otimes i[\lambda_1] \qquad \text{by Lemma 9.3.}
\end{align*}
$$

This is a statement about measures. Restricting to open sets, we obtain the following statement about continuous valuations:

*Fact A.1.* $\pi_N([rand\_uniform\_seq] \rho)$ is the $N$-fold valuation product of $i[\lambda_1]$.

We use this to prove that $[[rand\_uniform\_seq]] \rho j[\lambda_1^\infty]$, qua continuous valuations. It suffices to show that the two sides of the equation coincide on basic open subsets of $[[int \to real]]$: as in the proof of Theorem 4.1 or of Lemma 9.4, modularity and Scott-continuity will imply they also coincide on every open set at all.

As basic open subsets, Lemma 9.1 suggests that we take the finite intersections of sets of the form $[n \in V]$. Without loss of generality, let $U = \overline{[0 \in V_0] \cap [1 \in V_1] \cap \dots \cap [N-1 \in V_{N-1}]}$. (Any set of the form $[n \in V_n]$ where $V_n$ is the whose of $\mathbb{R}_\perp$ can be inserted at will, since they will not modify the intersection.) We note that $U = \pi_N^{-1}(V_0 \times V_1 \times \dots \times V_{N-1})$, so:

$$
\begin{align*}
[[rand\_uniform\_seq]] \rho(U) &= \pi_N([rand\_uniform\_seq]) \rho(V_0 \times V_1 \times \dots \times V_{N-1}) \\
&= \prod_{n=0}^{N-1} i[\lambda_1](V_n) \quad \text{by Fact A.1.}
\end{align*}
$$
Now, since $j(\vec{x})(n) = i(x_n)$ for all $\vec{x} \in [0, 1]^N$ and $n \in \mathbb{N}$, $j^{-1}(U) = \pi_N^{-1}(i^{-1}(V_0) \times i^{-1}(V_1) \times \cdots \times i^{-1}(V_{N-1}))$, so:

$$ 
\begin{aligned}
j[\lambda_1^\infty](U) &= \pi_N[\lambda_1^\infty](i^{-1}(V_0) \times i^{-1}(V_1) \times \cdots \times i^{-1}(V_{N-1})) \\
&= \prod_{n=0}^{N-1} \lambda_1(i^{-1}(V_n)),
\end{aligned}
$$

by definition of $\lambda_1^\infty$, and this concludes the proof. □

## A.5 More distributions on higher-order objects

At this point, let us be less formal. The construction of $\lambda_1^\infty$ through `randUniform_seq` opens up several avenues, which we mostly leave as programming exercises to the reader.

For one, we can now implement the Box-Muller algorithm (see Section 9.2) by drawing just one random real. We remember that the Box-Muller algorithm uses rejection sampling, which may require us to draw arbitrarily many independent, random, $\lambda_1$-distributed real numbers. Instead, we can just call `randUniform_seq` once, obtaining a random, $\lambda_1^\infty$-distributed function $f$ (modulo the embedding $j$); each time we need another random real number, we simply read the next value $f(n)$, for larger and larger values of $n$.

Going further, instead of calling `randUniform_seq`, we may call `mux` on a random $\lambda_1$-distributed real number given as argument. We obtain an ISPCF term `box_muller_transform` of type `real \to real \times real` (not `real \to D(real \times real)`), since that term no longer draws anything at random by itself) that maps a random $\lambda_1$-distributed real number to a pair of two independent, random $\mathcal{N}(0, 1)$-distributed real numbers.

$$ \text{box\_muller\_transform} \stackrel{\text{def}}{=} \lambda_{\text{seed}}_{\text{real}}. $$

let `randnums`$_{int}$$\to$`real` = `mux` seed in

let `x`$_{real}$ = `randnums` 0 in

let `y`$_{real}$ = `randnums` 1 in

let `c`$_{real}$ = `cos(2.0 \times \pi \times y)` in

let `s`$_{real}$ = `sin(2.0 \times \pi \times y)` in

let `m`$_{real}$ = `sqrt(-2.0 \times log x)` in

$$ \langle m \times c, m \times s \rangle. $$

We let the reader check that the semantics of:

do `seed` $\leftarrow$ `sample`[$\lambda_1$]; `ret`(box\_muller\_transform `seed`)

is $i[\mathcal{N}(0, 1) \otimes \mathcal{N}(0, 1)]$, just like `box_muller`.

The tricks described above suggest the following scheme for implementing the infinite product $\mathcal{N}(0, 1)^\infty$. We call `randUniform_seq` in order to obtain an infinite, independent sequence of $\lambda_1$-distributed real numbers. We then apply `box_muller Transform` to each. Explicitly, we form the ISPCF term:

do `f`$_{int}$$\to$`real` $\leftarrow$ `randUniform_seq`; `ret` $\lambda n$$_{int}$.box\_muller\_transform($f$ $n$),

of type $D(int \to real)$.
Again, this can be made into a transformer

box_muller_sequence_transform: real → D(int → real)

that maps any random $\lambda_1$-distributed real number to a random $N(0, 1)^\infty$-distributed infinite sequence of real numbers. This can also be iterated. We let the reader explore around this idea. For example, given two maps mean, sigma: int → real, build a term that maps any random $\lambda_1$-distributed real number to a random infinite sequence of independent real numbers, whose nth entry follows a normal distribution with mean mean(n) and with standard deviation sigma(n).

One can implement infinite independent sequences of random real numbers following various other distributions in the same way. For example, do this for infinite products of exponential distributions.

This machinery can also be used to implement non-trivial distributions over distributions. A typical, and useful, application is the Dirichlet process [22], which is widely used as a source of Bayesian priors in the field of nonparametric estimation problems. Given a base distribution $H$ over some space $X$, and a parameter $\alpha \in ]0, 1[$, the Dirichlet process DP($H$) is a distribution over the space of probability distributions over $X$, which one may describe as follows. We draw an infinite sequences of elements $x_n, n \in \mathbb{N}$, from $X$. At step $n$, with probability $\alpha/(\alpha + n)$, we draw $x_n$ from $X$, independently from all previous values, using the distribution $H$; otherwise, we draw $x_n$ at random among the previous values, each having the same probability, in other words with respect to the distribution $\frac{1}{n} \sum_{i=0}^{n-1} \delta_{x_i}$. (This is undefined if $n = 0$, but then, if $n = 0$, that second case happens with zero probability.) This process yields a random infinite sequence, which we can use directly, or which we can convert to a distribution, the directing measure, mapping every measurable subset $E$ of $X$ to the limit of $(\frac{1}{n} \sum_{i=0}^{n-1} \delta_{x_i})(E)$ as $n$ tends to $+\infty$, which exists $H$-almost surely by de Finetti's theorem [47, Chapter 1.1], based on the fact that the sequence $(x_n)_{n \in \mathbb{N}}$ is what is known as an exchangeable sequence.

In principle, one can compute the directing measure from any exchangeable sequence, as shown by Daniel Roy [65, Chapter IV]. In the special case of the Dirichlet process, there is a popular, and more efficient, implementation of DP($H$), using the stick-breaking algorithm, see Figure 2 of [29] for example. (We also refer to that paper for an application of the Dirichlet process to an interesting, stochastic form of memoization.) While the latter relies on memoizing facilities (hence on global state, possibly hidden), one can implement it in ISPCF as follows, given $H^\infty$ (not $H!$) as argument.

We assume that $X$ is the denotation $[\tau]$ of some type $\tau$, and that the variable $proc_D(int \to \tau)$ holds a representation of $H^\infty$. We draw a random function atoms: int → τ with respect to $H^\infty$, representing some infinite sequence $(\theta_n)_{n \in \mathbb{N}}$ of elements of $X$; this uses do and proc. We also draw a random function sticks: int → real with respect to the distribution Beta(1, $\alpha)^\infty$ (the infinite product of the $\beta$ distribution with parameters 1 and $\alpha$), representing a random sequence $(\beta'_n)_{n \in \mathbb{N}}$. We define a new random (but no longer independent) sequence $(\beta_n)_{n \in \mathbb{N}}$, where $\beta_n \stackrel{\text{def}}{=} \beta'_n \cdot \prod_{i=0}^{n-1} (1 - \beta'_i)$. and we return the (random) distribution $\sum_{n \in \mathbb{N}} \beta_n \delta_{\theta_n}$.

While that would be possible in ISPCF, we do not compute any $\beta_n$ explicitly. Instead, the final distribution is obtained by the following informal procedure: with probability $\beta'_0$, return $\theta_0$; else, with probability $\beta'_1$, return $\theta_1$; else, with probability $\beta'_2$, return $\theta_2$, and so on. This terminates with probability 1.
This can be implemented in ISPCF by drawing a third function `rand: int → real` at random with respect to $\lambda_1^\infty$, then returning `atoms` (`pick_a_stick sticks rand 0`), where:

$$ 
\begin{align*}
\text{pick\_a\_stick} &\stackrel{\text{def}}{=} \lambda\text{sticks}_{\text{int}→\text{real}}.\lambda\text{rand}_{\text{int}→\text{real}}.\text{rec}(\lambda\text{pick}_{\text{int}→\text{int}}. \\
&\qquad \lambda j_{\text{int}}. \\
&\qquad \mathbf{if}(\underline{\text{pos}(\text{sticks } j - \text{rand } j)}) \\
&\qquad \qquad j \\
&\qquad \qquad (\text{pick } (j + 1))).
\end{align*}
$$

We have taken the same procedure names as in [29, Figure 2], in the hope that this will ease a comparison with the Church implementation of the Dirichlet process given there.

# B OTHER OMITTED PROOFS

## B.1 Proof of Proposition 10.8

**Proposition 10.8 (recap).** Let $\Sigma$ consist of strictly observable first-order constants. The map Next is Scott-continuous from $\Gamma$ to $V\Gamma$.

**PROOF.** Let $L$ be any generalized ISPCF term, $V$ be any Scott-open subset of $V\Gamma$, and let us assume that $\text{Next}(L) \in V$. We will show that there is a Scott-open neighborhood $U$ of $L$ such that $U \subseteq \text{Next}^{-1}(V)$. $U$ will consist of terms of the same shape $P$ as $L$.

If $L$ is of the form $E[\text{rec } M]$, then $\text{Next}(L) = \delta_R$ where $R \stackrel{\text{def}}{=} E[M(\text{rec } M)]$ is computed as follows: writing $L$ as $P\theta$ for some unique configuration $(P, \theta)$, $R$ is obtained as $Q\theta'$ for some unique configuration $(Q, \theta')$, where $Q$ is obtained from $P$ alone (independently of $\theta$), and $\theta' = \theta \circ \sigma$ for some function $\sigma: \text{fv}(Q) \to \text{fv}(P)$ that is determined from $P$ alone, again. For example, if $L = \underline{1.0} + \text{rec}(\lambda x.x \times \underline{2.0})(3.0)$, then $P = x_1 + \text{rec}(\lambda x.x \times x_2)(x_3)$, $Q = x_1 + (\lambda x.x \times x_2)(\text{rec}(\lambda x.x \times x_3))(x_4)$, and $\sigma$ maps $x_1$ to $x_1$, $x_2$ and $x_3$ to $x_2$, and $x_4$ to $x_3$.

Since $\delta_R$ is in $V$, $R$ is in $V \stackrel{\text{def}}{=} \eta_\Gamma^{-1}(V)$, and $\theta'$ is in the open subset $\{\theta' \in \mathbb{R}^{\text{fv}(Q)} | Q\theta' \in V\}$. The map $S: \theta \mapsto \theta \circ \sigma$ is clearly Scott-continuous. It follows that $U \stackrel{\text{def}}{=} \{P\theta | \theta \in S^{-1}(\{\theta' \in \mathbb{R}^{\text{fv}(Q)} | Q\theta' \in V\})\}$ is Scott-open in $\Gamma$. Moreover, by definition, for every generalized ISPCF term $P\theta$ in $U$, $\text{Next}(P)$ is in $V$.

We reason similarly for all other rules except (5), (6), and (7). The case of (7) is not that different. In the final step, $U$ is equal to the intersection of $\{P\theta | \theta \in S^{-1}(\{\theta' \in \mathbb{R}^{\text{fv}(Q)} | Q\theta' \in V\})\}$ with the set $U'$ of generalized ISPCF terms of shape $P$ on which rule (7) applies; then we will be able to conclude as above, once we prove that $U'$ is open. In order to do so, and since we are in the case of (7), $P$ is of the form $E[\underline{f} M_1 \cdots M_k]$, where each $M_i$ is either a constant (if its type is not **real**) or a template variable. Let $x_{j+1}, \dots, x_{j+p}$ be the template variables occurring among the terms $M_i$, listed from left to right, and say that $x_{j+1} = M_{i_1}, \dots, x_{j+p} = M_{i_p}$, where $1 \le i_1 < \cdots i_p \le k$. Let also $M_i$ be the constant $\underline{a}_i$ for each $i$ not among $i_1, \dots, i_p$. Then $U' = \{P\theta | \theta \in \mathbb{R}^{\text{fv}(P)}, f(a_1) \cdots (a_{i_1-1})(\theta(x_{j+1}))(a_{i_1+1}) \cdots (a_{i_2-1})(\theta(x_{j+2}))(a_{i_2+1}) \cdots (a_{i_{p-1}})(\theta(x_{k+p}))(a_{i_{p+1}}) \cdots (a_k) \in \text{Obs}_\beta\}$, where $\beta$ is the (observable) type of $f M_1 \cdots M_k$, and $\text{Obs}_\beta$ is the subset of observable elements of $[\beta]$. It is easy to see that $\text{Obs}_\beta$ is Scott-open. Since $f$ is Scott-continuous, $U'$ is open.

In the case of (6), $L = E^0[\text{score } \underline{a}]$. We write $L$ as $P\theta$ for some unique configuration $(P, \theta)$, once again. Then $\text{Next}(L) = |\underline{a}|.\delta_{E[\text{ret}_*]}$ where $E^0[\text{ret}_*]$ can be written as $Q\theta'$ for some configuration $(Q, \theta')$. Once again, $Q$ is determined as a function of $P$ alone. In fact, if $\underline{a}$ is the $m$th occurrence of a constant of type **real** in $L$ (so that $\theta(x_m) = \underline{a}$;
recall that $x_m$ is the $m$th template variable), and $fv(P) = \{x_1, \cdots, x_n\}$ with $n \ge m$, then $fv(Q) = \{x_1, \cdots, x_{n-1}\}$, and $\theta' = \theta \circ \sigma$, where $\sigma$ maps $x_1$ to $x_1, \dots, x_{m-1}$ to $x_{m-1}$, and $x_m$ to $x_{m+1}, \dots, x_{n-1}$ to $x_n$. The map $a \mapsto |a|$ is Scott-continuous from $\mathbb{R}$ to $\bar{\mathbb{R}}_+$. Product is a Scott-continuous map on $\bar{\mathbb{R}}_+$, from which we obtain easily that $(a, v) \mapsto av$ is Scott-continuous from $\bar{\mathbb{R}}_+ \times \mathbb{V}\Gamma$ to $\mathbb{V}\Gamma$. Using that $\eta_\Gamma$ is also Scott-continuous, the map $(a, \theta') \in \mathbb{R} \times \mathbb{R}^{fv(Q)} \mapsto |a| \cdot \delta_{Q\theta'}$ is Scott-continuous, and therefore $S: \theta \in \mathbb{R}^{fv(P)} \mapsto |\theta(x_m)| \cdot \delta_{Q(\theta \circ \sigma)}$ is also Scott-continuous. We then define $U$ as $\{P\theta \mid \theta \in S^{-1}(V)\}$. This is open, contains $L$, and its image by $\mathcal{N}ext$ is included in $V$ by definition.

In the case of (5), finally, $L = E^0[\mathbf{sample}[\mu]]$. This time, $L = P\theta$ for some unique configuration $(P, \theta)$. For every $a \in \mathbb{R}$, $f_{E^0}(a) = E^0[\underline{ret a}]$ can be written as $Q\theta'(a)$, where $(Q, \theta'(a))$ is a configuration such that $Q$ is obtained from $P$ alone, as in previous cases. Additionally, there is a number $m$ (the number of the template variable that is replaced by $a$ in $Q$), the template variables of $P$ are $x_1, \cdots, x_n$ with $n \ge m$, the template variables of $Q$ are $x_1, \cdots, x_{n+1}$, and $\theta'$ is obtained as $S(\theta, i(a))$, where the map $S$ is defined by: for all $\theta \in \mathbb{R}^{fv(P)}$ and $a \in \mathbb{R}$, $S(\theta, a)$ maps $x_m$ to $a$, every $x_i$ with $i < m$ to $\theta(x_i)$, and every $x_i$ with $i > m$ to $\theta(x_{i-1})$. $S$ is clearly Scott-continuous. In particular, $f_{E^0} = Q S(\theta, i(\_))$ is lower semicontinuous, so $f_{E^0}[\mu]$ makes sense. Moreover, the map $\theta \mapsto f_{E^0}(a) = Q S(\theta, i(a))$ is also Scott-continuous for every $a \in \mathbb{R}$, so the map that sends every $\theta$ to $f_{E^0}[\mu] = \lambda V \in \mathcal{O}\Gamma.\mu\{a \in \mathbb{R} \mid Q S(\theta, i(a)) \in V\}$ is also Scott-continuous. Therefore $U \stackrel{\text{def}}{=} \{P\theta \in \mathbb{R}^{fv(P)} \mid f_{E^0}[\mu] \in V\}$ is open. By construction, $L$ is in $U$, and every element of $U$ maps to an element of $V$ by $\mathcal{N}ext$. $\square$

## B.2 Soundness (Section 10.1)

**Lemma 10.11 (recap).** Let $\Sigma$ consist of strictly observable first-order constants. The weak normal forms are exactly the lazy values.

*PROOF.* It is clear that every lazy value is in weak normal form. Conversely, we show that every weak normal form $M$ is a lazy value $V^0$, by induction on the size of $M$.

We start with the case where $M$ is a constant $f$. If $\alpha(f) = 0$, then $M$ is a zero-ary constant of observable type. By the last condition of Definition 10.5, it is of basic type, and therefore it is a lazy value. If $\alpha(f) \ne 0$, then it is a lazy value of the form $f V_1 \cdots V_i$, with $i < \alpha(f)$ (namely with $i=0$).

If $M$ is of the form **score N**, then $N$ is weakly normal, since **score**[] is a weak evaluation context and $M$ is weakly normal. We apply the induction hypothesis to $N$, and we realize that because of typing, $N$ must be of the form $a$ for some zero-ary constant $a$ of type **real**. However, $M = \text{score } a$ is not weakly normal, so $M$ cannot be of the form **score N** after all.

$M$ cannot be of the form **rec N** or **sample**[μ], which are not weakly normal. Lambda-abstractions, and terms of the form **ret N**, ⟨N, P⟩, $\iota_1 N$, or $\iota_2 N$ are all lazy values.

If $M$ is of the form $\pi_1 N$, then $N$ is weakly normal, so by induction hypothesis and typing, $N$ is a pair, which would contradict the normality of $M$; similarly if $M = \pi_2 N$. If $M$ is of the form **case NPQ**, then $N$ is weakly normal, so by induction hypothesis and typing it is of the form $\iota_1 N_1$ or $\iota_2 N_2$, and that would contradict the normality of $M$ as well.

If $M$ is of the form **do x ← N; P**, then by induction hypothesis and typing $N$ is of the form **ret P**, which would contradict the fact that $M$ is weakly normal.

If $M$ is an application $NP$, then by induction hypothesis and typing, either $N$ is a $\lambda$-abstraction (which is impossible since $M$ is weakly normal), or $N$ is of the form $f M_1 \cdots M_i$ with $i < \alpha(f)$ and where $M_1, \dots, M_i$ are weakly normal. Then $M = f M_1 \cdots M_i P$, where $M_1, \dots, M_i$ and $P$ are weakly normal, hence are lazy values. By the first condition of
Definition 10.5, they are lazy values of basic types, hence are constants of arity 0. If $i + 1 = \alpha(\underline{f})$, either rule (7) would apply or $M$ would be blocked. Hence $i + 1 < \alpha(\underline{f})$, showing that $M$ is a lazy value. $\square$

**Lemma 10.12 (recap).** Let $\Sigma$ consist of strictly observable first-order constants. For every type $\tau$, $\text{Norm}_\tau$ is exactly the set of values of type $\tau$.

*PROOF.* It is clear that every value is in normal form. Conversely, we argue that every element $M$ of $\text{Norm}_\tau$ is a value, by induction on $M$. Every normal form is weakly normal, since every weak evaluation context $E^0$ is a context $E$; so $M$ is a lazy value. In order to show that it is a value, we only need to show that if it is of the form $\text{ret } N$, $\langle N, P \rangle$, $i_1 N$ or $i_2 N$, then $N$ and $P$ are values. If $M = \text{ret } N$, this is because $\text{ret}[]$ is an evaluation context, so that $N$ is a value by induction hypothesis. Similarly when $M = i_1 N$ or $M = i_2 N$. When $M = \langle N, P \rangle$, since $\langle [] , P \rangle$ is an evaluation context, by induction hypothesis $N$ is a value $V$. Since $\langle V, [] \rangle$ is a context, $P$ is a value. $\square$

**Lemma 10.13 (recap).** Let $X$ be a topological space, and let $\text{Norm}$ and $\overline{\text{Norm}}$ be two complementary open subsets of $X$. Let $\kappa: X \to \mathcal{V}X$ be a continuous map, and let us assume that for every $x \in \text{Norm}$, $\kappa(x)$ is the zero valuation. We define:

* $\kappa^{\le 0}$ as mapping every $x \in \text{Norm}$ to $\delta_x$, and every $x \in \overline{\text{Norm}}$ to the zero valuation;

* $\kappa^{\le 1} \stackrel{\text{def}}{=} \kappa + \kappa^{\le 0}$;

* $\kappa^{\le n+1} \stackrel{\text{def}}{=} (\kappa^{\le n})^{\dagger} \circ \kappa^{\le 1}$, for every $n \ge 1$.

Then:

(1) the maps $\kappa^{\le n}$ are continuous from $X$ to $\mathcal{V}X$;

(2) for every $x \in X$, the family $(\kappa^{\le n}(x)|_{\text{Norm}})_{n \ge 1}$ is monotonically increasing;

(3) the formula $\kappa^*(x) \stackrel{\text{def}}{=} \sup_{n \ge 1} \kappa^{\le n}(x)|_{\text{Norm}}$ defines a continuous map $\kappa^*$ from $X$ to $\mathcal{V}X$.

*PROOF.* 1. Since $X$ is homeomorphic to the topological coproduct $\overline{\text{Norm}} + \text{Norm}$, the continuity of $\kappa^{\le 0}$ reduces to that the unit $\eta_{\text{Norm}}$ and of the constant zero map. Then $\kappa^{\le 1}$ is continuous since $+$ is Scott-continuous on $\overline{\mathbb{R}}_+$, and by induction on $n \ge 1$, $\kappa^{\le n+1}$ is continuous as a composition of continuous maps.

2. We show that $\kappa^{\le n}(x)(U) \le \kappa^{\le n+1}(x)(U)$ for every $x \in X$ and every open subset $U$ of $\text{Norm}$ by induction on $n \in \mathbb{N}$.

In the base case $n=0$, this is obvious. Otherwise, $n \ge 1$, and $\kappa^{\le n+1}(x)(U) = \int_{y \in X} \kappa^{\le n}(y)(U) d\kappa^{\le 1}(x)$. For every $y \in X$, $\kappa^{\le n}(y)(U) \ge \kappa^{\le n-1}(y)(U)$ by induction hypothesis, so $\kappa^{\le n+1}(x)(U) \ge \int_{y \in X} \kappa^{\le n-1}(y)(U) d\kappa^{\le 1}(x) = \kappa^{\le n}(x)(U)$.

3. $\mathcal{V}X$ is a dcpo, and suprema in the dcpo of continuous maps from $X$ to $\mathcal{V}X$ are computed pointwise. $\square$

**Lemma 10.14 (recap).** Let $\Sigma$ consist of strictly observable first-order constants. For every generalized ISPCF term $M$, for every $n \in \mathbb{N}$, we have:

(1) if $M \in \text{Norm}$, then $\text{Next}^{\le n}(M) = \delta_M$;

*PROOF.* By induction on $n$. If $n=0$, then $\text{Next}^{\le 0}(M) = \delta_M$ since $M \in \text{Norm}$. If $n=1$, then $\text{Next}(M) = 0$, so $\text{Next}^{\le 1}(M) = \text{Next}(M) + \text{Next}^{\le 0}(M) = \delta_M$. If $n \ge 2$, then $\text{Next}^{\le n}(M) = (\text{Next}^{\le n-1})^{\dagger}(\text{Next}^{\le 1}(M)) = (\text{Next}^{\le n-1})^{\dagger}(\delta_M) = \text{Next}^{\le n-1}(M) = \delta_M$, by induction hypothesis. $\square$

(2) if $M = E^0[\text{sample}[\mu]]$, and $n \ge 1$, then for every $U \in \mathcal{O}\Gamma$, $\text{Next}^{\le n}(M)(U) = \int_{a \in \overline{\mathbb{R}}} \text{Next}^{\le n-1}(E^0[\text{ret } a])(U) d\mu$;

*PROOF.* Since $M = E^0[\text{sample}[\mu]] \in \overline{\text{Norm}}$, $\text{Next}^{\le 1}(M) = \text{Next}(M)$ is equal to $f_{E^0}[\mu]$, where $f_{E^0}(a) \stackrel{\text{def}}{=} E^0[\text{ret } a]$ for every $a \in \overline{\mathbb{R}}$. Therefore $\text{Next}^{\le n}(M)(U) = (\text{Next}^{\le n-1})^{\dagger}(f_{E^0}[\mu])(U) = \int_{N \in \Gamma} \text{Next}^{\le n-1}(N)(U) d f_{E^0}[\mu]$.
By the change-of-variables formula, this is equal to $\int_{a \in \mathbb{R}} Next^{\le n-1}(f_{E^0}(a))(U) d\mu = \int_{a \in \mathbb{R}} Next^{\le n-1}(E^0[\text{ret}_a])(U) d\mu$. $\square$

(3) if $M = E^0[\text{score } a]$ and $n \ge 1$, then $Next^{\le n}(M) = |a| \cdot Next^{\le n-1}(E^0[\text{ret}_*])$;

PROOF. Since $M = E^0[\text{score } a] \in \overline{\text{Norm}}$, $Next^{\le 1}(M) = Next(M) = |a| \cdot \delta_{E^0[\text{ret}_*]}$. Then, for every $U \in \mathcal{O}\Gamma$, $Next^{\le n}(M)(U) = (Next^{\le n-1})^{\dagger}(|a| \cdot \delta_{E^0[\text{ret}_*]})(U) = \int_{N \in \Gamma} Next^{\le n-1}(N)(U) d|a| \cdot \delta_{E^0[\text{ret}_*]}$, and this is equal to $|a| \cdot Next^{\le n-1}(E^0[\text{ret}_*])(U)$. $\square$

(4) if $M = E[f \underline{a_1} \cdots \underline{a_k}]$ and $n \ge 1$, then $Next^{\le n}(M)$ is equal to $Next^{\le n-1}(E[f(a_1) \cdots (a_k)])$ if $f(a_1) \cdots (a_k)$ is observable, to the zero valuation otherwise;

PROOF. Let $M = E[f \underline{a_1} \cdots \underline{a_k}]$. If $f(a_1) \cdots (a_k)$ is not observable, then $M$ is blocked, so $Next^{\le 1}(M) = 0$. For every $U \in \mathcal{O}\Gamma$, $Next^{\le n}(M)(U) = (Next^{\le n-1})^{\dagger}(0) = \int_{N \in \Gamma} Next^{\le n-1}(N)(U) d0 = 0$, so $Next^{\le n}(M) = 0$. If $f(a_1) \cdots (a_k)$ is observable, then $Next^{\le 1}(M) = Next(M) = \delta_{E[f(a_1) \cdots (a_k)]}$. It follows that $Next^{\le n}(M) = (Next^{\le n-1})^{\dagger}(\eta_{\Gamma}(E[f(a_1) \cdots (a_k)])) = Next^{\le n-1}(E[f(a_1) \cdots (a_k)])$. $\square$

(5) for every instance of a rule $L \to R$ of Figure 3 except (5), (6) and (7), if $n \ge 1$ then $Next^{\le n}(L) = Next^{\le n-1}(R)$.

PROOF. This is similar to the latter case. $\square$

LEMMA B.1. The only weak evaluation contexts $E^0$ whose type is of the form $D\sigma \vdash \tau$ are those of the form:

$$ \mathbf{do} x_n \leftarrow (\mathbf{do} x_{n-1} \leftarrow \dots (\mathbf{do} x_1 \leftarrow [] ; N_1) ; \dots ; N_{n-1}) ; N_n, $$

and then $\tau$ is a distribution type $D\tau'$.

PROOF. By induction on the size of $E^0$. This is obvious if $E^0 = []$, otherwise we see that $E^0$ must be of the form $E'^0[\mathbf{do} x \leftarrow [] ; N]$, by inspection of the evaluation context formation rules, using typing to rule out all the other possibilities. $\square$

The following linearity property is crucial for soundness. The importance of such linearity properties have already been made in [33, Proposition 5.1], where probabilistic choice was discrete, and in [17, Lemma 7.6]. Given any evaluation context $E$, we write $\llbracket E \rrbracket$ for $\llbracket \lambda x.E[x] \rrbracket$.

LEMMA B.2. Assume that all constants in $\Sigma$ are first-order constants. For every weak evaluation context $E^0$ of type $D\sigma \vdash D\tau$, $\llbracket E^0 \rrbracket$ is linear:

(1) for all $\mu, \mu' \in \mathbf{V}[\sigma]$, for every $a \in \mathbb{R}_+$, $\llbracket E^0 \rrbracket (a, \mu) = a \llbracket E^0 \rrbracket (\mu)$ and $\llbracket E^0 \rrbracket (\mu + \mu') = \llbracket E^0 \rrbracket (\mu) + \llbracket E^0 \rrbracket (\mu')$;

(2) for every dcpo $X$, for every Scott-continuous map $f: X \to \mathbf{V}[\sigma]$, $\llbracket E^0 \rrbracket \circ f^\dagger = (\llbracket E^0 \rrbracket \circ f)^\dagger$.

PROOF. By Lemma B.1, $E^0$ is of the form $\mathbf{do} x_n \leftarrow (\mathbf{do} x_{n-1} \leftarrow \dots (\mathbf{do} x_1 \leftarrow [] ; N_1) ; \dots ; N_{n-1}) ; N_n$. We prove both claims by induction on $n$, the length of $E^0$.

1. If $n=0$, this is obvious. Otherwise, we can write $E^0$ as $\mathbf{do} x_n \leftarrow E'^0 ; N_n$ where $E'^0$ has length $n-1$. We note that, for every continuous map $f: X \to \mathbf{V}Y$, $f^\dagger$ is linear, in the sense that $f^\dagger(a, \mu) = a \cdot f^\dagger(\mu)$ and $f^\dagger(\mu + \mu') = f^\dagger(\mu) + f^\dagger(\mu')$. This is clear from the definition of $f^\dagger$, see formula (1). Then:

$$ \begin{align*} \llbracket E^0 \rrbracket (a, \mu) &= (\llbracket \lambda x_n . N_n \rrbracket)^\dagger (\llbracket E'^0 \rrbracket (a, \mu)) \\ &= (\llbracket \lambda x_n . N_n \rrbracket)^\dagger (a . (\llbracket E'^0 \rrbracket (\mu))) \tag*{by induction hypothesis} \\ &= a . (\llbracket \lambda x_n . N_n \rrbracket)^\dagger (\llbracket E'^0 \rrbracket (\mu)) = a . \llbracket E^0 \rrbracket (\mu) \end{align*} $$
and similarly for $\llbracket E \rrbracket (\mu + \mu')$.

2. Again, this is clear when $n = 0$. When $n \ge 1$, we have:

$$ 
\begin{align*}
\llbracket E^0 \rrbracket \circ f^\dagger &= (\llbracket \lambda x_n \cdot N_n \rrbracket)^\dagger \circ \llbracket E'^0 \rrbracket \circ f^\dagger && \text{by induction hypothesis} \\
&= (\llbracket \lambda x_n \cdot N_n \rrbracket)^\dagger \circ (\llbracket E'^0 \rrbracket \circ f)^\dagger && \text{by the equation } (g^\dagger \circ f)^\dagger = g^\dagger \circ f^\dagger \\
&= (\llbracket E^0 \rrbracket \circ f)^\dagger. && \qed
\end{align*}
$$

We can now establish soundness. **Proposition 10.17 (recap).** Let $\Sigma$ consist of strictly observable first-order constants. For every generalized ISPCF term $M$: $D\tau$, where $\tau$ is any type, for every open subset $U$ of $\llbracket \tau \rrbracket$, $\llbracket M \rrbracket (U) \ge \text{Next}^*(M)(\bar{U})$.

**PROOF.** We show that $\llbracket M \rrbracket \rho(U) \ge \text{Next}^{\le n}(M)(\bar{U})$ for every $n \in \mathbb{N}$. If $M \in \text{Norm}$, then $\text{Next}^{\le n}(M) = \delta_M$ by Lemma 10.14, item 1. By Lemma 10.12 (and typing), $M = \text{ret} V$ for some value $V$ of type $\tau$. Hence $\llbracket M \rrbracket (U) = \delta_{\llbracket V \rrbracket}(U)$, which is equal to 1 if $\llbracket V \rrbracket \in U$, and to 0 otherwise. Since $\llbracket V \rrbracket \in U$ if and only if $V \in \bar{U}$ if and only if $\text{ret} V \in \bar{U}$, $\llbracket M \rrbracket (U) = \text{Next}^{\le n}(M)(\bar{U})$.

Henceforth, we assume that $M$ is not normal, and we prove the claim by induction on $n$. If $n = 0$, then $\text{Next}^{\le 0}(M) = 0$, so the claim is clear. Let therefore $n \ge 1$, and let us look at the possible shapes of $M$.

IF $M = E^0[\text{sample}[\mu]]$, then:

$$ 
\begin{align*}
\text{Next}^{\le n}(M)(\bar{U}) &= \int_{a \in \mathbb{R}} \text{Next}^{\le n-1}(E^0[\text{ret a}]) (\bar{U}) \, d\mu && \text{by Lemma 10.14, item 2} \\
&\le \int_{a \in \mathbb{R}} \llbracket E^0[\text{ret a}] \rrbracket (U) \, d\mu && \text{by induction hypothesis} \\
&= \int_{a \in \mathbb{R}_{\perp}} \llbracket E^0 \rrbracket (\eta_{\llbracket \text{real} \rrbracket}(a))(U) \, di[\mu]
\end{align*}
$$

by the change-of-variables formula

$$ 
\begin{align*}
&= (\llbracket E^0 \rrbracket \circ \eta_{\llbracket \text{real} \rrbracket})^\dagger (i[\mu])(U) && \text{by definition of } \dagger \\
&= \llbracket E^0 \rrbracket (\eta_{\llbracket \text{real} \rrbracket}^\dagger (i[\mu]))(U) && \text{by Lemma B.2, item 2} \\
&= \llbracket E^0 \rrbracket (i[\mu])(U) && \text{since } \eta_X^\dagger = \text{id}_{\mathcal{V}_X} \\
&= \llbracket E^0[\text{sample}[\mu]] \rrbracket (U) = \llbracket M \rrbracket (U).
\end{align*}
$$

If $M = E^0[\text{score a}]$, then:

$$ 
\begin{align*}
\text{Next}^{\le n}(M)(\bar{U}) &= |a| \cdot \text{Next}^{\le n-1}(E^0[\text{ret}_*]) (\bar{U}) \, d\mu && \text{by Lemma 10.14, item 3} \\
&\le |a| \cdot \llbracket E^0[\text{ret}_*] \rrbracket (U) && \text{by induction hypothesis} \\
&= |a| \cdot \llbracket E^0 \rrbracket (\delta_*)(U) \\
&= \llbracket E^0 \rrbracket (|a| \cdot \delta_*)(U) && \text{by Lemma B.2, item 1} \\
&= \llbracket E^0[\text{score a}] \rrbracket (U) = \llbracket M \rrbracket (U).
\end{align*}
$$
If $M = E[f \underline{a_1} \cdots \underline{a_k}]$, then we consider two cases. If $f(a_1) \cdots (a_k)$ is not observable, then $Next^{\le n}(M)(\overline{\overline{U}}) = 0$ by Lemma 10.14, item 4, and the claim is clear. If $f(a_1) \cdots (a_k)$ is observable, then:

$$
\begin{align*}
Next^{\le n}(M)(\overline{\overline{U}}) &= Next^{\le n-1}(E[f(a_1) \cdots (a_k)])(\overline{\overline{U}}) && \text{by Lemma 10.14, item 4} \\
&\le \left[ E[f(a_1) \cdots (a_k)] \right] (U) && \text{by induction hypothesis} \\
&= \left[ E[f \underline{a_1} \cdots \underline{a_k}] \right] (U) = [M](U).
\end{align*}
$$

Finally, if $M$ an instance $L$ of a rule $L \to R$ of Figure 3 except (5), (6) and (7), then by inspection $[L] = [R]$, so:

$$
\begin{align*}
Next^{\le n}(M)(\overline{\overline{U}}) &= Next^{\le n-1}(R)(\overline{\overline{U}}) && \text{by Lemma 10.14, item 5} \\
&\le [R](U) && \text{by induction hypothesis} \\
&= [L](U) = [M](U).
\end{align*}
$$

□

B.3 Adequacy (Section 10.2)

LEMMA B.3. Let $\Sigma$ consist of strictly observable first-order constants. For every string of rewrite steps $M = M_0 \to M_1 \to \dots \to M_n \to \dots$ by deterministic rules, $Next^*(M) = Next^*(M_i)$ for every $i$.

PROOF. It suffices to show that if $M \to N$ by some deterministic rule, then $Next^*(M) = Next^*(N)$. This follows from the fact that, for every $n \ge 1$, $Next^{\le n}(M) = Next^{\le n-1}(N)$ (Lemma 10.14, items 4 and 5), and by taking suprema over $n$. $\square$

LEMMA B.4. Let $\Sigma$ consist of strictly observable first-order constants.

(1) For every generalized ISPCF term $M$ of type $\tau$, there is at most one maximal string of instances of weak deterministic rules $M_0 \stackrel{\text{def}}{=} M \to M_1 \to \dots \to M_n \dots$. Every $M_i$ has type $\tau$. If $\tau$ is an observable type, and if that string stops at rank $n$, then $M_n$ is a weak value $V^0$.

(2) For every generalized ISPCF term $M$ of type $\tau$, there is at most one maximal string of instances of deterministic rules $M_0 \stackrel{\text{def}}{=} M \to M_1 \to \dots \to M_n \dots$. Every $M_i$ has type $\tau$. If $\tau$ is an observable type, either that string stops at rank $n$, then $M_n$ is a value $V$, and $Next^*(M) = \delta_V$; or else $Next^*(M) = 0$.

PROOF. The unicity of any maximal string of (weak) deterministic rules starting from $M$ is clear, as well as the fact
that every $M_i$ has type $\tau$. We now assume that $\tau$ is an observable type.

1. We consider a maximal string of weak deterministic rules stopping at rank $n$, namely $M = M_0 \to^* M_n$. We claim that $M_n$ is weakly normal. If $M_n$ is of the form $E^0[\text{sample}[\mu]]$ or $E^0[\text{score } \underline{\text{a}}]$ or $E^0[\text{do x } \leftarrow \text{ret } M; N]$, then $E^0$ has a type of the form $D\sigma \vdash \tau$. By Lemma B.1, that would imply that $\tau$ is of the form $D\tau'$ for some type $\tau'$, which is impossible since $\tau$ is observable. Since no weak deterministic rule applies to $M_n$, no weak rule at all applies, so $M_n$ is weakly normal. By Lemma 10.12, it is a weak value $V^0$.

2. We reason similarly, assuming a maximal string of deterministic rules stopping at rank $n$, $M = M_0 \to^* M_n$. Then $M_n$ is a value $V$. By Lemma B.3, $Next^*(M) = Next^*(M_n) = Next^*(V)$, and this is equal to $\delta_V$ by Lemma 10.14, item 1.

If instead the maximal string $M = M_0 \to M_1 \to \dots$ does not stop, then for every $m \in \mathbb{N}$, we have $Next^{\le m}(M) = Next^{\le m-1}(M_1) = \dots = Next^{\le 0}(M_m)$, by Lemma 10.14, items 4 and 5. Since $M_m$ is not normal, this is equal to 0. Taking suprema over $m \in \mathbb{N}$, we obtain that $Next^*(M) = 0$. $\square$
**LEMMA B.5.** Let $\Sigma$ consist of strictly observable first-order constants. Let $\tau$ be any type. If $M \to^* M'$ by weak deterministic rules, then $M R_\tau a$ if and only if $M' R_\tau a$.

*PROOF.* It suffices to show this when $M \to M'$ by one weak deterministic rule, and we show this by induction on $\tau$.

When $\tau$ is a basic type, and if $M' R_\tau a$, then either $a = \perp$, or $M' \to^* \underline{b}$ by weak deterministic rules, with $b \ge a$. In the second case, $M \to M' \to^* b$ by weak deterministic rules, so $M R_\tau a$. In the reverse direction, if $M R_\tau a$, either $a = \perp$, or $M \to^* \underline{b}$ by weak deterministic rules, with $b \ge a$. Since $M \to M'$ by a weak deterministic rule, since $\underline{b}$ is (weakly) normal, and since weak deterministic rules are deterministic by construction, the string of reduction steps $M \to^* \underline{b}$ is of the form $M \to M' \to^* \underline{b}$. Therefore $M R_\tau a$.

The argument is similar when $\tau$ is a product type $\tau_1 \times \tau_2$. The key is that, if $M \to^* \langle M_1, M_2 \rangle$ by weak deterministic rules, and if $M \to M'$ by a weak deterministic rule, then $M$ is not weakly normal, so the first string of rewrite steps must be of the form $M \to M' \to^* \langle M_1, M_2 \rangle$. Hence, if $M \to M'$ by a weak deterministic rule, then $M \to^* \langle M_1, M_2 \rangle$ by weak deterministic rules if and only if $M' \to^* \langle M_1, M_2 \rangle$ by weak deterministic rules. We reason similarly if $\tau$ is a sum type $\tau_1 + \tau_2$, where if $M \to M'$ by a weak deterministic rule, then $M \to^* \iota_i N$ by weak deterministic rules if and only if $M' \to^* \iota_i N$ by weak deterministic rules.

For arrow types $\sigma \to \tau$, we assume $M$ and $M'$ of type $\sigma \to \tau$, such that $M \to M'$ by a weak deterministic rule. Then, for every $N: \sigma, MN \to M'N$ by the same weak deterministic rule. If $M R_{\sigma \to \tau} f$, then for all $N R_\tau a, MN R_\tau f(a)$, and since $MN \to M'N$, by induction hypothesis $M'N R_\tau f(a)$; therefore $M' R_{\sigma \to \tau} f$. The fact that $M' R_{\sigma \to \tau} f$ implies $M R_{\sigma \to \tau} f$ is similar.

For distribution types $\tau \stackrel{\text{def}}{=} D\sigma$, we use a variant of that argument. We assume $M, M': D\sigma$ such that $M \to M'$ by some weak deterministic rule. Then, for every weak evaluation context $E^0, E^0[M] \to^* E^0[M']$ by the same weak deterministic rule. By Lemma B.3, $\text{Next}^*(E^0[M]) = \text{Next}^*(E^0[M'])$, from which it follows immediately that $M R_{D\sigma} \mu$ if and only if $M' R_{D\sigma} \mu$, for any $\mu$. $\square$

**LEMMA B.6.** Let $\Sigma$ consist of strictly observable first-order constants. For every type $\tau$, for every generalized ISPCF term $M$ of type $\tau$, $M R_\tau$ is a Scott-closed subset of $[\tau]$ that contains $\perp$.

*PROOF.* By induction on $\tau$. That $M R_\tau$ contains $\perp$ is clear except perhaps when $\tau$ is a distribution type $D\tau'$. In that case, the $\perp$ element of $[\tau]$ is the zero valuation 0, and $h^\dagger(0)(U)$ is equal to 0 for every $h \in [\tau \vdash D\beta]$, which trivially entails the statement.

If $\tau$ is a basic type, then $M R_\tau$ is the closed set $\{\perp\}$ if the maximal string of weak deterministic rewriting steps starting from $M$ does not stop, or $\downarrow b$ if $M \to^* \underline{b}$ by weak deterministic rules. Then, $\downarrow b$ is closed because downward closures of points are closed.

In the case of product types, either $M \to^* V^0$ by weak deterministic rules for no lazy value $V^0$, and then $M R_{\tau_1 \times \tau_2}$ is equal to $\{\perp\}$; or $M \to^* V^0$ for some uniquely determined lazy value $V^0$ by Lemma B.4, item 1. By typing and Lemma 10.12, $V^0 = \langle M_1, M_2 \rangle$ for some $M_1: \tau_1$ and $M_2: \tau_2$. Then $M R_{\tau_1 \times \tau_2}$ is equal to $(M_1 R_\sigma) \times (M_2 R_\sigma)$ union $\{\perp\}$. The latter is a finite union of Scott-closed sets, hence is Scott-closed.

In the case of sum types, we reason similarly. Either $M R_{\tau_1 + \tau_2}$ is equal to $\{\perp\}$, or $M \to^* \iota_i N$ by weak deterministic rules, and then $M R_{\tau_1 + \tau_2}$ is the set of elements $\{\perp\} \cup \{(i, b) \mid b \in N R_{\tau_i}\}$. It is easy to see that the latter is downwards closed and closed under directed suprema, hence is Scott-closed.

In the case of arrow types $\sigma \to \tau, M R_{\sigma \to \tau}$ is equal to the intersection over all $N R_\sigma a$ of the sets $\text{App}(\_, a)^{-1}(MN R_\tau)$. ($\text{App}$ is the application morphism $(g, a) \mapsto g(a)$.) This set is closed because $\text{App}$ and therefore $\text{App}(\_, a)$ is continuous for every $a$, and intersections of closed sets are closed.
In the case of distribution types $D\tau$, $M R_{D\tau}$ is the intersection of the sets $(h^\dagger(\cdot)(U))^{-1}(\llcorner \mathrm{Next}^*(E^0[M])(\overline{\Upsilon}))$ over all $E^0 R_{\tau \cup D\beta}^\perp$ $h$ and all observable open subsets $U$ of $[[\beta]]$. We conclude because downward closures of points are closed, and since $h^\dagger$ is Scott-continuous, hence also $h^\dagger(\cdot)(U)$ for every $U$. $\square$

**LEMMA B.7.** Let $\Sigma$ consist of strictly observable first-order constants. For every observable type $\beta$, for every observable element $a$ of $[[\beta]]$, $a R_\beta a$.

**PROOF.** We recall that $\underline{a}$ was defined in Definition 10.4. We show this by induction on $\beta$. If $\beta$ is a basic type, this follows from the fact that $\underline{a} \to^* \underline{a}$ (in 0 step) and $[[\underline{a}]] = a$. If $\beta$ is a product type $\beta_1 \times \beta_2$, then $a$ is of the form $(a_1, a_2)$ with $a_1$ observable in $[[\beta_1]]$ and $a_2$ observable in $[[\beta_2]]$. Then $\underline{a} \to^* \langle \underline{a}_1, \underline{a}_2 \rangle$ (in 0 step), while $\underline{a}_1 R_{\beta_1} a_1$ and $\underline{a}_2 R_{\beta_2} a_2$ by induction hypothesis. The case of sum types is similar. $\square$

**Proposition 10.20 (recap).** Let $\Sigma$ consist of strictly observable first-order constants. For every ISPCF term $M: \tau$, for all $\theta R_* \rho$, $M\theta R_\tau [[M]] \rho$.

**PROOF.** By induction on the size of $M$.

• If $M$ is a constant $f$, say of type $\sigma_1 \to \dots \to \sigma_k \to \tau$ where every $\sigma_i$ is a basic type and $\tau$ is an observable type, then we must show that for all $N_1 R_{\sigma_1} a_1, \dots, N_k R_{\sigma_k} a_k$, $f N_1 \cdots N_k R_\tau f(a_1) \cdots (a_k)$. If $f(a_1) \cdots (a_k) = \perp$, this is clear, so let us assume $f(a_1) \cdots (a_k) \neq \perp$. By the second condition of Definition 10.5, $f(a_1) \cdots (a_k)$ is observable, and every $a_i$ is different from $\perp$. Since every $\sigma_i$ is a basic type, we have $N_i \to^* \underline{a}'_i$ by weak deterministic rules for some zero-ary constant $\underline{a}'_i$ such that $a'_i \ge a_i$, for every $i$ with $1 \le i \le k$. It is easy to see that $f N_1 \cdots N_k \to^* f \underline{a}'_1 \cdots \underline{a}'_k \to f(a'_1) \cdots (a'_k)$ by weak deterministic rules; the last step is justified by the fact that $f(a'_1) \cdots (a'_k) \ge f(a_1) \cdots (a_k)$, that $f(a_1) \cdots (a_k)$ is observable, and that every element larger than an observable element is itself observable. By Lemma B.7, $f(a'_1) \cdots (a'_k) R_\tau [[f(a'_1) \cdots (a'_k)]] \rho = f(a'_1) \cdots (a'_k)$. Using Lemma B.5, we deduce that $f N_1 \cdots N_k R_\tau f(a'_1) \cdots (a'_k)$. Since $f(a'_1) \cdots (a'_k) \ge f(a_1) \cdots (a_k)$, and since $f N_1 \cdots N_k R_\tau$ is Scott-closed, hence downwards-closed (Lemma B.6), we obtain that $f N_1 \cdots N_k R_\tau f(a_1) \cdots (a_k)$, as desired.

• If $M$ is a variable, this is by the assumption $\theta R_* \rho$.

• If $M = \mathbf{sample}[\mu]$, we must show that for all $E^0 R_{\mathbf{real}}^\perp \to D\beta$ $h$, for every observable open subset $U$ of $[[\beta]]$, $\mathrm{Next}^*(E^0[\mathbf{sample}[\mu]])(\overline{\Upsilon}) \ge h^\dagger(\mu)(U)$. By Lemma 10.14, item 2, and taking suprema over $n \ge 1$, $\mathrm{Next}^*(E^0[\mathbf{sample}[\mu]])(\overline{\Upsilon})$ is equal to $\int_{a \in \mathbb{R}} \mathrm{Next}^*(E^0[\mathrm{ret} \underline{a}])(\overline{\Upsilon}) d\mu$. By Lemma B.7, $\underline{a} R_{\mathbf{real}} a$ for every $a \in \mathbb{R}$. In particular, $\underline{a} R_{\mathbf{real}} i(a)$ for every $a \in \mathbb{R}$. Since $E^0 R_{\mathbf{real}}^\perp \to D\beta$ $h$, $\mathrm{Next}^*(E^0[\mathrm{ret} \underline{a}])(\overline{\Upsilon}) \ge h(a)(U)$ for every $a \in \mathbb{R}$. From this, we conclude that $\mathrm{Next}^*(E^0[\mathbf{sample}[\mu]])(\overline{\Upsilon}) \ge \int_{a \in \mathbb{R}} h(a)(U) d\mu = h^\dagger(\mu)(U)$.

• If $M = \mathbf{score} N$, we must show that for all $E^0 R_{\mathbf{unit}}^\perp \to D\beta$ $h$, for every observable open subset $U$ of $[[\beta]]$, $\mathrm{Next}^*(E^0[M\theta])(\overline{\Upsilon}) \ge h^\dagger(|a|\cdot\delta_*)(U)$ where $a \stackrel{\text{def}}{=} [[N]] \rho$. We observe that $h^\dagger(|a|\cdot\delta_*) = |a|\cdot h(\cdot)$. Hence the claim is clear if $|a| = 0$, notably if $a = \perp$. Let us assume that $a \neq \perp$. Then $N\theta R_{\mathbf{real}} a$, by induction hypothesis. By definition of $R_{\mathbf{real}}$, $N\theta \to^* \underline{a}'$ by weak deterministic rules, for some zero-ary constant $\underline{a}'$ such that $\underline{a}' \ge a$.

Since $E^0 R_{\mathbf{unit}}^\perp \to D\beta$ $h$, and since $\underline{a} R_{\mathbf{unit}}^* (\text{by the case of zero-ary constants, already treated})$, $\mathrm{Next}^*(E^0[\mathrm{ret} \underline{a}^*])(\overline{\Upsilon}) \ge h(\cdot)(U)$. We have $N\theta \to^* \underline{a}'$ by weak deterministic rules, so $E^0[M\theta] = E^0[\mathbf{score} N\theta] \to^* E^0[\mathbf{score} \underline{a}']$ by weak deterministic rules. By Lemma B.3, $\mathrm{Next}^*(E^0[M\theta])(\overline{\Upsilon}) = \mathrm{Next}^*(E^0[\mathbf{score} \underline{a}']) (\overline{\Upsilon})$, which is equal to $|a'| \cdot \mathrm{Next}^*(E^0[\mathrm{ret} \underline{a}^*])(\overline{\Upsilon})$ by Lemma 10.14, item 3, hence is larger than or equal to $|a'| \cdot h(\cdot)(U)$. We verify that $|a'| \ge |a|$, owing to the fact that $\underline{a}' \ge a$. Hence $\mathrm{Next}^*(E^0[M\theta])(\overline{\Upsilon}) \ge |a| \cdot h(\cdot)(U) = h^\dagger(|a|\cdot\delta_*)(U)$.
• If $M = \lambda x.N : \sigma \to \tau$, then we must show that for all $P R_\sigma$ $a$, $(M\theta)P R_\tau [[M]] \rho(a)$. By induction hypothesis, we have $N\theta[x := P] R_\tau [[N]] \rho[x \mapsto a]$. Since $(M\theta)P \to N\theta[x := P]$, we conclude by Lemma B.5.

• The case where $M$ is an application is immediate.

• If $M = \mathbf{rec} N$, where $N : \sigma \to \sigma$, then let $f \stackrel{\text{def}}{=} [[N]] \rho$. By induction hypothesis, $N R_\sigma \to \sigma f$, so: (*) for all $P R_\sigma$ $a$, we have $(N\theta)P R_\sigma f(a)$. We show that $M\theta R_\sigma f^n(\perp)$ for every $n \in \mathbb{N}$, by induction on $n$. If $n = 0$, then $f^0(\perp) = \perp$ is in $M\theta R_\sigma$ by Lemma B.6. If $n \ge 1$, then $N\theta(M\theta) R_\sigma f (f^{n-1}(\perp))$, using (*) and the induction hypothesis. Now $M\theta = \mathbf{rec}(N\theta) \to N\theta(M\theta)$ by a weak deterministic rule, so $M\theta R_\sigma f^n(\perp)$, by Lemma B.5. Now that we have shown that $M\theta R_\sigma f^n(\perp)$, namely that $f^n(\perp)$ is in $M\theta R_\sigma$ for every $n \in \mathbb{N}$, we use the fact that $M\theta R_\sigma$ is Scott-closed (Lemma B.6) and we conclude that $[[M]] \rho = \text{lfp}(f) = \sup_{n \in \mathbb{N}} f^n(\perp)$ is in $M\theta R_\sigma$.

• If $M = \mathbf{ret} N$, with $N : \sigma$, then we must show that for all $E^0 R_{\sigma \vdash D\beta}^\perp h$, for every observable open subset $U$ of $[[\beta]]$, $\mathit{Next}^*(E^0[M\theta])(\overline{\Upsilon}) \ge h^\dagger(\delta_{[[N]]\rho})(U)$. By induction hypothesis, $N\theta R_\sigma [[N]] \rho$, so by definition of $R_{\sigma \vdash D\beta}^\perp$, we obtain $\mathit{Next}^*(E^0[\mathbf{ret} N\theta])(\overline{\Upsilon}) \ge h([[[N]] \rho](U)$; this is exactly what we want to prove.

• If $M = \mathbf{do} x_\sigma \to N; P : D\tau$, then we must show that for all $E^0 R_{\tau \vdash D\beta}^\perp h$, for every observable open subset $U$ of $[[\beta]]$, $\mathit{Next}^*(E^0[M\theta])(\overline{\Upsilon}) \ge h^\dagger(\llbracket \lambda x_\sigma . P \rrbracket \rho)^\dagger(\llbracket N \rrbracket \rho))(U) = (h^\dagger \circ \llbracket \lambda x_\sigma . P \rrbracket \rho)^\dagger(\llbracket N \rrbracket \rho))(U)$, where the last equality is by the monad equation $g^\dagger \circ f^\dagger = (g^\dagger \circ f)^\dagger$.

We consider the weak evaluation context $E^{\prime 0} \stackrel{\text{def}}{=} E^0[\mathbf{do} x_\sigma \to []; P\theta]$, and we claim that $E^{\prime 0} R_{\sigma \vdash D\beta}^\perp h^\dagger \circ \llbracket \lambda x_\sigma . P \rrbracket \rho$. This means showing that for all $Q R_\sigma$ $b$, for every observable open subset $V$ of $[[D\beta]]$, $\mathit{Next}^*(E^{\prime 0}[\mathbf{ret} Q])(\overline{\Upsilon}) \ge h^\dagger(\llbracket \lambda x_\sigma . P \rrbracket \rho(b))(V)$. The right-hand side is equal to $h^\dagger(\llbracket P \rrbracket \rho[x \mapsto b])(V)$. Since $E^{\prime 0}[\mathbf{ret} Q] = E^0[\mathbf{do} x_\sigma \to \mathbf{ret} Q; P\theta] \to E^0[P\theta[x := Q]]$ by a weak deterministic rule, and by Lemma B.3, the left-hand side $\mathit{Next}^*(E^{\prime 0}[\mathbf{ret} Q])(\overline{\Upsilon})$ is equal to $\mathit{Next}^*(E^0[P\theta[x := Q]])(\overline{\Upsilon})$. The latter is larger than or equal to $h^\dagger(\llbracket P \rrbracket \rho[x \mapsto b])(V)$ since $P\theta[x := Q] R_{D\tau} [[P]] \rho[x \mapsto b]$ by induction hypothesis and since $E^0 R_{\tau \vdash D\beta}^\perp h$.

Since $E^{\prime 0} R_{\sigma \vdash D\beta}^\perp h^\dagger \circ \llbracket \lambda x_\sigma . P \rrbracket \rho$ and since by induction hypothesis $N\theta R_{D\sigma} [[N]] \rho$, we have $\mathit{Next}^*(E^{\prime 0}[N\theta])(\overline{\Upsilon}) \ge (h^\dagger \circ \llbracket \lambda x_\sigma . P \rrbracket \rho)^\dagger(\llbracket N \rrbracket \rho)(U)$, and this is exactly what we had to prove.

• If $M = \langle M_1, M_2 \rangle$, with $M_1 : \tau_1$ and $M_2 : \tau_2$, then $M\theta \to^* \langle M_1\theta, M_2\theta \rangle$ by weak deterministic rules (vacuously), and $M_1\theta R_{\tau_1} [[M_1]] \rho, M_2\theta R_{\tau_2} [[M_2]] \rho$, by induction hypothesis.

• If $M = \pi_1 N$, with $N : \tau_1 \times \tau_2$, then $N\theta R_{\tau_1 \times \tau_2} [[N]] \rho$ by induction hypothesis. If $[[N]] \rho = \perp$, then $[[M]] \rho = \perp$, and therefore $M\theta R_{\tau_1 \times \tau_2} = [[M]] \rho$, by Lemma B.6. Otherwise, $[[N]] \rho$ is of the form $(a_1, a_2)$ with $a_1 \ne \perp$ or $a_2 \ne \perp$. By definition of $R_{\tau_1 \times \tau_2}$, $N\theta \to^* \langle N_1, N_2 \rangle$ by weak deterministic rules in such a way that $N_1 R_{\tau_1}$ $a_1$ and $N_2 R_{\tau_2}$ $a_2$. We note that $M\theta = \pi_1 N\theta \to^* \pi_1 \langle N_1, N_2 \rangle \to N_1$ by weak deterministic rules, so $M\theta R_{\tau_1}$ $a_1 = [[M]] \rho$, using Lemma B.5.

The case $M = \pi_2 N$ is similar.

• If $M = \iota_1 N : \tau_1 + \tau_2$, then vacuously $M\theta \to^* \iota_1 N\theta$ by weak deterministic rules. By induction hypothesis, $N\theta R_{\tau_1} [[N]] \rho$, so $M\theta R_{\tau_1 + \tau_2} (1, [[N]] \rho) = [[M]] \rho$.

The case $M = \iota_2 N$ is similar.

• If $M = \mathbf{case} N P_1 P_2 : \tau$, with $N : \tau_1 + \tau_2$, then by induction hypothesis $N\theta R_{\tau_1 + \tau_2} [[N]] \rho$. If $[[N]] \rho = \perp$, then $[[M]] \rho = \perp$, so $M\theta R_\tau [[M]] \rho$, by Lemma B.6. Otherwise, $[[N]] \rho = (i, b)$ for some $i \in \{1, 2\}$ and $b \in \llbracket \tau_i \rrbracket$. By definition of $R_{\tau_1 + \tau_2}$, $N\theta \to^* \iota_i N'$ by weak deterministic rules, in such a way that $N' R_{\tau_i}$ $b$. Then $M\theta \to^* \mathbf{case}(\iota_i N')(P_1\theta)(P_2\theta) \to P_i \theta N'$ by weak deterministic rules. By induction hypothesis, $P_i \theta R_{\tau_i \to \tau} [[P_i]] \rho$, so $P_i \theta N' R_\tau [[P_i]] \rho(b)$. By Lemma B.5, $M\theta R_\tau [[P_i]] \rho(b) = [[M]] \rho$. $\square$
**Lemma 10.22 (recap).** Let $\Sigma$ consist of strictly observable first-order constants. For every observable type $\beta$, for every generalized ISPCF term $N: \beta$, for every $b \in [[\beta]]$, if $N R_\beta b$ then either $b$ is not observable, or $b$ is observable and $N \to^* V$ by deterministic rules for some value $V: \beta$ such that $[[V]] \ge b$.

**PROOF.** We show that $N R_\beta b$ and the fact that $b$ is observable together imply the existence of a value $V: \beta$ such that $[[V]] \ge b$, by induction on $R_\beta$. If $\beta$ is a basic type, then this is by definition of $R_\beta$. If $\beta$ is a product type $\beta_1 \times \beta_2$, then let us write $b$ as $(b_1, b_2)$, where $b_1 \neq \perp$ and $b_2 \neq \perp$ since $b$ is observable. Since $b \neq \perp$, by definition of $R_{\beta_1 \times \beta_2}$, $M \to^* \langle M_1, M_2 \rangle$ by weak deterministic rules, for some $M_1 R_{\tau_1} b_1$ and $M_2 R_{\tau_2} b_2$. By induction hypothesis, $M_1 \to^* V_1$ and $M_2 \to^* V_2$ by weak deterministic rules, for some values $V_1$ and $V_2$ such that $[[V_1]] \ge b_1$, $[[V_2]] \ge b_2$. Then $M \to^* \langle M_1, M_2 \rangle \to^* \langle V_1, M_2 \rangle \to^* \langle V_1, V_2 \rangle$ by (non-weak) deterministic rules. The term $V \stackrel{\text{def}}{=} \langle V_1, V_2 \rangle$ is a value, and $[[V]] \ge (b_1, b_2) = b$. The case of sum types is similar. $\square$

We can now establish adequacy. **Theorem 10.23 (recap).** Let $\Sigma$ consist of strictly observable first-order constants. For every observable type $\beta$, for every generalized ISPCF term $M: D\beta$, for every observable open subset $U$ of $[[\beta]]$, $[[M]](U) = \text{Next}^*(M)(\bar{U})$.

**PROOF.** We consider the empty weak evaluation context $E^0 \stackrel{\text{def}}{=} []$, and we claim that $E^0 R_{\beta \vdash D\beta}^{\perp} \eta_{[[\beta]]}$. In order to show this, we need to show that for all $N R_\beta b$, for every observable open subset $U$ of $[[\beta]]$, $\text{Next}^*(E^0[\text{ret } N])(\bar{U}) \ge \delta_b(U)$. If $b \notin U$, then $\delta_b(U) = 0$, and this is obvious.

Otherwise, $\delta_b(U) = 1$. Since $b \in U$ and since $U$ is observable, $b$ is an observable element of $[[\beta]]$. Since $N R_\beta b$, Lemma 10.22 tells us that $N \to^* V$ by deterministic rules for some value $V: \beta$ such that $[[V]] \ge b$. Since $U$ is upwards closed, $[[V]]$ is in $U$. Therefore $V$ is in $\bar{U}$, and $\text{ret } V$ is in $\bar{\bar{U}}$.

We note that since $N \to^* V$ by deterministic rules, $\text{ret } N \to^* \text{ret } V$ by deterministic rules as well. By Lemma B.3, $\text{Next}^*(E^0[\text{ret } N]) = \text{Next}^*(\text{ret } N)$ is equal to $\text{Next}^*(\text{ret } V)$. By Lemma 10.14, item 1, (and taking suprema over all $n$) since $\text{ret } V$ is a normal form, $\text{Next}^*(\text{ret } V)(\bar{\bar{U}}) = \delta_{\text{ret } V}(\bar{\bar{U}}) = 1 = \delta_b(U)$.

Now that we have proved $E R_{\beta \vdash D\beta}^{\perp} \eta_{[[\beta]]}$, we apply it to $M R_{D\beta} [[M]]$ (Corollary 10.21), and, noting that $E = []$ is a weak evaluation context, we obtain that $\text{Next}^*(E[M])(\bar{\bar{U}}) \ge (\eta_{[[\beta]]})^{\dagger}([[[M]]](U)) = [[M]](U)$. The converse inequality is by soundness (Proposition 10.17). $\square$

## B.4 The sampling-based operational semantics (Section 12.2)

**Lemma 12.5 (recap).** Under the assumptions of Definition 12.1, for every open subset $U$ of Norm, the maps $\sigma_k[U]$ ($k \in \mathbb{N}$) and $\sigma[U]$ are lower semicontinuous from $\Gamma \times \{0, 1\}^\mathbb{N}$ to $\mathbb{R}_+$.

**PROOF.** We recall that lower semicontinuous simply means continuous, provided that we equip $\mathbb{R}_+$ with its Scott topology, which we now assume.

In order to simplify the proof, we use the following result by Ershov [18, Proposition 2]: given a c-space $X$ (an $\alpha$-space in Ershov's terminology, e.g., a continuous poset with its Scott topology), and two topological spaces $Y$ and $Z$, a function $f: X \times Y \to Z$ is separately continuous if and only if it is jointly continuous. Joint continuity is ordinary continuity from $X \times Y$ with the product topology. Separate continuity means that $f(x, \_)$ and $f(\_, y)$ are continuous for fixed $x$ and $y$ respectively. This applies here, as $\Gamma'$ is a continuous poset.

Since suprema of lower semicontinuous maps are lower semicontinuous, it suffices to show that $\sigma_k[U]$ is lower semicontinuous for every $k \in \mathbb{N}$, which we do by induction on $k$.
We fix a template $M_0$, and we show that $\sigma_k[U]$ is continuous from the product of the space of generalized ISPCF terms of shape $M_0$ with $\{0, 1\}^N$ to $\overline{\mathbb{R}}_+$. We only need to prove separate continuity.

If $k=0$, then $\sigma_0[U](M,s) = 1$ if $M$ is normal, 0 otherwise. For $M$ fixed, this is constant hence continuous in $s$. For $s$ fixed, we note that normality only depends on the shape (here, $M_0$). Hence $\sigma_0[U](\_, s)$ is constant, hence continuous, on the subspace of generalized ISPCF terms of shape $M_0$.

Let us assume $k \ge 1$. If the unique $\to_s$ step from $(M, i, r)$ is by applying a rule $L \to R$ of $L \to R$ of Figure 3 except (5), (6) and (7), then we note that the same rule would apply if we replaced $M$ by any other term with the same shape $M_0$. Then $\sigma_k[U](M, s) = \sigma_{k-1}[U](R, s)$, and we apply the induction hypothesis.

In the case of **sample**, $M = E[\text{sample}[\lambda_1]]$, and if $(M, 0, 1) \to_s^{\le k} (M', i', r')$ for some $M' \in U$, then $(M, 0, 1) \to_s (E[\text{ret num}(s[0])], 1, 1) \to_s^{\le k-1} (M', i', r')$, where $r' = \sigma_k[U](M, s)$. We then have $(E[\text{ret num}(s[0])], 0, 1) \to_{\uparrow s}^{\le k-1} (M', i' - 1, r')$ by Lemma 12.3, hence $r' = \sigma_k[U](M, \uparrow s) = \sigma_{k-1}[U](E[\text{ret num}(s[0])], \uparrow s)$. For $M$ fixed, we see that the composition of the maps $s \mapsto s[0] \mapsto \text{num}(s[0])$ is continuous from $\{0, 1\}^N$ to $\mathbb{R}$, using Lemma 9.3; also, $s \mapsto \uparrow s$ is continuous. As in the proof of Proposition 10.8, the map $a \in \mathbb{R} \mapsto E[\text{ret a}]$ is continuous, so $\sigma_k[U](M, s)$ defines a continuous function of $s$. For $s$ fixed, this is the composition of the continuous function that maps every term $M = E[\text{sample}[\lambda_1]]$ of shape $M_0$ to $E[\text{ret a}]$ (where $a \stackrel{\text{def}}{=} \text{num}(s[0])$) with $s_{k-1}[U](\_, \uparrow s)$, hence is continuous as well.

In the case of **score**, we have $M = E[\text{score a}]$, and assuming that $(M, 0, 1) \to_s^{\le k} (M', i', r')$ for some $M' \in U$, we have $(M, 0, 1) \to_s (E[\text{ret*}, 0, |a|) \to_s^{\le k-1} (M', i', r')$, and $r' = \sigma_k[U](M, s)$. In particular, if $|a| \ne 0$ then $(E[\text{ret*}, 0, 1) \to_s^{\le k-1} (M', i', r'/|a|)$ by Lemma 12.4 (final part), so $\sigma_{k-1}[U](E[\text{ret*}], s) = r'/|a|$. Therefore $\sigma_k[U](M, s) = |a|\cdot\sigma_{k-1}[U](E[\text{ret*}], s)$. We see that this holds also when $|a| = 0$, using the first part of Lemma 12.4, and also when $(M, 0, 1) \to_s^{\le k} (M', i', r')$ for no $M' \in U$, in which case both sides of the equality are 0. By induction hypothesis, $\sigma_{k-1}$ is continuous. The map $M = E[\text{score a}] \mapsto E[\text{ret*}]$ is continuous, by a similar argument as in Proposition 10.8. The map $M = E[\text{score a}] \mapsto a$ is also clearly continuous, the map $a \mapsto |a|$ is continuous from $\mathbb{R}_\perp$ to $\overline{\mathbb{R}}_+$, and product is Scott-continuous on $\overline{\mathbb{R}}_+$, so $\sigma_k[U](\_, s)$ is continuous, for every fixed $s$. For $M = E[\text{score a}]$ fixed, $\sigma_k[U](M, \_) = |a|\cdot\sigma_{k-1}[U](E[\text{ret*}], \_)$ is obviously continuous. Hence $\sigma_k[U]$ itself is continuous.

In case $M = E[\underline{f \ a_1 \cdots a_k}]$ where $k = \alpha(\underline{f}) \ne 0$, then either $f(a_1) \cdots (a_k)$ is observable and $\sigma_k[U](M, s) = \sigma_{k-1}[U](E[\underline{f(a_1) \cdots (a_k)}]), s)$, or else $\sigma_k[U](M, s) = 0$. For $M$ fixed, this defines a continuous map in $s$. We now consider $s$ fixed. The function that maps every term $M$ as above, of shape $M_0$, to the tuple of (denotations of) constants of type **real** among $\underline{a_1}, \dots, \underline{a_k}$ is continuous, hence also the function that maps $M$ (of given shape $M_0$) to $f(a_1) \cdots (a_k)$. In particular the set $V$ of generalized ISPCF terms of shape $M_0$ such that $f(a_1) \cdots (a_k)$ is observable is open. Let $g$ be the function that maps every $M = E[\underline{f \ a_1 \cdots a_k}]$ in $V$ to $E[\underline{f(a_1) \cdots (a_k)}]$. This is continuous. The inverse image of every non-trivial Scott-open subset $]a, +\infty]$ of $\overline{\mathbb{R}}_+$ (namely, $a > 0$) by $\sigma_k[U](\_, s)$ is equal to $g^{-1}(\sigma_{k-1}[U](\_, s)^{-1}]a, +\infty)]$ is then open, showing that $\sigma_k[U](\_, s)$ is continuous. $\square$

**Proposition 12.6 (recap).** Assume that all constants in $\Sigma$ are first-order constants, and that the only available term of the form **sample**[$\mu$] is **sample**[$\lambda_1$], where $\lambda_1$ is Lebesgue measure on $[0, 1]$. For every open subset $U$ of Norm, for every generalized ISPCF term $M$, $P[M \to U] = \text{Next}^*(M)(U)$.

**PROOF.** We show that $\int_{s \in \{0,1\}^N} \sigma_k[U](M,s) dv = \text{Next}^{\le k}(M)(U)$ by induction on $k \in \mathbb{N}$. The result will follow by taking suprema over $k$.

When $k=0$, $\text{Next}^0(M)(U)$ is equal to $\delta_M(U)$ if $M \in \text{Norm}$, to 0 otherwise, hence to $\chi_U(M)$ in all cases. For every $s \in [0, 1]^N$, $\sigma_0[U](M, s)$ is equal to $\chi_U(M)$, and since $v$ is a probability distribution, $\int_{s \in \{0,1\}^N} \sigma_k[U](M, s) dv = \chi_U(M)$. When $k \ge 1$, we look at the shape of $M$, and we use Lemma 10.14 to evaluate $\text{Next}^{\le k}(M)(U)$.
If $M \in \text{Norm}$, then $\text{Next}^{\leq k}(M)(U) = \delta_M(U) = \chi_U(M)$. Also, $\sigma_k[U](M) = \chi_U(M)$, so $\int_{s \in \{0,1\}^N} \sigma_k[U](M,s) dv = \chi_U(M)$.

We arrive at the main case of the proof. If $M = E[\text{sample}[\mu]]$, where necessarily $\mu = \lambda_1$, then, as in the proof of Lemma 12.5, $\sigma_k[U](M, \uparrow s) = \sigma_{k-1}[U](E[\text{ret num}(s[0])], \uparrow s)$, so:

$$ \int_{s \in \{0,1\}^N} \sigma_k[U](M,s) dv = \int_{s \in \{0,1\}^N} \sigma_{k-1}[U](E[\text{ret num}(s[0])], \uparrow s) dv. $$

We now use the change-of-variables formula with respect to the homeomorphism split: $s \in \{0,1\}^N \mapsto (s[0], \uparrow s) \in (\{0,1\}^N)^2$ (see Lemma 9.4). Since split[v] = v $\otimes$ v, and using Proposition 4.1:

$$ \begin{aligned} \int_{s \in \{0,1\}^N} \sigma_k[U](M,s) dv &= \int_{t \in \{0,1\}^N} \left( \int_{(s' \in \{0,1\}^N)} \sigma_{k-1}[U](E[\text{ret num}(t)], s') dv \right) dv \\ &= \int_{t \in \{0,1\}^N} \text{Next}^{\leq k-1}(E[\text{ret num}(t)]) (U) dv \end{aligned} $$

by induction hypothesis

$$ = \int_{a \in \mathbb{R}} \text{Next}^{\leq k-1}(E[\text{ret a}]) (U) d\lambda_1 $$

by the change-of-variables formula and Lemma 9.3

$$ = \text{Next}^{\leq k}(M)(U), $$

by Lemma 10.14, item 2.

If $M = E[\text{score a}]$, then, as in the proof of Lemma 12.5, $\sigma_k[U](M,s) = |a|\cdot\sigma_{k-1}[U](E[\text{ret *}], s)$. Hence:

$$ \begin{aligned} \int_{s \in \{0,1\}^N} \sigma_k[U](M,s) dv &= \int_{s \in \{0,1\}^N} |a| \cdot \sigma_{k-1}[U](E[\text{ret *}], s) dv \\ &= |a| \cdot \text{Next}^{\leq k-1}(E[\text{ret *}], s)(U) = \text{Next}^{\leq k}(M)(U), \end{aligned} $$

by induction hypothesis and Lemma 10.14, item 3. The remaining cases are equally easy, and left to the reader. $\square$

<figure><img src="image_6.png" /></figure>