# A Domain-Theoretic Approach to Statistical Programming Languages

Jean Goubault-Larrecq  Université Paris-Saclay, CNRS, ENS Paris-Saclay,
Laboratoire Méthodes Formelles, 91190, Gif-sur-Yvette, France
0000-0001-5879-3304 Xiaodong Jia  School of Mathematics, Hunan University,
Changsha, Hunan 410082, China  Department of Computer Science, Tulane
University, New Orleans, LA 70118, USA  0000-0001-9310-6143 Clément Théron
Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes
Formelles, 91190, Gif-sur-Yvette, France  0000-0003-2703-4289

###### Abstract

We give a domain-theoretic semantics to a statistical programming language,
using the plain old category of dcpos, in contrast to some more sophisticated
recent proposals. Remarkably, our monad of minimal valuations is commutative,
which allows for program transformations that permute the order of independent
random draws, as one would expect. A similar property is not known for Jones
and Plotkin’ s monad of continuous valuations. Instead of working with true
real numbers, we work with exact real arithmetic, providing a bridge towards
possible implementations. (Implementations by themselves are not addressed
here.) Rather remarkably, we show that restricting ourselves to minimal
valuations does not restrict us much: _all_ measures on the real line can be
modeled by minimal valuations on the domain $\mathbf{I}\mathbb{R}_{\bot}$ of
exact real arithmetic. We give three operational semantics for our language,
and we show that they are all adequate with respect to the denotational
semantics. We also explore quite a few examples in order to demonstrate that
our semantics computes exactly as one would expect, and in order to debunk the
myth that a semantics based on continuous maps would not be expressive enough
to encode measures with non-compact support using only measures with compact
support, or to encode measures via non-continuous density functions, for
instance. Our examples also include some useful, non-trivial cases of
distributions on higher-order objects.

##  1 Introduction

The purpose of this paper is to give a simple, domain-theoretic semantics to
statistical programming languages.

Statistical programming languages such as Church [Goodman et al., 2008],
Anglican [Wood et al., 2014], WebPPL [Goodman and Stuhlmüller, 2014] or
Venture [Mansinghka et al., 2014], were introduced as a convenient means to
describe and implement so-called stochastic generative processes. Those are
randomized programs that describe probability distributions.

Initial proposals focused on implementations. One of the first proposals for a
formal semantics of such a language, SFPC, is due to Vákár et al. [Vákár et
al., 2019], and is based on _quasi-Borel predomains_ , a notion that expands
on the clever notion of _quasi-Borel spaces_ [Heunen et al., 2017], with
additional domain-theoretic structure.

The constructions of [Vákár et al., 2019] are rather involved, and one may
wonder there would exist simpler denotational semantics for such languages. We
will give one, based on domain theory alone. Domain theory is probably one of
the oldest mathematical basis for denotational semantics [Scott, 1969]. It is
a common belief that it would be inadequate for giving semantics to
probabilistic languages. This may be due to a superficial reading of a famous
paper by A. Jung and R. Tix [Jung and Tix, 1998]. And indeed, there are
several purely domain-theoretic semantics of probabilistic languages [Jones,
1990, Goubault-Larrecq, 2015, Goubault-Larrecq, 2019].

However, it is true that statistical probabilistic languages present
additional challenges to the semanticist. Those are caused by several
additional features that one must take into account: a native type of real
numbers, continuous distributions, and perhaps most importantly, _soft
constraints_ [Staton et al., 2016]. The latter is a convenient way of
implementing the computation of conditional distributions, or smoothed
versions therefore, and is implemented by a primitive called
$\boldsymbol{\mathtt{score}}$ in SFPC.

One difference between the quasi-Borel semantics of SFPC [Vákár et al., 2019],
or that of PCFSS [Dal Lago and Hoshino, 2019], or that of PPCF [Ehrhard et
al., 2018], with our domain-theoretic semantics does not lie in probabilities
or soft constraints, but with the way we handle real numbers. SFPC, PCFSS, and
PPCF rely on _true_ real numbers, that is, values of type
$\boldsymbol{\mathtt{real}}$ are interpreted as elements of $\mathbb{R}$. We
interpret values of type $\boldsymbol{\mathtt{real}}$ as so-called _exact_
real numbers, namely as elements of a dcpo $\mathbf{I}\mathbb{R}_{\bot}$ of
interval approximations of real numbers, as in RealPCF and other proposals for
so-called exact real arithmetic [Boehm et al., 1986, Lester, 1992, Sünderhauf,
1995, Escardó, 1996, Escardó, 1996, Edalat et al., 1997, Plume, 1998, Marcial-
Romero, 2004, Ho, 2013]. This is the most natural choice with domain-theoretic
semantics, as $\mathbb{R}$ itself is not a dcpo (more precisely, the topology
of $\mathbb{R}$ cannot be obtained as a Scott topology), but embeds naturally
in a domain of interval approximations. This is also a natural bridge to
implementations; although we will not pursue this topic in depth, the final
section of this paper will give hints.

#### Contributions.

The main contribution of this paper is, therefore, a simple, purely domain-
theoretic denotational semantics for a statistical programming language with
exact real arithmetic, continuous distributions and soft constraints,
featuring full recursion. Additionally, and as in previous proposals such as
[Vákár et al., 2019], our monad of so-called _minimal valuations_ implementing
probabilistic choice is commutative. This is crucial in establishing the
correctness of run-of-the-mill program transformations such as permuting the
order in which two independent random variables are drawn. In domain-theoretic
semantics of probabilistic programming languages based on Jones and Plotkin’s
continuous valuations [Jones and Plotkin, 1989, Jones, 1990], it was not known
how to achieve this, at least until recent work by Jia, Lindenhovius, Mislove
and Zamdzhiev [Jia et al., 2021]. (We made that discovery at the same time
that they did: see the final related work section for details.) For the
moment, let us just say that there are two differences between our work and
theirs. The less significant one is probably that we work with (minimal)
valuations that are unbounded, as required to give semantics to
$\boldsymbol{\mathtt{score}}$, while they work with subprobability valuations.
The more significant one is that they do not handle _continuous_
distributions. It is a priori unclear which continuous distributions on
$\mathbb{R}$ can be represented as _minimal_ valuations. Being minimal,
indeed, is a genuine restriction: as we will see, Lebesgue measure is a
continuous valuation on $\mathbb{R}$ that is not minimal. In spite of this,
and this is perhaps the most pleasing aspect of the current work, _all_
measures on $\mathbb{R}$—including Lebesgue measure—can be realized as minimal
valuations on $\mathbf{I}\mathbb{R}_{\bot}$, as we will show in Section 6. We
will also provide an extensive list of examples in Section 9, by which we hope
to demonstrate that our approach is capable of defining a rich set of
distributions, including distributions on higher-order objects.

#### Outline.

We give some preliminary definitions in Section 2, where we also describe some
of the challenges in more detail. In Section 3, we recapitulate the
construction and basic properties of the monad $\mathbf{V}$ of continuous
valuations. The commutativity of that monad is equivalent to a form of the
Fubini-Tonelli theorem, which in its most basic form expresses an interchange
property for double integrals. Rather subtly, and perhaps paradoxically, such
a Fubini-Tonelli theorem is easy to obtain for the $\mathbf{V}$ monad on the
category ${\mathbf{Top}}$ of topological spaces, but is an open problem on the
subcategory ${\mathbf{Dcpo}}$ of dcpos. We will explain the issue in Section
4, where we will see that everything boils down to the fact that products in
${\mathbf{Dcpo}}$ are in general different from products in the larger
category ${\mathbf{Top}}$.

In order to obtain a Fubini-Tonelli theorem on ${\mathbf{Dcpo}}$, we may opt
to restrict to, say, continuous dcpos, but this runs into some trouble, as we
will have seen in Section 2. Our solution is much simpler: we restrict
continuous valuations to a submonad $\mathbf{V}_{m}$ of so-called _minimal_
valuations, and we show that $\mathbf{V}_{m}$ is a commutative monad on
${\mathbf{Dcpo}}$ in Section 5. Now, since we will restrict our valuations to
be minimal, doesn’t this exclude some interesting continuous distributions?
And indeed that will seem to be the case: as we have already mentioned, we
will show that Lebesgue measure, seen as a continuous valuation on
$\mathbb{R}$, is not minimal. But (and again, the shift is subtle), it _is_
minimal on the domain $\mathbf{I}\mathbb{R}_{\bot}$ that serves to do exact
real arithmetic. In fact, as we show in Section 6, _every_ measure on
$\mathbb{R}$ gives rise to a minimal valuation on
$\mathbf{I}\mathbb{R}_{\bot}$. We will even give a simple, explicit
description of the corresponding minimal valuation as a supremum of a
countable chain of simple valuations.

Having done all this preliminary work, we introduce a higher-order statistical
programming language, ISPCF, with continuous distributions and soft
constraints, as well as full recursion, in Section 7. Its denotational
semantics is somehow straightforward, considering our preparatory steps, and
is given in Section 8. In order to get a grasp of what we can express in
ISPCF, and more importantly, how one can reason about ISPCF programs using
that semantics, we provide a rather extensive list of examples in Section 9.
This culminates with non-trivial examples of distributions on some higher-
order data types.

Finally, we will explore a few operational semantics for ISPCF, paving the way
for formally verified implementations. (We will not address implementations
per se in this paper.) The first operational semantics for ISPCF we give is
similar to some other earlier proposals [Vákár et al., 2019, Dal Lago and
Hoshino, 2019, Ehrhard et al., 2018], except that our real numbers are exact
reals, not true reals, and that our transition function is continuous, not
just measurable; it is given in Section 10. It is not too hard to give another
operational semantics which works with _true_ reals, and which is therefore
even closer to the operational semantics given in [Vákár et al., 2019, Dal
Lago and Hoshino, 2019, Ehrhard et al., 2018]; this is the _precise_
operational semantics of Section 11. Finally, we give a sampling-based
operational semantics in Section 12. The name “sampling-based” is by analogy
with early work by [Park et al., 2008], and with one of the semantics of [Dal
Lago and Hoshino, 2019]. That semantics is meant to be one step closer to an
implementation: instead of drawing real numbers at random with respect to
arbitrary measures on $\mathbb{R}$, the sampling-based semantics draws bits
independently at random, and derives certain continuous distributions from
those bits. In each case, we show that our operational semantics are sound and
adequate with respect to our denotational semantics.

We finish by reviewing related work in Section 13, and by concluding in
Section 14.

##  2 Preliminaries, Challenges

We refer to [Billingsley, 1986] for basics of measure theory, and to [Abramsky
and Jung, 1994, Gierz et al., 2003, Goubault-Larrecq, 2013] for basics of
domain theory and topology.

###  2.1 Measure theory

A _$\sigma$ -algebra_ on a set $X$ is a collection of subsets closed under
countable unions and complements. A _measurable space_ $X$ is a set with a
$\sigma$-algebra $\Sigma_{X}$. The elements of $\Sigma_{X}$ are usually called
the _measurable subsets_ of $X$.

A _measure_ $\mu$ on $X$ is a $\sigma$-additive map from $\Sigma_{X}$ to
$\overline{\mathbb{R}}_{+}$, where $\overline{\mathbb{R}}_{+}$ is the set of
extended non-negative real numbers $\mathbb{R}_{+}\cup\\{+\infty\\}$. We will
agree that $0.(+\infty)=0$. (This makes multiplication on
$\overline{\mathbb{R}}_{+}$ Scott-continuous, see below.) The property of
_$\sigma$ -additivity_ means that, for every countable family of pairwise
disjoint sets $E_{n}$, $\mu(\bigcup_{n}E_{n})=\sum_{n}\mu(E_{n})$. (Here $n$
ranges over any subset of $\mathbb{N}$, possibly empty.)

A _measurable map_ $f\colon X\to Y$ between measurable spaces is a map such
that $f^{-1}(E)\in\Sigma_{X}$ for every $E\in\Sigma_{Y}$. The _image measure_
$f[\mu]$ of a measure $\mu$ on $X$ is defined by
$f[\mu](E)\mathrel{\buildrel\text{def}\over{=}}\mu(f^{-1}(E))$.

The $\sigma$-algebra $\Sigma(A)$ _generated by_ a family $A$ of subsets of $X$
is the the smallest $\sigma$-algebra containing $A$. The _Borel
$\sigma$-algebra_ on a topological space is the $\sigma$-algebra generated by
its topology. The _standard topology_ on $\overline{\mathbb{R}}_{+}$ is
generated by the intervals $[0,b[$, $]a,b[$ and $]a,+\infty]$, with
$0<a<b<+\infty$. Its Borel $\sigma$-algebra is also generated by just the
intervals $]a,+\infty]$ (the Scott-open subsets, see below). Hence a
measurable map $h\colon X\to\overline{\mathbb{R}}_{+}$ is a map such that
$h^{-1}(]t,+\infty])\in\Sigma_{X}$ for every $t\in\mathbb{R}$. Its _Lebesgue
integral_ can be defined elegantly through _Choquet’s formula_ :
$\int_{X}hd\mu\mathrel{\buildrel\text{def}\over{=}}\int_{0}^{+\infty}\mu(h^{-1}(]t,+\infty]))dt$,
where the right-hand integral is an ordinary Riemann integral.

This formula makes the following _change-of-variables formula_ an easy
observation: for every measurable map $f\colon X\to Y$, for every measurable
map $h\colon Y\to\overline{\mathbb{R}}_{+}$, $\int_{Y}hdf[\mu]=\int_{X}(h\circ
f)d\mu$.

There is a unique measure $\lambda$ on $\mathbb{R}$ such that
$\lambda(]a,b[)=b-a$ for every open bounded interval $]a,b[$. This measure is
called _Lebesgue measure_.

A measure $\mu$ on $X$ is _bounded_ if and only if $\mu(X)<+\infty$. A measure
$\mu$ is _$\sigma$ -finite_ if there is a sequence $E_{0}\subseteq
E_{1}\subseteq\cdots\subseteq E_{n}\subseteq\cdots$ of measurable subsets of
$X$ whose union is $X$ and such that $\mu(E_{n})<+\infty$ for every
$n\in\mathbb{N}$. A _$\pi$ -system_ $\Pi$ on a set $X$ is a family of sets
closed under finite intersections. If $X$ is a measurable space such that
$\Sigma_{X}=\Sigma(\Pi)$, any two $\sigma$-finite measures that agree on $\Pi$
also agree on $\Sigma_{X}$. In particular, Lebesgue measure on $\mathbb{R}$ is
uniquely defined by the specification $\lambda(]a,b[)=b-a$.

###  2.2 Domain theory and topology

A _dcpo_ is a poset in which every directed family $D$ has a supremum $\sup
D$. A prime example is $\overline{\mathbb{R}}_{+}$, with the usual ordering.
Another example is $\mathbf{I}\mathbb{R}$, the poset of closed intervals
$[a,b]$ with $a,b\in\mathbb{R}$ and $a\leq b$, ordered by reverse inclusion
$\supseteq$. Every directed family ${([a_{i},b_{i}])}_{i\in I}$ in
$\mathbf{I}\mathbb{R}$ has a supremum $\bigcap_{i\in
I}[a_{i},b_{i}]=[\sup_{i\in I}a_{i},\inf_{i\in I}b_{i}]$.
$\mathbf{I}\mathbb{R}_{\bot}$ is the _lift_ of $\mathbf{I}\mathbb{R}$, namely
the dcpo obtained by adding a fresh element $\bot$ below all others. In
general, we define the lift $X_{\bot}$ of a dcpo $X$ similarly. In the case of
$\mathbf{I}\mathbb{R}_{\bot}$, we may equate $\bot$ with the whole set
$\mathbf{I}\mathbb{R}$ itself, so that $\mathbf{I}\mathbb{R}_{\bot}$ is still
ordered by reverse inclusion. $\mathbf{I}\mathbb{R}_{\bot}$ will be the domain
of interpretation of the type $\boldsymbol{\mathtt{real}}$ of exact real
numbers. Among them, we find the _total_ numbers $a\in\mathbb{R}$, which we
may equate with the maximal elements $[a,a]$ of $\mathbf{I}\mathbb{R}$.

$\mathbf{I}\mathbb{R}_{\bot}$ is an example of a _pointed_ dcpo, namely one
that has a least element, which we will always write as $\bot$, and which we
read as _bottom_.

The _standard topology_ on $\mathbb{R}$ is generated by the open intervals
$]a,b[$, with $a<b$. The map $i\colon a\mapsto[a,a]$ is then a topological
embedding of $\mathbb{R}$, with its standard topology, into
$\mathbf{I}\mathbb{R}$ (or $\mathbf{I}\mathbb{R}_{\bot}$) with its Scott
topology. In other words, $i$ is continuous, and every open subset $U$ of
$\mathbb{R}$ is the inverse image of some Scott-open subset of
$\mathbf{I}\mathbb{R}$ (resp., $\mathbf{I}\mathbb{R}_{\bot}$) by $i$.
Explicitly, $]a,b[$ is the inverse image of the Scott-open subset of intervals
$[c,d]$ such that $a<c\leq d<b$. This allows us to consider $\mathbb{R}$ as a
subspace of $\mathbf{I}\mathbb{R}$, resp. $\mathbf{I}\mathbb{R}_{\bot}$.

We will also write $\leq$ for the ordering on any poset. In the example of
$\mathbf{I}\mathbb{R}$ or $\mathbf{I}\mathbb{R}_{\bot}$, $\leq$ is
$\supseteq$. The _upward closure_ $\mathop{\uparrow}A$ of a subset $A$ of a
poset $X$ is $\\{y\in X\mid\exists x\in A,x\leq y\\}$. The _downward closure_
$\mathop{\downarrow}A$ is defined similarly. A set $A$ is _upwards closed_ if
and only if $A=\mathop{\uparrow}A$, and _downwards closed_ if and only if
$A=\mathop{\downarrow}A$. A subset $U$ of a poset $X$ is _Scott-open_ if and
only if it is upwards closed and, for every directed family $D$ such that
$\sup D$ exists and is in $U$, some element of $D$ is in $U$ already. The
Scott-open subsets of a poset $X$ form its _Scott topology_.

The _way-below_ relation $\ll$ on a poset $X$ is defined by $x\ll y$ if and
only if, for every directed family $D$ with a supremum $z$, if $y\leq z$, then
$x$ is less than or equal to some element of $D$ already. We write $\hbox
to0.0pt{$\uparrow$\hss}\raise 2.15277pt\hbox{$\uparrow$}x$ for $\\{y\in X\mid
x\ll y\\}$, and $\hbox to0.0pt{$\downarrow$\hss}\raise
2.15277pt\hbox{$\downarrow$}y$ for $\\{x\in X\mid x\ll y\\}$. A poset $X$ is
_continuous_ if and only if $\hbox to0.0pt{$\downarrow$\hss}\raise
2.15277pt\hbox{$\downarrow$}x$ is directed and has $x$ as supremum for every
$x\in X$. A _basis_ $B$ of a poset $X$ is a subset of $X$ such that $\hbox
to0.0pt{$\downarrow$\hss}\raise 2.15277pt\hbox{$\downarrow$}x\cap B$ is
directed and has $x$ as supremum for every $x\in X$. A poset $X$ is continuous
if and only if it has a basis (namely, $X$ itself). A poset is _$\omega$
-continuous_ if and only if it has a countable basis. Examples include
$\overline{\mathbb{R}}_{+}$, with any countable dense subset (with respect to
its standard topology), such as the rational numbers, or such as the _dyadic
numbers_ $k/2^{n}$ ($k,n\in\mathbb{N}$); or $\mathbf{I}\mathbb{R}$ and
$\mathbf{I}\mathbb{R}_{\bot}$, with the basis of intervals $[a,b]$ where $a$
and $b$ are both dyadic or both rational.

We write ${\mathcal{O}}X$ for the lattice of open subsets of a topological
space. This applies to dcpos $X$ as well, which will always be considered with
their Scott topology. The continuous maps $f\colon X\to Y$ between two dcpos
coincide with the _Scott-continuous_ maps, namely the monotonic (order-
preserving) maps that preserve all directed suprema. We write $\mathcal{L}X$
for the space of continuous maps from a topological space $X$ to
$\overline{\mathbb{R}}_{+}$, the latter with its Scott topology, as usual.
Such maps are usually called _lower semicontinuous_ , or _lsc_ , in the
mathematical literature. Note that $\mathcal{L}X$, with the pointwise
ordering, is a dcpo.

There are several ways in which one can model probabilistic choice. The most
classical one is through measures. A popular alternative used in domain theory
is given by _continuous valuations_ [Jones and Plotkin, 1989, Jones, 1990]. A
continuous valuation is a Scott-continuous map
$\nu\colon{\mathcal{O}}X\to\overline{\mathbb{R}}_{+}$ such that
$\nu(\emptyset)=0$ (_strictness_) and, for all $U,V\in{\mathcal{O}}X$,
$\nu(U\cup V)+\nu(U\cap V)=\nu(U)+\nu(V)$ (_modularity_). Canonical examples
of continuous valuations on $X$ are _Dirac valuations_ $\delta_{x}$ for $x\in
X$, where for each open subset $U$ of $X$, $\delta_{x}(U)=1$ if $x\in U$ and
$\delta_{x}(U)=0$, otherwise. The set of all continuous valuations on $X$ is
denoted by $\mathbf{V}X$. We order $\mathbf{V}X$ by the _stochastic order_
defined as $\nu_{1}\leq\nu_{2}$ if and only if $\nu_{1}(U)\leq\nu_{2}(U)$ for
all opens of $X$. The set $\mathbf{V}X$ is a dcpo in the stochastic order.

There is a notion of integral $\int_{x\in X}h(x)d\nu$, or briefly $\int
hd\nu$, for every $h\in\mathcal{L}X$, which can again be defined by a Choquet
formula. Tix [Tix, 1995, Satz 4.4] showed that the integral is a Scott-
continuous bilinear form, namely:

  * •

for every $\nu\in\mathbf{V}X$, the map $h\in\mathcal{L}X\mapsto\int hd\nu$ is
Scott-continuous and linear, in the sense that $\int\alpha hd\nu=\alpha\int
hd\nu$ for every $\alpha\in\mathbb{R}$ and $\int(h+h^{\prime})d\nu=\int
hd\nu+\int h^{\prime}d\nu$, for all $h,h^{\prime}\in\mathcal{L}X$;

  * •

for every $h\in\mathcal{L}X$, the map $\nu\in\mathbf{V}X\mapsto\int hd\nu$ is
Scott-continuous and linear, in a similar sense.

More generally, a _linear_ map
$G\colon\mathcal{L}X\to\overline{\mathbb{R}}_{+}$ satisfies
$G(h+h^{\prime})=G(h)+G(h^{\prime})$ and $G(\alpha.h)=\alpha.G(h)$ for all
$\alpha\in\mathbb{R}_{+}$, $h,h^{\prime}\in\mathcal{L}X$. Conversely, any
Scott-continuous linear map $G\colon\mathcal{L}X\to\overline{\mathbb{R}}_{+}$
is of the form $h\mapsto\int hd\nu$ for a unique continuous valuation $\nu$,
given by $\nu(U)\mathrel{\buildrel\text{def}\over{=}}G(\chi_{U})$, where
$\chi_{U}$ is the characteristic map of $U$
($\chi_{U}(x)\mathrel{\buildrel\text{def}\over{=}}1$ if $x\in U$, $0$
otherwise).

Continuous valuations and measures are pretty much the same thing on
$\omega$-continuous dcpos, namely on continuous dcpos with a countable basis.
This holds more generally on de Brecht’s quasi-Polish spaces [de Brecht,
2013], a class of spaces that contains not only the $\omega$-continuous dcpos
from domain theory but also the Polish spaces from topological measure theory.

One can see this as follows. In one direction, Adamski’s theorem states that
every measure $\mu$ on a hereditarily Lindelöf space $X$ is $\tau$-smooth
[Adamski, 1977, Theorem 3.1], meaning that its restriction to the lattice of
open subsets of $X$ is a continuous valuation. A hereditarily Lindelöf space
is a space whose subspaces are all Lindelöf, or equivalently a space in which
every family of open sets contains a countable subfamily with the same union.
Every second-countable space is hereditarily Lindelöf, and that includes all
quasi-Polish spaces. In the other direction, every continuous valuation on an
LCS-complete space extends to a Borel measure [de Brecht et al., 2019, Theorem
1.1]. An _LCS-complete_ space is a space that is homeomorphic to a
$G_{\delta}$ subset of a locally compact sober space. Every quasi-Polish space
is LCS-complete; in fact, the quasi-Polish spaces are exactly the second-
countable LCS-complete spaces [de Brecht et al., 2019, Theorem 9.5].

###  2.3 Is there any trouble with the probabilistic powerdomain?

The probabilistic powerdomain, namely the dcpo $\mathbf{V}X$ of all continuous
valuations on a space $X$, ordered pointwise, is known to have its problems
[Jung and Tix, 1998]. Precisely, there is no known Cartesian-closed category
of continuous dcpos that is closed under the $\mathbf{V}$ functor. It is
sometimes believed that this means that domain theory cannot be used to give
semantics to higher-order probabilistic languages. This would be wrong: the
category ${\mathbf{Dcpo}}$ of _all_ dcpos, not just the continuous dcpos, _is_
Cartesian-closed and closed under the $\mathbf{V}$ functor [Jones and Plotkin,
1989, Jones, 1990].

Continuity is not required to prove, say, soundness and adequacy theorems
using logical relations, as one realizes by reading the relevant parts of
[Streicher, 2002], and as we will do in Section 10.2. But it is required to
obtain a form of the Fubini-Tonelli theorem, or, in categorical terms, to turn
$\mathbf{V}$ into a _commutative_ monad. (See [Kock, 2012, Theorem 9.2] for
the relation between the two notions.) Commutativity is important in
applications, as we will briefly discuss in Remark 8.1, and is a key
ingredient of the semantics of [Vákár et al., 2019]. We _do_ obtain a
commutative monad, without any need for continuity, by a simple trick based on
inductive closures (Definition 5.1, Section 5). This trick was found
independently by at least one other group of researchers [Jia et al., 2021],
but on different, and incomparable, monads.

###  2.4 Scoring, and density functions

Compared to ordinary probabilistic languages, statistical programming
languages aim to offer the possibility of computing conditional distributions.
This runs into questions on non-computability [Ackerman et al., 2011]. At this
point, we note that there are well-established theories of computable
probability distributions, notably on computable metric spaces [Galatolo et
al., 2010], on more general computable topological spaces [Roy, 2011], and
also based on Weihrauch’s type two theory of effectivity, also known as _TTE_
[Weihrauch, 1987], see [Weihrauch, 1999, Schröder and Simpson, 2006]. In the
absence of probabilities, Schulz [Schulz, 2000] shows that the functions from
$[0,1]^{n}$ to $[0,1]$ that are computable in the sense of TTE and of RealPCF
coincide.

In practice, a number of algorithms are implemented to compute certain special
conditional distributions, with a fallback strategy based on one form or
another of rejection sampling, or with a so-called _scoring_ mechanism, which
allows one to give more or less importance to specific outcomes.

This scoring mechanism is typically implemented through a primitive called
$\boldsymbol{\mathtt{score}}$ [Staton et al., 2016, Vákár et al., 2019, Dal
Lago and Hoshino, 2019, Ehrhard et al., 2018]. Roughly, the effect of
$\boldsymbol{\mathtt{score}}\;M$, where $M\colon\boldsymbol{\mathtt{real}}$
evaluates to a non-negative real number $\alpha$, is to multiply the
‘probability’ of the current computation branch by $\alpha$—making it a
measure rather than a probability, whence the quotes.

As a consequence, $\boldsymbol{\mathtt{score}}$ can be used to build new
measures $g\cdot\mu$ from a measure $\mu$ and a density function $g$. The
measure $g\cdot\mu$ is defined by
$(g\cdot\mu)(E)\mathrel{\buildrel\text{def}\over{=}}\int_{x}\chi_{E}(x)g(x)d\mu$,
and is sometimes written as $gd\mu$. Indeed, in case $x$ is drawn at random
with respect to some measure $\mu$, writing
$\boldsymbol{\mathtt{score}}\;g(x);M(x)$ will have the effect of executing
$M(x)$ as though $x$ had been drawn with probability multiplied by $g(x)$,
namely as though it had been drawn at random with respect to $g\cdot\mu$. This
interpretation conforms to intuition if $g$ really is a density function,
namely if $\int_{x}g(x)d\mu=1$, in which case $g\cdot\mu$ is a probability
distribution. In general, however, $g\cdot\mu$ will be a measure. As a simple,
but extreme example, $\boldsymbol{\mathtt{score}}\;0$ annihilates the effect
of the current computation. If $x$ is drawn with a measure whose total mass
is, say, $\pi/4$, then $\boldsymbol{\mathtt{score}}(4/\pi)$ will renormalize
the measure to a probability distribution. Other uses of
$\boldsymbol{\mathtt{score}}$ include soft conditioning and Bayesian fitting,
as illustrated in [Vákár et al., 2019].

##  3 Monads of continuous valuations

We will describe probabilistic effects by following Moggi’s seminal work on
monads [Moggi, 1989, Moggi, 1991]. We use Manes’ presentation of monads
[Manes, 1976]: a monad $(T,\eta,\\_^{\dagger})$ on a category ${\mathbf{C}}$
is a function $T$ mapping objects of ${\mathbf{C}}$ to objects of
${\mathbf{C}}$, a collection of morphisms $\eta_{X}\colon X\to TX$, one for
each object $X$ of ${\mathbf{C}}$, and called the _unit_ , and for every
morphism $f\colon X\to TY$, a morphism $f^{\dagger}\colon TX\to TY$ called the
_extension_ of $f$; those are required to satisfy the axioms:

  1. 1.

$f^{\dagger}\circ\eta_{X}=f$;

  2. 2.

$\eta_{X}^{\dagger}=\mathrm{id}_{TX}$;

  3. 3.

$(g^{\dagger}\circ f)^{\dagger}=g^{\dagger}\circ f^{\dagger}$.

Then $T$ extends to an endofunctor, acting on morphisms through
$Tf=(\eta_{Y}\circ f)^{\dagger}$. Proposition 3.2 below is due to Jones
[Jones, 1990, Theorem 4.5]. Her definition of the integral was different, and
she implicitly restricted valuations to subprobability valuations. A similar
statement is due to Kirch [Kirch, 1993, Satz 6.1], for continuous dcpos
instead of general dcpos. Tix [Tix, 1995] was probably the first to use the
Choquet formula in this context. Her study was also restricted to continuous
dcpos.

We define $\eta_{X}\colon X\to\mathbf{V}X$ as mapping $x\in X$ to
$\delta_{x}$. For every Scott-continuous map $f\colon X\to\mathbf{V}Y$, for
every $\mu\in\mathbf{V}X$, for every Scott-open subset $V$ of $Y$, we define:

$\displaystyle f^{\dagger}(\mu)(V)$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}\int_{x\in X}f(x)(V)d\mu.$
(1)

The following lemma is proved exactly as in most of the references we have
just cited.

######  Lemma 3.1.

For all dcpos $X$ and $Y$, for every Scott-continuous map $f\colon
X\to\mathbf{V}Y$,

  1. (i)

the map $\eta_{X}$ is Scott-continuous;

  2. (ii)

the map $f^{\dagger}$ is Scott-continuous from $\mathbf{V}X$ to $\mathbf{V}Y$;

  3. (iii)

for every $\mu\in\mathbf{V}X$, for every $g\in\mathcal{L}Y$,

$\displaystyle\int_{y\in Y}g(y)df^{\dagger}(\mu)$ $\displaystyle=\int_{x\in
X}\left(\int_{y\in Y}g(y)df(x)\right)d\mu.$ (2)

  4. (iv)

For every $h\in\mathcal{L}X$, $\int_{x^{\prime}\in
X}h(x^{\prime})d\delta_{x}=h(x)$.

###### Proof.

(i) If $x\leq y$, then for every $U\in{\mathcal{O}}X$, if $\delta_{x}(U)=1$
then $x$ is in $U$, so $y$ is in $U$ as well, and therefore $\delta_{y}(U)=1$.
It follows that $\delta_{x}\leq\delta_{y}$. Let $D$ be any directed family in
$X$, and $x\mathrel{\buildrel\text{def}\over{=}}\sup D$. For every
$U\in{\mathcal{O}}X$, $\delta_{x}(U)=1$ if and only if $x\in U$, if and only
if some element $y\in D$ is in $U$, by definition of Scott-open sets; and that
is equivalent to $\sup_{y\in D}\delta_{y}(U)=1$.

(ii) We first verify that $f^{\dagger}(\mu)$ is a continuous valuation, for
every $\mu\in\mathbf{V}X$. Strictness and modularity follow easily from the
fact that $f(x)\in\mathbf{V}Y$ for every $x\in X$. Scott-continuity follows
from the fact that the integral is a (bilinear) form that is Scott-continuous
in its function argument. The integral is also Scott-continuous in its
valuation argument, so $f^{\dagger}$ is itself Scott-continuous.

(iii) We write $g$ as the directed supremum of the maps $g_{K}$, defined by
$g_{K}(y)\mathrel{\buildrel\text{def}\over{=}}\sum_{k=1}^{K2^{K}}\frac{1}{2^{K}}\chi_{g^{-1}(]\frac{k}{2^{K}},+\infty])}$,
$K\in\mathbb{N}$. Then:

$\displaystyle\int_{y\in Y}g_{K}(y)df^{\dagger}(\mu)$
$\displaystyle=\sum_{k=1}^{K2^{K}}\frac{1}{2^{K}}\int_{y\in
Y}\chi_{g^{-1}(]\frac{k}{2^{K}},+\infty])}(y)df^{\dagger}(\mu)$
$\displaystyle=\sum_{k=1}^{K2^{K}}\frac{1}{2^{K}}f^{\dagger}(\mu)(g^{-1}(]\frac{k}{2^{K}},+\infty])$
$\displaystyle=\sum_{k=1}^{K2^{K}}\frac{1}{2^{K}}\int_{x\in
X}f(x)(g^{-1}(]\frac{k}{2^{K}},+\infty])d\mu$ $\displaystyle=\int_{x\in
X}\sum_{k=1}^{K2^{K}}\frac{1}{2^{K}}f(x)(g^{-1}(]\frac{k}{2^{K}},+\infty])d\mu$
$\displaystyle=\int_{x\in X}\left(\int_{y\in Y}g_{K}(y)df(x)\right)d\mu,$

and the result follows by Scott-continuity of the integral in its function
argument and taking suprema, as $K$ tends to $+\infty$.

(iv) The Choquet formula for the integral yields
$\int_{x^{\prime}\in
X}h(x^{\prime})d\delta_{x}=\int_{0}^{+\infty}\delta_{x}(h^{-1}(]t,+\infty]))dt=\int_{0}^{h(x)}1dt=h(x)$.
∎

######  Proposition 3.2.

The triple $(\mathbf{V},\eta,\\_^{\dagger})$ is a monad on the category
${\mathbf{Dcpo}}$ of dcpos and Scott-continuous maps. For every Scott-
continuous map $f\colon X\to Y$, for every $\mu\in\mathbf{V}X$,
$\mathbf{V}f(\mu)$ is the image valuation $f[\mu]$, defined by
$f[\mu](V)\mathrel{\buildrel\text{def}\over{=}}\mu(f^{-1}(V))$, for every
$V\in{\mathcal{O}}Y$.

###### Proof.

In light of Lemma 3.1, the first part will be proved once we have verified the
three axioms given by Manes:

  1. 1.

$f^{\dagger}\circ\eta_{X}$ maps $x$ to the continuous valuation $\nu$ defined
by $\nu(V)\mathrel{\buildrel\text{def}\over{=}}\int_{x\in
X}f(x)(V)d\delta_{x}=f(x)(V)$; so $\nu=f(x)$, and therefore
$f^{\dagger}\circ\eta_{X}=f$.

  2. 2.

$\eta_{X}^{\dagger}$ satisfies $\eta_{X}^{\dagger}(\mu)(U)=\int_{x\in
X}\eta_{X}(x)(U)d\mu=\int_{x\in X}\chi_{U}(x)d\mu=\mu(U)$, so
$\eta_{X}^{\dagger}=\mathrm{id}_{\mathbf{V}X}$.

  3. 3.

For all $f\colon X\to\mathbf{V}Y$, $g\colon Y\to\mathbf{V}Z$, and
$W\in{\mathcal{O}}Z$,

$\displaystyle(g^{\dagger}\circ f)^{\dagger}(\mu)(W)$
$\displaystyle=\int_{x\in X}g^{\dagger}(f(x))(W)d\mu$
$\displaystyle=\int_{x\in X}\left(\int_{y\in Y}g(y)(W)df(x)\right)d\mu,$

while:

$\displaystyle g^{\dagger}(f^{\dagger}(\mu))(W)$ $\displaystyle=\int_{y\in
Y}g(y)(W)df^{\dagger}(\mu)$ $\displaystyle=\int_{x\in X}\left(\int_{y\in
Y}g(y)(W)df(x)\right)d\mu,$

by (2).

∎

##  4 The Fubini-Tonelli theorem, and what goes wrong with ${\mathbf{Dcpo}}$

Jones proved a form of Fubini’s (more accurately, Tonelli’s) theorem for
(subprobability) continuous valuations, on continuous dcpos [Jones, 1990].
This actually generalizes to continuous valuations on arbitrary topological
spaces, and the proof is not that complicated, as we demonstrate. (Another
purpose we have in giving that proof is in order to fix a gap in Jones’ proof,
who actually does not show the existence of the product valuation.)

As we will see in more detail later, Tonelli’s theorem turns $\mathbf{V}$ into
a commutative monad, and that is a basic requirement for being able to say
that drawing two objects at random independently can be done in any order.

######  Proposition 4.1 (Fubini-Tonelli for continuous valuations on
${\mathbf{Top}}$).

Let $X$ and $Y$ be two spaces, $\mu\in\mathbf{V}X$, $\nu\in\mathbf{V}Y$. There
is a unique so-called product valuation $\mu\times\nu$ on $X\times Y$ such
that, for every $U\in{\mathcal{O}}X$ and for every $V\in{\mathcal{O}}Y$,
$(\mu\times\nu)(U\times V)=\mu(U).\nu(V)$. For every $f\in\mathcal{L}(X\times
Y)$,

$\displaystyle\int_{(x,y)\in X\times Y}f(x,y)d(\mu\times\nu)$
$\displaystyle=\int_{x\in X}\left(\int_{y\in Y}f(x,y)d\nu\right)d\mu$
$\displaystyle=\int_{y\in Y}\left(\int_{x\in X}f(x,y)d\mu\right)d\nu.$

###### Proof.

(Sketch.) We first deal with uniqueness. We assume any continuous valuation
$\xi$ on $X\times Y$ such that $\xi(U\times V)=\mu(U).\nu(V)$ for all
$U\in{\mathcal{O}}X$ and $V\in{\mathcal{O}}Y$. We call any such product
$U\times V$ an _open rectangle_. The value of $\xi$ on finite unions
$W\mathrel{\buildrel\text{def}\over{=}}\bigcup_{i\in J}U_{i}\times V_{i}$ of
open rectangles is determined uniquely: either $\mu(U_{i}).\nu(U_{i})=+\infty$
for some $i\in J$, and then $\xi(W)$ must be equal to $+\infty$, by
monotonicity; or $\xi(W)$ must be equal to $\sum_{K\neq\emptyset,K\subseteq
J}(-1)^{|K|+1}\xi(\bigcap_{i\in K}U_{i}\times V_{i})$ by the so-called
inclusion-exclusion formula (an easy consequence of modularity), showing that
$\xi(W)$ is again determined uniquely. Finally, by definition of the product
topology, every open subset $W$ of $X\times Y$ is a union $\bigcup_{i\in
I}U_{i}\times V_{i}$ of open rectangles, hence a directed union of finite
unions $\bigcup_{i\in J}U_{i}\times V_{i}$ (where $J$ ranges over the finite
subsets of $I$); $\xi(W)$ is then determined uniquely, since $\xi$ is Scott-
continuous.

For the existence part, the easiest route is to consider the two maps
$G,G^{\prime}\colon\mathcal{L}(X\times Y)\to\overline{\mathbb{R}}_{+}$ defined
by:

$\displaystyle G(f)$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}\int_{x\in
X}\left(\int_{y\in Y}f(x,y)d\nu\right)d\mu$ $\displaystyle G^{\prime}(f)$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}\int_{y\in
Y}\left(\int_{x\in X}f(x,y)d\mu\right)d\nu.$

We check that $G$ and $G^{\prime}$ are Scott-continuous, linear maps, and are
therefore integral functionals for unique continuous valuations $\xi$ and
$\xi^{\prime}$ on $X\times Y$, respectively. For every open rectangle $U\times
V$, $\xi(U\times V)=G(\chi_{U\times V})$ is equal to $\mu(U).\nu(V)$, and
similarly for $\xi^{\prime}(U\times V)$. By the uniqueness part,
$\xi=\xi^{\prime}$, so $G=G^{\prime}$. We write $\mu\times\nu$ for $\xi$, and
the theorem is proved. ∎

This proof is the core of several similar proofs. One of the closest is due to
Vickers [Vickers, 2011], who proves a similar theorem on the category of
locales instead of ${\mathbf{Top}}$. Although localic theorems usually
generalize purely topological theorems, this one does not, because locale
products do not coincide with products in ${\mathbf{Top}}$ in general [Isbell,
1981, Theorem 2].

Since every dcpo can be seen as a topological space with its Scott topology,
it would seem that we would obtain a Fubini-Tonelli theorem for Scott-
continuous maps and continuous valuations on arbitrary dcpos, as a special
case of Proposition 4.1.

This is not the case, but the reason is subtle. As with locales, products in
${\mathbf{Dcpo}}$ do not usually coincide with products in ${\mathbf{Top}}$.
Explicitly, let us write $X_{\sigma}$ for the topological space obtained by
equipping a dcpo $X$ with its Scott topology. Then the topology on $(X\times
Y)_{\sigma}$ (where $\times$ is dcpo product) is finer, and in general
strictly finer, than the product topology on $X_{\sigma}\times Y_{\sigma}$.
(See Exercise 5.2.16 of [Goubault-Larrecq, 2013] for an example where it is
strictly finer.) As a consequence, there are more, and generally, strictly
more Scott-continuous maps from $X\times Y$ to $\overline{\mathbb{R}}_{+}$
than continuous maps from the topological product $X_{\sigma}\times
Y_{\sigma}$ to $\overline{\mathbb{R}}_{+}$. The Fubini-Tonelli formula holds
for functions of the second, smaller class, but it is unknown whether it holds
for the first kind of functions. One exception is when either $X$ or $Y$ is
_core-compact_ (the Scott-opens form a continuous lattice), in which case the
Scott and product topologies coincide on $X\times Y$ [Gierz et al., 2003,
Theorem II-4.13]; then we retrieve Jones’ version of the Fubini-Tonelli
theorem.

One may blame ${\mathbf{Dcpo}}$ for this state of affairs. Another possibility
is to consider that we are considering too general a notion of continuous
valuation. We will explore this avenue in the next section, by restricting to
so-called minimal valuations.

##  5 Minimal valuations, and Fubini-Tonelli again

A _simple valuation_ is any finite linear combination
$\sum_{i=1}^{n}r_{i}\delta_{x_{i}}$ of Dirac masses, with coefficients $r_{i}$
in $\mathbb{R}_{+}$.

######  Definition 5.1 (Minimal valuations).

Let $\mathbf{V}_{\mathrm{f}}X$ be the poset of simple valuations on $X$, and
$\mathbf{V}_{m}X$ be the inductive closure of $\mathbf{V}_{\mathrm{f}}X$ in
$\mathbf{V}X$. The elements of $\mathbf{V}_{m}X$ are called the _minimal
valuations_ on $X$.

The _inductive closure_ of a subset $A$ of a dcpo $Z$ is the smallest subset
of $Z$ that contains $A$ and is closed under directed suprema. It is obtained
by taking all directed suprema of elements of $A$, all directed suprema of
elements obtained in this fashion, and proceeding this way transfinitely.

######  Remark 5.2.

On a continuous dcpo $X$, every continuous valuation is a directed supremum of
simple valuations. In fact, $\mathbf{V}X$ is a continuous dcpo with a basis of
simple valuations, as showed by Jones [Jones, 1990], at least in the case of
subprobability valuations. (The general theorem can be found as Theorem
IV-9.16 of [Gierz et al., 2003].) Hence, in particular, continuous valuations
and minimal valuations agree on every continuous dcpo. One may wonder whether
all continuous valuations on a dcpo are minimal. We will give a counterexample
to this claim in a forthcoming paper.

###  5.1 The monad $\mathbf{V}_{m}$ of minimal valuations

We will now show that $\mathbf{V}_{m}$ defines a submonad of $\mathbf{V}$. To
this end, we need to know more about inductive closures. A _d-closed subset_
of a dcpo $Z$ is a subset $C$ such that the supremum of every directed family
of elements of $C$, taken in $Z$, is in $C$. The d-closed subsets form the
closed subsets of a topology called the _d-topology_ [Keimel and Lawson, 2008,
Section 5], and the inductive closure of a subset $A$ coincides with its _d-
closure_ $cl_{d}(A)$, namely its closure in the d-topology.

We note that every Scott-continuous map is continuous with respect to the
underlying d-topologies. This is easily checked, or see [Keimel and Lawson,
2008, Lemma 5.3]. In particular:

######  Fact 5.3.

For every Scott-continuous map $f\colon\mathbf{V}X\to\mathbf{V}Y$, for every
$A\subseteq\mathbf{V}X$, $f(cl_{d}(A))\subseteq cl_{d}(f(A))$.

######  Lemma 5.4.

For every space $X$, $\mathbf{V}_{m}X$ is closed under addition and
multiplication by elements of $\overline{\mathbb{R}}_{+}$, as computed in the
larger space $\mathbf{V}X$.

###### Proof.

Let us deal with addition. Multiplication is similar.

For every simple valuation $\mu$, the map
$f_{\mu}\colon\nu\in\mathbf{V}X\mapsto\mu+\nu$ is Scott-continuous, and maps
simple valuations to simple valuations. By Fact 5.3 with
$A\mathrel{\buildrel\text{def}\over{=}}\mathbf{V}_{\mathrm{f}}X$, $f_{\mu}$
maps all elements of $cl_{d}(A)=\mathbf{V}_{m}X$ to
$cl_{d}(f_{\mu}(A))\subseteq
cl_{d}(\mathbf{V}_{\mathrm{f}}X)=\mathbf{V}_{m}X$.

It follows that for every minimal valuation $\nu$, the map
$g\colon\mu\in\mathbf{V}X\mapsto\mu+\nu=f_{\mu}(\nu)$ maps simple valuations
to minimal valuations. We observe that $g$ is also Scott-continuous. By Fact
5.3 with the same $A$ as above, $g$ maps all elements of
$cl_{d}(A)=\mathbf{V}_{m}X$ to $cl_{d}(g(A))\subseteq
cl_{d}(\mathbf{V}_{m}X)=\mathbf{V}_{m}X$. Hence, for every
$\nu\in\mathbf{V}_{m}X$, for every $\mu\in\mathbf{V}_{m}X$, $\mu+\nu$ is in
$\mathbf{V}_{m}X$. ∎

######  Lemma 5.5.

For any Scott-continuous map $f\colon X\to\mathbf{V}_{m}Y$, $f^{\dagger}$ is a
Scott-continuous map from $\mathbf{V}_{m}X$ to $\mathbf{V}_{m}Y$. Similarly,
for every Scott-continuous map $f\colon X\to Y$, $\mathbf{V}f$ is a Scott-
continuous map from $\mathbf{V}_{m}X$ to $\mathbf{V}_{m}Y$.

###### Proof.

For the first part, the only challenge is to show that, for every
$\nu\in\mathbf{V}_{m}X$, $f^{\dagger}(\nu)$ is in $\mathbf{V}_{m}Y$. Scott-
continuity follows from the fact that $f^{\dagger}$ is Scott-continuous from
$\mathbf{V}X$ to $\mathbf{V}Y$.

For every
$\nu\mathrel{\buildrel\text{def}\over{=}}\sum_{i=1}^{n}r_{i}\delta_{x_{i}}$ in
$\mathbf{V}_{\mathrm{f}}X$, $f^{\dagger}(\nu)$ is the continuous valuation
$\sum_{i=1}^{n}r_{i}f(x_{i})$: for every $V\in{\mathcal{O}}Y$,
$f^{\dagger}(\nu)(V)=\int_{x\in X}f(x)(V)d\nu=\sum_{i=1}^{n}r_{i}f(x_{i})(V)$.
By Lemma 5.4, and since $f(x_{i})$ is in $\mathbf{V}_{m}Y$ for each $i$,
$f^{\dagger}(\nu)$ is in $\mathbf{V}_{m}Y$ as well.

Hence $f^{\dagger}$ maps $\mathbf{V}_{\mathrm{f}}X$ to $\mathbf{V}_{m}Y$.
Using Fact 5.3 with
$A\mathrel{\buildrel\text{def}\over{=}}\mathbf{V}_{\mathrm{f}}X$,
$f^{\dagger}(cl_{d}(A))=f^{\dagger}(\mathbf{V}_{m}X)$ is included in
$cl_{d}(f^{\dagger}(A))\subseteq cl_{d}(\mathbf{V}_{m}Y)=\mathbf{V}_{m}Y$.

The second part follows from the first part and the equation
$\mathbf{V}f=(\eta_{Y}\circ f)^{\dagger}$. ∎

We observe that $\eta_{X}(x)=\delta_{x}$ is in
$\mathbf{V}_{\mathrm{f}}X\subseteq\mathbf{V}_{m}X$ for every dcpo $X$, and
every $x\in X$, whence the following.

######  Proposition 5.6.

The triple $(\mathbf{V}_{m},\eta,\\_^{\dagger})$ is a monad on the category of
dcpos and Scott-continuous maps.

###  5.2 Tensorial strengths

A tensorial strength for a monad $(T,\eta,\\_^{\dagger})$ is a collection $t$
of morphisms $t_{X,Y}\colon X\times TY\to T(X\times Y)$, natural in $X$ and
$Y$, satisfying certain coherence conditions (which we omit, see [Moggi,
1991].) We then say that $(T,\eta,\\_^{\dagger},t)$ is a _strong_ monad. We
will satisfy ourselves with the following result. By [Moggi, 1991, Proposition
3.4], in a category with finite products and enough points, if one can find
morphisms $t_{X,Y}\colon X\times TY\to T(X\times Y)$ for all objects $X$ and
$Y$ such that $t_{X,Y}\circ\langle x,\nu\rangle=T(\langle
x\circ!,\mathrm{id}_{Y}\rangle)\circ\nu$, then the collection of those
morphisms is the unique tensorial strength. A category with a terminal object
$1$ has _enough points_ if and only if, for any two morphisms $f,g\colon X\to
Y$, $f=g$ if and only if for every $x\colon 1\to X$, $f\circ x=g\circ x$.

The category ${\mathbf{Dcpo}}$ of dcpos has finite products, and has enough
points. Specializing the above to
$T\mathrel{\buildrel\text{def}\over{=}}\mathbf{V}$, the formula for $t_{X,Y}$
reads: for every $x\in X$, for every $\nu\in\mathbf{V}Y$, for every
$W\in{\mathcal{O}}(X\times Y)$, $t_{X,Y}(x,\nu)(W)=\nu(\\{y\in Y\mid(x,y)\in
W\\}$. Rewriting this as $t_{X,Y}(x,\nu)(W)=\int_{y\in Y}\chi_{W}(x,y)d\nu$,
hence $t_{X,Y}(x,\nu)=\mathbf{V}(\lambda y\in Y.(x,y))(\nu)$, we retrieve
formulae already given by Jones [Jones, 1990, Section 4.3], and which show
immediately that the map $t_{X,Y}$ is well-defined and Scott-continuous.

It also follows from Lemma 5.5 that, if $\nu$ is a minimal valuation, namely
an element of $\mathbf{V}_{m}X$, then $t_{X,Y}(x,\nu)$ is an element of
$\mathbf{V}_{m}(X\times Y)$. It follows:

######  Proposition 5.7.

$(\mathbf{V},\eta,\\_^{\dagger},t)$ and
$(\mathbf{V}_{m},\eta,\\_^{\dagger},t)$ are strong monads on
${\mathbf{Dcpo}}$.

###  5.3 Minimal valuations form a commutative monad on ${\mathbf{Dcpo}}$, or
Fubini-Tonelli again

We now show that $\mathbf{V}_{m}$ is a _commutative_ monad on
${\mathbf{Dcpo}}$. The corresponding result is unknown for $\mathbf{V}$.
Equivalently, the Fubini-Tonelli theorem holds for minimal valuations. In
order to prove it, we use the following simple lemma.

######  Lemma 5.8.

Two morphisms $f,g\colon X\to Y$ in ${\mathbf{Dcpo}}$ that coincide on
$A\subseteq X$ also coincide on $cl_{d}(A)$.

###### Proof.

Let $B\mathrel{\buildrel\text{def}\over{=}}\\{x\in X\mid f(x)=g(x)\\}$. Since
$f$ and $g$ preserve directed suprema, $B$ is d-closed. By assumption, $A$ is
included in $B$, so $B$ also contains $cl_{d}(A)$. ∎

######  Theorem 5.9 (Fubini-Tonelli for minimal valuations on
${\mathbf{Dcpo}}$).

Let $X$, $Y$ be two dcpos, $f\in\mathcal{L}(X\times Y)$, $\mu\in\mathbf{V}X$,
and $\nu\in\mathbf{V}Y$. If $\mu$ or $\nu$ is minimal, then:

$\displaystyle\int_{x\in X}\left(\int_{y\in Y}f(x,y)d\nu\right)d\mu$
$\displaystyle=\int_{y\in Y}\left(\int_{x\in X}f(x,y)d\mu\right)d\nu.$ (3)

###### Proof.

When $\mu$ is a simple valuation $\sum_{i=1}^{n}a_{i}\delta_{x_{i}}$, it is
clear that the two sides of the equation coincide. Hence the two Scott-
continuous functions:

$\displaystyle\mu$ $\displaystyle\mapsto\int_{x\in X}\left(\int_{y\in
Y}f(x,y)d\nu\right)d\mu$ $\displaystyle\mu$ $\displaystyle\mapsto\int_{y\in
Y}\left(\int_{x\in X}f(x,y)d\mu\right)d\nu$

coincide on $\mathbf{V}_{\mathrm{f}}X$. By Lemma 5.8, they coincide on
$cl_{d}(\mathbf{V}_{\mathrm{f}}X)=\mathbf{V}_{m}X$. This finishes the case
where $\mu$ is minimal. The case where $\nu$ is minimal is symmetric. ∎

Given a tensorial strength $t$ for a monad $T$ on a category with finite
products, there is a dual tensorial strength $t^{\prime}$, where
$t^{\prime}_{X,Y}\colon TX\times Y\to T(X\times Y)$, obtained by swapping the
two arguments, applying $t_{X,Y}$, and then swapping back the roles of $X$ and
$Y$. Here $t^{\prime}_{X,Y}(\mu,y)(W)=\int_{x\in X}\chi_{W}(x,y)d\mu$. We can
then define two morphisms from $TX\times TY$ to $T(X\times Y)$, namely
${t^{\prime}}^{\dagger}_{X,Y}\circ t_{TX,Y}$ and $t^{\dagger}_{X,Y}\circ
t^{\prime}_{X,TY}$. The monad $T$ is _commutative_ when they coincide. The
connection between commutative monads and Fubini-Tonelli-like theorems is made
explicit by Kock [Kock, 2012]. For completeness, we prove the following
explicitly.

######  Proposition 5.10.

Let $X$, $Y$ be two dcpos. The maps $t^{\dagger}_{X,Y}\circ
t^{\prime}_{X,\mathbf{V}Y}$ and ${t^{\prime}}^{\dagger}_{X,Y}\circ
t_{\mathbf{V}X,Y}$ coincide on those pairs
$(\mu,\nu)\in\mathbf{V}X\times\mathbf{V}Y$ such that $\mu\in\mathbf{V}_{m}X$
or $\nu\in\mathbf{V}_{m}Y$.

###### Proof.

We have already seen that $t_{X,Y}(x,\nu)=\mathbf{V}(\lambda y\in
Y.(x,y))(\nu)$, for all $x$ and $\nu$. In other words,
$t_{X,Y}(x,\nu)=(\lambda y\in Y.\delta_{(x,y)})^{\dagger}(\nu)$. Similarly,
$t^{\prime}_{X,Z}(\mu,z)=(\lambda x\in X.\delta_{(x,z)})^{\dagger}(\mu)$.

For every $W\in{\mathcal{O}}(X\times Y)$,

$\displaystyle t^{\dagger}_{X,Y}(t^{\prime}_{X,\mathbf{V}Y}(\mu,\nu))(W)$
$\displaystyle=\int_{(x^{\prime},\nu)\in
X\times\mathbf{V}Y}t_{X,Y}(x^{\prime},\nu)(W)dt^{\prime}_{X,\mathbf{V}Y}(\mu,\nu)$
$\displaystyle=\int_{(x^{\prime},\nu)\in
X\times\mathbf{V}Y}t_{X,Y}(x^{\prime},\nu)(W)d(\lambda x\in
X.\delta_{(x,\nu)})^{\dagger}(\mu)$ $\displaystyle=\int_{x\in
X}\left(\int_{(x^{\prime},\nu)\in
X\times\mathbf{V}Y}t_{X,Y}(x^{\prime},\nu)(W)d\delta_{(x,\nu)}\right)d\mu$ by
(2) $\displaystyle=\int_{x\in X}t_{X,Y}(x,\nu)(W)d\mu$
$\displaystyle=\int_{x\in X}\left(\int_{y\in Y}\chi_{W}(x,y)d\nu\right)d\mu.$

Symmetrically,

$\displaystyle{t^{\prime}}^{\dagger}_{X,Y}(t_{\mathbf{V}X,Y}(\mu,\nu))(W)$
$\displaystyle=\int_{y\in Y}\left(\int_{x\in X}\chi_{W}(x,y)d\mu\right)d\nu.$

The result then follows from Theorem 5.9. ∎

######  Corollary 5.11.

$(\mathbf{V}_{m},\eta,\\_^{\dagger},t)$ is a commutative monad on
${\mathbf{Dcpo}}$.

######  Remark 5.12.

Strictly speaking, the Fubini-Tonelli theorem is more general, and states the
existence of a product measure. Here we obtain a minimal product valuation, as
follows. We write $\otimes$ for the morphism
${t^{\prime}}^{\dagger}_{X,Y}\circ t_{\mathbf{V}X,Y}$
($=t^{\dagger}_{X,Y}\circ t^{\prime}_{X,\mathbf{V}Y}$) from
$\mathbf{V}_{m}X\times\mathbf{V}_{m}Y$ to $\mathbf{V}_{m}(X\times Y)$, as with
any commutative monad [Kock, 2012, Section 5]. Then, for all
$\mu\in\mathbf{V}_{m}X$ and $\nu\in\mathbf{V}_{m}Y$, $\otimes(\mu,\nu)$, which
we prefer to write as $\mu\otimes\nu$, is in $\mathbf{V}_{m}(X\times Y)$.
Looking back at the computations we have done during the proof of Proposition
5.10,

$\displaystyle(\mu\otimes\nu)(W)$ $\displaystyle=\int_{x\in X}\left(\int_{y\in
Y}\chi_{W}(x,y)d\nu\right)d\mu$ $\displaystyle=\int_{y\in Y}\left(\int_{x\in
X}\chi_{W}(x,y)d\mu\right)d\nu$

for every $W\in{\mathcal{O}}(X\times Y)$. An easy computation, based on (2),
yields that, for every $f\in\mathcal{L}(X\times Y)$, $\int_{(x,y)\in X\times
Y}f(x,y)d(\mu\otimes\nu)$ is equal to any of the double integrals of (3).

As an additional benefit of the categorical approach, we obtain that the map
$\otimes\colon(\mu,\nu)\mapsto\mu\otimes\nu$ is Scott-continuous from
$\mathbf{V}_{m}X\times\mathbf{V}_{m}Y$ to $\mathbf{V}_{m}(X\times Y)$.

##  6 Measures on $\mathbb{R}$, minimal valuations on $\mathbf{I}\mathbb{R}$

All this is good, but aren’t we restricting continuous valuations too much by
only considering minimal valuations? And indeed, Lebesgue measure is not
minimal on $\mathbb{R}$, as we will soon see. But it _is_ minimal on
$\mathbf{I}\mathbb{R}$ and on $\mathbf{I}\mathbb{R}_{\bot}$. In fact, we will
see that _every_ measure $\mu$ on $\mathbb{R}$ is represented by a minimal
valuation on $\mathbf{I}\mathbb{R}$ and on $\mathbf{I}\mathbb{R}_{\bot}$.

To be more precise, since $\mathbb{R}$ is second-countable hence hereditarily
Lindelöf, every measure $\mu$ on $\mathbb{R}$ restricts to a continuous
valuation on $\mathbb{R}$. Its image valuation $i[\mu]$ by the embedding
$i\colon x\mapsto[x,x]$ of $\mathbb{R}$ into $\mathbf{I}\mathbb{R}$ (or
$\mathbf{I}\mathbb{R}_{\bot}$) is then a continuous valuation on
$\mathbf{I}\mathbb{R}$ (resp., $\mathbf{I}\mathbb{R}_{\bot}$). While the
former is rarely minimal, we will see that the latter always is.

Let us call _valuation_ on $X$ any strict, modular, monotonic map from
${\mathcal{O}}X$ to $\overline{\mathbb{R}}_{+}$; namely, we forgo the
continuity requirement. A valuation $\nu$ on $X$ is _point-continuous_ if and
only if for every open subset $U$ of $X$, for every $r\in\mathbb{R}_{+}$ such
that $r<\nu(U)$, there is a finite subset $A$ of $U$ such that, for every open
neighborhood $V$ of $A$, $\nu(V)>r$. The notion is due to Heckmann [Heckmann,
1996]. His main achievement was to show that the space $\mathbf{V}_{p}X$ of
point-continuous valuations over $X$, with the so-called weak topology, is a
sobrification of the space of simple valuations, also with the weak topology.
This can be used to show that there is also a commutative monad
$(\mathbf{V}_{p},\eta,\\_^{\dagger},t)$ on ${\mathbf{Dcpo}}$, but we will not
show this here. We will use the following results by Heckmann: every point-
continuous valuation is continuous; every simple valuation is point-
continuous; $\mathbf{V}_{p}X$ is sober, in particular it is a dcpo under the
pointwise ordering; in particular, every minimal valuation is point-
continuous.

Let $\lambda$ be the Lebesgue measure on $\mathbb{R}$, or ambiguously, its
restriction to the open subsets of $\mathbb{R}$, in which case we call it the
_Lebesgue valuation_.

######  Lemma 6.1.

The Lebesgue valuation $\lambda$ on $\mathbb{R}$ is not point-continuous,
hence not minimal.

###### Proof.

Let $U$ be any non-empty open subset of $\mathbb{R}$. Then $\lambda(U)>0$. Let
us pick any $r\in\mathbb{R}_{+}$ such that $r<\lambda(U)$. For every finite
subset $A$ of $U$, say of cardinality $n$, the open set
$V\mathrel{\buildrel\text{def}\over{=}}\bigcup_{x\in
A}]x-\epsilon,x+\epsilon[$, where $\epsilon>0$ is chosen so that
$2n\epsilon<r$, is an open neighborhood of $A$ but $\lambda(V)\leq\sum_{x\in
A}\lambda(]x-\epsilon,x+\epsilon[)=2n\epsilon<r$. ∎

######  Proposition 6.2.

For every measure $\mu$ on $\mathbb{R}$, and writing again $\mu$ for the
valuation it induces by restriction to ${\mathcal{O}}\mathbb{R}$, the image
valuation $i[\mu]$ is a minimal valuation on $\mathbf{I}\mathbb{R}$ (resp.,
$\mathbf{I}\mathbb{R}_{\bot}$).

###### Proof.

$\mathbf{I}\mathbb{R}$ (resp., $\mathbf{I}\mathbb{R}_{\bot}$) is a continuous
dcpo. Hence $\mathbf{V}(\mathbf{I}\mathbb{R})$ (resp.,
$\mathbf{V}(\mathbf{I}\mathbb{R}_{\bot})$) is also a continuous dcpo, with a
basis of simple valuations [Gierz et al., 2003, Theorem IV-9.16]. In
particular, $i[\mu]$ is a directed supremum of simple valuations, hence a
minimal valuation. ∎

######  Remark 6.3.

The proof of Proposition 6.2 shows, more generally, that, given any
hereditarily Lindelöf space $X$ with a topological embedding $i$ into some
continuous dcpo $P$, for every Borel measure $\mu$ on $X$, $i[\mu]$ is a
minimal valuation on $P$. Lawson showed that every Polish space $X$, not just
$\mathbb{R}$, has this property [Lawson, 1997].

$\mathbf{I}\mathbb{R}$ and $\mathbf{I}\mathbb{R}_{\bot}$ are even
$\omega$-continuous, namely, they have a countable basis. One can then show
that $i[\mu]$ is the supremum of a countable chain of simple valuations
(Exercise IV-9.29 of [Gierz et al., 2003] helps). It is interesting to see
that we can obtain such an explicit countable chain by elementary means. The
following construction, which has some common points with the so-called
Riemann-Stieltjes integral, is uniform, and only requires the knowledge of
$\mu(]a,b])$ for intervals $]a,b]$ with rational or dyadic endpoints.

######  Definition 6.4.

A _partition_ $P$ (of $\mathbb{R}$) is a finite non-empty subset of
$\mathbb{R}$. We write $P$ as $\\{a_{1}<\cdots<a_{n}\\}$ in order to make both
the elements and their order manifest, with $n\geq 1$. Every such partition
induces a finite subset $E_{P}$ of $\mathbf{I}\mathbb{R}$ defined by
$E_{P}\mathrel{\buildrel\text{def}\over{=}}\\{[a_{1},a_{2}],\cdots,[a_{n-1},a_{n}]\\}$.
If $n=1$, then $E_{P}$ is empty.

Let $\mathcal{P}$ be the set of all partitions of $\mathbb{R}$. A partition
$Q$ _refines_ $P$ if and only if $P\subseteq Q$.

Given any measure $\mu$ on $\mathbb{R}$, and any partition
$P\mathrel{\buildrel\text{def}\over{=}}\\{a_{1}<\cdots<a_{n}\\}$ of
$\mathbb{R}$, we let $\mu_{P}$ be the simple valuation
$\sum_{i=2}^{n}\mu(]a_{i-1},a_{i}]).\delta_{[a_{i-1},a_{i}]}$ on
$\mathbf{I}\mathbb{R}$ (resp., $\mathbf{I}\mathbb{R}_{\bot}$).

######  Remark 6.5.

The coefficient of $\delta_{[a_{i-1},a_{i}]}$ in $\mu_{P}$ is
$\mu(]a_{i-1},a_{i}])$, not $\mu([a_{i-1},a_{i}])$. The point is that
$\mu(]a_{i-1},a_{i}])+\mu(]a_{i},a_{i+1}])=\mu(]a_{i-1},a_{i+1}])$. Choosing
the coefficient to be $\mu([a_{i-1},a_{i}[)$ would work equally well.

######  Remark 6.6.

If $\mu$ is a probability valuation on $\mathbb{R}$ given by its cumulative
distribution function $F$ (namely,
$F(t)\mathrel{\buildrel\text{def}\over{=}}\mu(]-\infty,t])$), then $\mu_{P}$
is equal to $\sum_{i=2}^{n}(F(a_{i})-F(a_{i-1})).\delta_{[a_{i-1},a_{i}]}$,
and represents the process of picking the interval $[a_{i-1},a_{i}]$ with
probability $F(a_{i})-F(a_{i-1})$.

######  Theorem 6.7.

Let $\mu$ be any measure on $\mathbb{R}$. Then:

  1. 1.

for all partitions $P$ and $Q$ of $\mathbb{R}$, if $P\subseteq Q$ then
$\mu_{P}\leq\mu_{Q}$;

  2. 2.

$i[\mu]$ is the directed supremum of ${(\mu_{P})}_{P\in\mathcal{P}}$, and is
therefore a minimal valuation;

  3. 3.

for every dense subset $D$ of $\mathbb{R}$, $i[\mu]$ is also the directed
supremum of ${(\mu_{P})}_{P\in\mathcal{P}_{D}}$, where $\mathcal{P}_{D}$ is
the collection of partitions $P\subseteq D$.

###### Proof.

1\. Since $Q$ refines $P$, $Q$ is obtained by adding some points to $P$, and
it suffices to show the claim when we add just one point. Let us write $P$ as
$\\{a_{1}<\cdots<a_{n}\\}$, and let
$Q\mathrel{\buildrel\text{def}\over{=}}P\cup\\{a\\}$, where $a\not\in P$. If
$a<a_{1}$, then $\mu_{Q}$ is equal to
$\mu_{P}+\mu(]a,a_{1}]).\delta_{[a,a_{1}]}\geq\mu_{P}$; similarly if
$a>a_{n}$. Otherwise, let $j$ be the unique index such that $a_{j-1}<a<a_{j}$,
$2\leq j\leq n$. Then:

$\displaystyle\mu_{P}$ $\displaystyle=\sum_{\begin{subarray}{c}i=2\\\ i\neq
j\end{subarray}}^{n}\mu(]a_{i-1},a_{i}]).\delta_{[a_{i-1},a_{i}]}+\mu(]a_{j-1},a_{j}]).\delta_{[a_{j-1},a_{j}]}$
$\displaystyle=\sum_{\begin{subarray}{c}i=2\\\ i\neq
j\end{subarray}}^{n}\mu(]a_{i-1},a_{i}]).\delta_{[a_{i-1},a_{i}]}+\mu(]a_{j-1},a]).\delta_{[a_{j-1},a_{j}]}+\mu(]a,a_{j}]).\delta_{[a_{j-1},a_{j}]}$
$\displaystyle\leq\sum_{\begin{subarray}{c}i=2\\\ i\neq
j\end{subarray}}^{n}\mu(]a_{i-1},a_{i}]).\delta_{[a_{i-1},a_{i}]}+\mu(]a_{j-1},a]).\delta_{[a_{j-1},a]}+\mu(]a,a_{j}]).\delta_{[a,a_{j}]}=\mu_{Q},$

where the latter inequality is justified by the fact that $[a_{j-1},a]$ and
$[a,a_{j}]$ are both larger than or equal to $[a_{j-1},a_{j}]$, and that
$\mathbf{x}\mapsto\delta_{\mathbf{x}}$ is monotonic.

Item 2 is a special case of item 3, with
$D\mathrel{\buildrel\text{def}\over{=}}\mathbb{R}$. Hence we prove item 3
directly. Let $D$ be any dense subset of $\mathbb{R}$.

The family $\mathcal{P}_{D}$ is directed under inclusion, since
$\\{d\\}\in\mathcal{P}$ for any given $d\in D$, and since for all
$P,Q\in\mathcal{P}_{D}$, $P\cup Q$ is in $\mathcal{P}_{D}$. By item 1,
${(\mu_{P})}_{P\in\mathcal{P}_{D}}$ is therefore directed.

Let us fix an arbitrary Scott-open subset $\mathcal{U}$ of
$\mathbf{I}\mathbb{R}$ (resp., $\mathbf{I}\mathbb{R}_{\bot}$), and let
$U\mathrel{\buildrel\text{def}\over{=}}i^{-1}(\mathcal{U})$.

For every
$P\mathrel{\buildrel\text{def}\over{=}}\\{a_{1}<\cdots<a_{n}\\}\in\mathcal{P}_{D}$,
$\mu_{P}(\mathcal{U})\leq i[\mu](\mathcal{U})$. Indeed,

$\displaystyle\mu_{P}(\mathcal{U})$
$\displaystyle=\sum_{\begin{subarray}{c}2\leq i\leq n\\\
[a_{i-1},a_{i}]\in\mathcal{U}\end{subarray}}\mu(]a_{i-1},a_{i}])$
$\displaystyle=\mu\left(\bigcup_{\begin{subarray}{c}2\leq i\leq n\\\
[a_{i-1},a_{i}]\in\mathcal{U}\end{subarray}}]a_{i-1},a_{i}]\right)$
$\displaystyle\text{since the sets }]a_{i-1},a_{i}]\text{ are pairwise
disjoint}$ $\displaystyle\leq\mu(U)=i[\mu](\mathcal{U}).$

The last inequality is justified by the fact that for every $i$ with $2\leq
i\leq n$ such that $[a_{i-1},a_{i}]\in\mathcal{U}$, $[a_{i-1},a_{i}]$ is
included in $U$: for every $x\in[a_{i-1},a_{i}]$, $[a_{i-1},a_{i}]$ is below
$[x,x]$ in $\mathbf{I}\mathbb{R}$ (resp., $\mathbf{I}\mathbb{R}_{\bot}$), so
$[x,x]\in\mathcal{U}$, meaning that $x\in U$.

In order to show that $\sup_{P\in\mathcal{P}_{D}}\mu_{P}(\mathcal{U})\geq
i[\mu](\mathcal{U})$, we consider any $r\in\mathbb{R}_{+}$ such that
$r<i[\mu](\mathcal{U})=\mu(U)$, and we will show that there is a partition
$P\in\mathcal{P}_{D}$ such that $\mu_{P}(\mathcal{U})>r$. For every $x\in U$,
$[x,x]$ is in $\mathcal{U}$ and is the supremum of the chain of elements
$[x-\epsilon,x+\epsilon]$, $\epsilon>0$. Therefore there is a positive real
number $\epsilon_{x}$ such that $[x-\epsilon_{x},x+\epsilon_{x}]$ is in
$\mathcal{U}$. Since $D$ is dense in $\mathbb{R}$, we can find a subinterval
$[a_{x},b_{x}]$ such that $a_{x}$ and $b_{x}$ are in $D$, and $a_{x}<x<b_{x}$.
We note that $[a_{x},b_{x}]$ is also in $\mathcal{U}$. In particular,
$[a_{x},b_{x}]$, hence also $]a_{x},b_{x}[$, is included in $U$ for every
$x\in U$, so $U=\bigcup_{x\in U}]a_{x},b_{x}[$. We write the latter as the
directed union of the open sets
$U_{E}\mathrel{\buildrel\text{def}\over{=}}\bigcup_{x\in E}]a_{x},b_{x}[$,
where $E$ ranges over the finite subsets of $U$. Since $\mu$ restricted to the
open sets of $\mathbb{R}$ is a continuous valuation, there is a finite subset
$E$ of $U$ such that $r<\mu(U_{E})$.

We let $P$ be the collection of elements $a_{x}$ and $b_{x}$, $x\in E$. This
is an element of $\mathcal{P}_{D}$. Let us write $P$ as
$\\{c_{1}<\cdots<c_{n}\\}$. For every $x\in E$, $[a_{x},b_{x}]$ is an element
of $\mathcal{U}$, and is equal to $[c_{i_{x}},c_{j_{x}}]$ for some indices
$i_{x}$ and $j_{x}$ such that $1\leq i_{x}<j_{x}\leq n$. Then
$[c_{i-1},c_{i}]$ is larger than or equal to $[a_{x},b_{x}]$ for every $i$
with $i_{x}+1\leq i\leq j_{x}$, hence is also in $\mathcal{U}$. It follows
that $\mu_{P}(\mathcal{U})=\sum_{\begin{subarray}{c}2\leq i\leq n\\\
{}[c_{i-1},c_{i}]\in\mathcal{U}\end{subarray}}\mu(]c_{i-1},c_{i}])\geq\sum_{\begin{subarray}{c}x\in
E\\\ i_{x}+1\leq i\leq j_{x}\end{subarray}}\mu(]c_{i-1},c_{i}])$. The latter
is equal to $\mu(\bigcup_{\begin{subarray}{c}x\in E\\\ i_{x}+1\leq i\leq
j_{x}\end{subarray}}]c_{i-1},c_{i}])$, since the intervals $]c_{i-1},c_{i}]$
are pairwise disjoint. By definition of $i_{x}$ and $j_{x}$, this is larger
than or equal to $\mu(\bigcup_{x\in E}]a_{x},b_{x}])$, hence to
$\mu(\bigcup_{x\in E}]a_{x},b_{x}[)=\mu(U_{E})$. Therefore
$r<\mu_{P}(\mathcal{U})$, as desired. ∎

######  Corollary 6.8.

Let $\mu$ be any measure on $\mathbb{R}$. For every $n\in\mathbb{N}$, let the
partition $P_{n}$ consist of all integer multiples of $1/2^{n}$ between $-n$
and $n$. The minimal valuation $i[\mu]$ is the supremum of the countable chain
of simple valuations $\mu_{P_{n}}$, $n\in\mathbb{N}$.

###### Proof.

The family ${(P_{n})}_{n\in\mathbb{N}}$ is a subfamily of $\mathcal{P}_{D}$,
where $D$ is the set of dyadic numbers. It is in fact cofinal: every element
$P$ of $\mathcal{P}_{D}$ is refined by $P_{n}$ for some $n\in\mathbb{N}$,
namely for any $n$ larger than every element of $P$, every opposite of an
element of $P$, and such that every element of $P$ is an integer multiple of
$1/2^{n}$. It follows that ${(\mu_{P})}_{p\in\mathcal{P}_{D}}$ and
${(\mu_{P_{n}})}_{n\in\mathbb{N}}$ have the same supremum, and that is
$i[\mu]$ by Theorem 6.7, item 3. ∎

##  7 The ISPCF Calculus

We now come to the description of our calculus. This is a variant of SFPC, a
statistical variant of Fiore and Plotkin’s Fixed Point Calculus [Fiore and
Plotkin, 1994] due to Vákár, Kammar, and Staton [Vákár et al., 2019]. It is
also very close to the calculus PCFSS of [Dal Lago and Hoshino, 2019] and to
PPCF [Ehrhard et al., 2018]. Just like the latter, but contrarily to the other
languages we have mentioned, our calculus ISPCF (for _Interval_ statistical
PCF) is a call-by-name language.

Its algebra of types is as follows. One may naturally consider additional
types, such as more complex, recursively defined data types.

$\displaystyle\sigma,\tau,\ldots$
$\displaystyle::=\boldsymbol{\mathtt{unit}}\mid\boldsymbol{\mathtt{void}}\mid\boldsymbol{\mathtt{int}}\mid\boldsymbol{\mathtt{real}}\mid\sigma+\tau\mid\sigma\times\tau\mid\sigma\to\tau\mid
D\tau$

The types of the form $D\tau$ are called _distribution types_. The function
arrow $\to$ associates to the right, so that $\sigma\to\tau\to\lambda$
abbreviates $\sigma\to(\tau\to\lambda)$. Compared to the algebra of types of
SFPC, first, we keep a type $\boldsymbol{\mathtt{real}}$ of real numbers—exact
reals instead of true reals, though. Second, we do not require the presence of
recursive types as SFPC, so as to simplify the presentation. Accommodating
such type constructions is not central to our work, and can be handled through
bilimit constructions [Abramsky and Jung, 1994, Section 5]. (Showing adequacy,
as we will do in Section 10.2, in the presence of recursive types, is much
more challenging, though. See [Jia et al., 2021] for adequacy in the presence
of recursive types and discrete probabilistic choice, and [Pitts, 1993] for a
general technique for proving adequacy in the presence of recursive types.)
Third, and finally, we choose to have an explicit type of distributions former
$D$, in the style of Moggi’s Simple Metalanguage [Moggi, 1991]: arrow types
$\sigma\to\tau$ in SFPC are typically encoded as $\sigma\to D\tau$ in ISPCF.

$\begin{array}[]{cc}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 14.53682pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=29.07364pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\vdash x_{\sigma}\colon\sigma$}}}}&{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
7.78532pt\hbox{$\displaystyle\penalty 1\underline{f}\in\Sigma$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=37.23729pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\underline{f}\colon
typ(\underline{f})$}}}}\qquad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\vdash M\colon\sigma\to\sigma$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=52.77509pt\hbox{}}}\hbox{\kern
1.73201pt\hbox{$\displaystyle\vdash\boldsymbol{\mathtt{rec}}\;M\colon\sigma$}}}}\\\
\\\ {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
41.77728pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=83.55457pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\vdash\boldsymbol{\mathtt{sample}}[\mu]\colon
D\boldsymbol{\mathtt{real}}$}}}}&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt
plus 0.0001fil\hbox{\kern 15.97295pt\hbox{$\displaystyle\penalty 1\vdash
M\colon\boldsymbol{\mathtt{real}}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=76.0985pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\vdash\boldsymbol{\mathtt{score}}M\colon
D\boldsymbol{\mathtt{unit}}$}}}}\\\ \\\ {tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{\kern 17.73126pt\hbox{$\displaystyle\penalty 1\vdash
M\colon\tau$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=67.84775pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\vdash\lambda
x_{\sigma}.M\colon\sigma\to\tau$}}}}&{tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\vdash
M\colon\sigma\to\tau\quad\vdash N\colon\sigma$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=90.71593pt\hbox{}}}\hbox{\kern
24.60286pt\hbox{$\displaystyle\vdash MN\colon\tau$}}}}\\\ \\\
{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
10.40347pt\hbox{$\displaystyle\penalty 1\vdash M\colon\tau$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=53.19217pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\vdash\mathop{\boldsymbol{\mathtt{ret}}}\nolimits
M\colon D\tau$}}}}&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\vdash M\colon D\sigma\quad\vdash
N\colon D\tau$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=91.56026pt\hbox{}}}\hbox{\kern
2.4001pt\hbox{$\displaystyle\vdash\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x_{\sigma}\leftarrow
M};N\colon D\tau$}}}}\\\ \\\ {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\vdash M\colon\sigma\quad\vdash
N\colon\tau$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=80.00179pt\hbox{}}}\hbox{\kern
10.2776pt\hbox{$\displaystyle\langle
M,N\rangle\colon\sigma\times\tau$}}}}&{tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\vdash
M\colon\sigma\times\tau$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=53.0992pt\hbox{}}}\hbox{\kern
4.04669pt\hbox{$\displaystyle\vdash\pi_{1}M\colon\sigma$}}}}\quad{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\vdash
M\colon\sigma\times\tau$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=53.0992pt\hbox{}}}\hbox{\kern
4.71799pt\hbox{$\displaystyle\vdash\pi_{2}M\colon\tau$}}}}\\\ \\\
{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
12.02194pt\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\\\ \vdash
M\colon\sigma\end{array}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=59.43857pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\vdash\iota_{1}M\colon\sigma+\tau$}}}}\quad{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
12.69324pt\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\\\ \vdash
M\colon\tau\end{array}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=59.43857pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\vdash\iota_{2}M\colon\sigma+\tau$}}}}&{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\begin{array}[]{c}\vdash M\colon\sigma+\tau\\\ \vdash
N\colon\sigma\to\upsilon\quad\vdash P\colon\tau\to\upsilon\end{array}$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=85.60312pt\hbox{}}}\hbox{\kern
13.15405pt\hbox{$\displaystyle\boldsymbol{\mathtt{case}}MNP\colon\upsilon$}}}}\end{array}$
Figure 1: The typing rules of ISPCF

Just like SFPC, ISPCF is a typed higher-order functional language. Its terms
are given by the following grammar:

$\displaystyle M,N,P,\ldots$
$\displaystyle::=x_{\sigma}\mid\underline{f}\mid\boldsymbol{\mathtt{sample}}[\mu]\mid\boldsymbol{\mathtt{score}}M$
$\displaystyle\quad\mid\lambda x.M\mid
MN\mid\boldsymbol{\mathtt{rec}}\;M\mid\mathop{\boldsymbol{\mathtt{ret}}}\nolimits
M\mid\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x\leftarrow M};N$
$\displaystyle\quad\mid\langle
M,N\rangle\mid\pi_{1}M\mid\pi_{2}M\mid\iota_{1}M\mid\iota_{2}M\mid\boldsymbol{\mathtt{case}}MNP$

where $x_{\sigma}$ (and also $y_{\tau}$, $z_{\upsilon}$, etc.) range over
variables, whose type appears explicitly as a subscript (which we will often
omit for clarity), $\underline{f}$ ranges over a fixed set $\Sigma$ of
constants, and $\mu$ ranges over a fixed set $\mathcal{M}$ of measures on
$\mathbb{R}$. We assume a countably infinite supply of variables of each type.

We assume a function $typ$ from $\Sigma$ to the set of ISPCF types:
$typ(\underline{f})$ is the type of $\underline{f}$, by definition.

Amongst those we require a constant $\underline{*}$ of type
$\boldsymbol{\mathtt{unit}}$, and constants $\underline{n}$, one for each
integer $n\in\mathbb{Z}$, with $typ(\underline{n})=\boldsymbol{\mathtt{int}}$.

We may include constants $\underline{q}$, one for each rational number $q$,
with $typ(\underline{q})=\boldsymbol{\mathtt{real}}$. We may also include
constants for non-rational numbers, such as $\underline{\pi}$; and standard
numerical primitives such as $\underline{\sin}$, $\underline{\mathrm{exp}}$ or
$\underline{\log}$, with
$typ(\underline{\sin})=typ(\underline{\mathrm{exp}})=typ(\underline{\log})=\boldsymbol{\mathtt{real}}\to\boldsymbol{\mathtt{real}}$,
meant to implement the sine, exponential and logarithm functions respectively,
as in SFPC.

We will see later that we can define a type $\boldsymbol{\mathtt{bool}}$ of
Booleans, namely $\boldsymbol{\mathtt{void}}+\boldsymbol{\mathtt{void}}$, and
two terms $\underline{\mathrm{true}}$ and $\underline{\mathrm{false}}$ of type
$\boldsymbol{\mathtt{bool}}$. Given that, we may include a sign test
$\underline{\text{pos}}\colon\boldsymbol{\mathtt{real}}\to\boldsymbol{\mathtt{bool}}$,
with the intention that $\underline{\text{pos}}\;M$ evaluates to the value
$\mathrm{true}$ of $\underline{\mathrm{true}}$ if $M$ evaluates to a positive
real number, and to the value $\mathrm{false}$ of $\underline{\mathrm{false}}$
if $M$ evaluates to a negative real number (we will discuss semantics soon).

The constructs $\mathop{\boldsymbol{\mathtt{ret}}}\nolimits$ and
$\mathop{\boldsymbol{\mathtt{do}}}\nolimits$ are standard monadic constructs;
$\boldsymbol{\mathtt{rec}}$ is a fixed-point combinator, and we assume the
usual $\alpha$-renaming conventions. Crucially, we keep the two iconic
primitives of SFPC: $\boldsymbol{\mathtt{sample}}$ (or rather,
$\boldsymbol{\mathtt{sample}}[\mu]$) and $\boldsymbol{\mathtt{score}}$. The
typing rules are given in Figure 1.

We also write $M;N$ for
$\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x\leftarrow M};N$, where $x$ is a
fresh variable—one that is not free in $N$.

While SFPC is call-by-value, ISPCF is a call-by-name language, just like
Hakaru [Shan and Ramsey, 2017] or PPCF [Ehrhard et al., 2018]. (Hakaru,
however, lacks higher-order functions and recursion.) This slightly simplifies
the denotational semantics, and does not preclude us from using a call-by-
value style of programming if we so desire. Namely, call-by-value application
$M@N$ of $M\colon\sigma\to D\tau$ to $N\colon D\sigma$ is defined as
$\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x\leftarrow N};Mx$, where $x$ is a
fresh variable. We will return to this point in Section 9.1.

##  8 The Denotational Semantics of ISPCF

The semantics $\left\llbracket{\tau}\right\rrbracket$ of types $\tau$ is given
by induction on $\tau$:

$\begin{array}[]{c}\left\llbracket{\boldsymbol{\mathtt{unit}}}\right\rrbracket\mathrel{\buildrel\text{def}\over{=}}\\{*,\bot\\}\quad\left\llbracket{\boldsymbol{\mathtt{void}}}\right\rrbracket\mathrel{\buildrel\text{def}\over{=}}\\{\bot\\}\quad\quad\left\llbracket{\boldsymbol{\mathtt{int}}}\right\rrbracket\mathrel{\buildrel\text{def}\over{=}}\mathbb{Z}_{\bot}\quad\left\llbracket{\boldsymbol{\mathtt{real}}}\right\rrbracket\mathrel{\buildrel\text{def}\over{=}}\mathbf{I}\mathbb{R}_{\bot}\\\
\left\llbracket{\sigma\to\tau}\right\rrbracket\mathrel{\buildrel\text{def}\over{=}}[\left\llbracket{\sigma}\right\rrbracket\to\left\llbracket{\tau}\right\rrbracket]\quad\left\llbracket{D\tau}\right\rrbracket\mathrel{\buildrel\text{def}\over{=}}\mathbf{V}_{m}(\left\llbracket{\tau}\right\rrbracket)\\\
\left\llbracket{\sigma\times\tau}\right\rrbracket\mathrel{\buildrel\text{def}\over{=}}\left\llbracket{\sigma}\right\rrbracket\times\left\llbracket{\tau}\right\rrbracket\quad\left\llbracket{\sigma+\tau}\right\rrbracket\mathrel{\buildrel\text{def}\over{=}}(\left\llbracket{\sigma}\right\rrbracket+\left\llbracket{\tau}\right\rrbracket)_{\bot}.\end{array}$

In $\left\llbracket{\boldsymbol{\mathtt{unit}}}\right\rrbracket$, we have
$\bot<*$. $\mathbb{Z}_{\bot}$ is $\mathbb{Z}$ plus a fresh element $\bot$,
ordered so that $\bot$ is least and all integers are pairwise incomparable.
$[X\to Y]$ denotes the dcpo of Scott-continuous maps from the dcpo $X$ to the
dcpo $Y$, ordered pointwise. Given any two pointed dcpos $X$ and $Y$, $X\times
Y$ is their ordinary product, ordered pointwise. $X+Y$ is their coproduct, and
consists of elements $(1,x)$ with $x\in X$, $(2,y)$ with $y\in Y$, so that
$(1,x)\leq(1,x^{\prime})$ if and only if $x\leq x^{\prime}$,
$(2,y)\leq(2,y^{\prime})$ if and only if $y\leq y^{\prime}$, and $(1,x)$ and
$(2,y)$ are incomparable.

$\displaystyle\left\llbracket{x_{\sigma}}\right\rrbracket\rho$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}\rho(x_{\sigma})$
$\displaystyle\left\llbracket{\underline{f}}\right\rrbracket\rho$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}f$
$\displaystyle\left\llbracket{\boldsymbol{\mathtt{sample}}[\mu]}\right\rrbracket\rho$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}i[\mu]$
$\displaystyle\left\llbracket{\boldsymbol{\mathtt{score}}M}\right\rrbracket\rho$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}|\left\llbracket{M}\right\rrbracket\rho|.\delta_{*}$
$\displaystyle\left\llbracket{\lambda x_{\sigma}.M}\right\rrbracket\rho$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}\lambda
V\in\left\llbracket{\sigma}\right\rrbracket.\left\llbracket{M}\right\rrbracket(\rho[x_{\sigma}\mapsto
V])\mskip-180.0mu$ $\displaystyle\left\llbracket{MN}\right\rrbracket\rho$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}\left\llbracket{M}\right\rrbracket\rho(\left\llbracket{N}\right\rrbracket\rho)\mskip-20.0mu$
$\displaystyle\left\llbracket{\boldsymbol{\mathtt{rec}}\;M}\right\rrbracket\rho$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}\mathop{\text{lfp}}(\left\llbracket{M}\right\rrbracket\rho)$
$\displaystyle\left\llbracket{\mathop{\boldsymbol{\mathtt{ret}}}\nolimits
M}\right\rrbracket\rho$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}\delta_{\left\llbracket{M}\right\rrbracket\rho}$
$\displaystyle\left\llbracket{\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x_{\sigma}\leftarrow
M};N}\right\rrbracket\rho$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}(\left\llbracket{\lambda
x_{\sigma}.N}\right\rrbracket\rho)^{\dagger}(\left\llbracket{M}\right\rrbracket\rho)$
$\displaystyle\left\llbracket{\langle M,N\rangle}\right\rrbracket\rho$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}(\left\llbracket{M}\right\rrbracket\rho,\left\llbracket{N}\right\rrbracket\rho)$
$\displaystyle\left\llbracket{\pi_{i}M}\right\rrbracket\rho$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}\lambda(V_{1},V_{2}).V_{i}$
$\displaystyle\left\llbracket{\boldsymbol{\mathtt{case}}MNP}\right\rrbracket\rho$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}\left\\{\begin{array}[]{ll}\left\llbracket{N}\right\rrbracket\rho(a)&\text{if
}\left\llbracket{M}\right\rrbracket\rho=(1,a)\\\
\left\llbracket{P}\right\rrbracket\rho(b)&\text{if
}\left\llbracket{M}\right\rrbracket\rho=(2,b)\\\
\bot&\text{otherwise}\end{array}\right.\mskip-80.0mu$
$\displaystyle\left\llbracket{\iota_{i}M}\right\rrbracket\rho$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}(i,\left\llbracket{M}\right\rrbracket\rho)$
Figure 2: The semantics of ISPCF

The denotational semantics $\left\llbracket{M}\right\rrbracket\rho$ of each
term $M$, in the environment $\rho$, is given in Figure 2. Environments map
variables $x_{\sigma}$ to elements of the corresponding dcpo
$\left\llbracket{\sigma}\right\rrbracket$. The notation $\rho[x\mapsto V]$
stands for the environment that maps $x$ to $V$ and every other variable $y$
to $\rho(y)$. The least fixed point operator $\mathop{\text{lfp}}$ on every
pointed dcpo $X$ is such that
$\mathop{\text{lfp}}(f)\mathrel{\buildrel\text{def}\over{=}}\bigcup_{n\in\mathbb{N}}f^{n}(\bot)$
for every $f\in[X\to X]$. In the denotation of
$\boldsymbol{\mathtt{case}}MNP$, $\left\llbracket{N}\right\rrbracket\rho(a)$
is the application of $\left\llbracket{N}\right\rrbracket\rho$, which is a
function, to the value $a$.

Let us make a few comments. We assume an element
$f\in\left\llbracket{\tau}\right\rrbracket$ for each constant
$\underline{f}\in\Sigma$ of type $\tau$. Hence, for example, we have elements
$\pi\in\left\llbracket{\boldsymbol{\mathtt{real}}}\right\rrbracket$,
$\sin,\mathrm{exp},\log\in\left\llbracket{\boldsymbol{\mathtt{real}}\to\boldsymbol{\mathtt{real}}}\right\rrbracket$,
etc. The case of sign tests $\underline{\text{pos}}$ is interesting: by an
easy argument based on the fact that the real line is connected, there is no
Scott-continuous function from $\mathbf{I}\mathbb{R}_{\bot}$ to
$\left\llbracket{\boldsymbol{\mathtt{bool}}}\right\rrbracket$, where
$\boldsymbol{\mathtt{bool}}\mathrel{\buildrel\text{def}\over{=}}\boldsymbol{\mathtt{unit}}+\boldsymbol{\mathtt{unit}}$,
which would map the elements $[a,a]$ with $a\geq 0$ to
$\mathrm{true}\mathrel{\buildrel\text{def}\over{=}}(1,*)$, and those with
$a<0$ to $\mathrm{false}\mathrel{\buildrel\text{def}\over{=}}(2,*)$ (see
[Edalat and Escardó, 2000, Proposition 2.4] for a generalization of this
observation). And indeed, such tests are not computable. One reasonable choice
for the semantics of $\underline{\text{pos}}$, if we decide to include it, is
to define $\text{pos}([a,b])$ as $\mathrm{true}$ if $a>0$, $\mathrm{false}$ if
$b<0$, and $\bot$ otherwise.

The semantics of $\boldsymbol{\mathtt{sample}}[\mu]$, namely $i[\mu]$, is the
minimal valuation associated with the measure $\mu$ on $\mathbb{R}$, see
Theorem 6.7.

For every $\mathbf{a}\in\mathbf{I}\mathbb{R}^{\star}$, the notation
$|\mathbf{a}|$ denotes $0$ if $\mathbf{a}=\bot$ or if $\mathbf{a}=[a,b]$ with
$a\leq 0\leq b$, $a$ if $\mathbf{a}=[a,b]$ with $a\geq 0$, and $-b$ if
$\mathbf{a}=[a,b]$ with $b\leq 0$.

This, as well as the semantics of $\underline{\text{pos}}$, is an instance of
a more general, well-known domain-theoretic construction. A _bc-domain_ is a
continuous dcpo in which every subset with an upper bound has a least upper
bound. The bc-domains with their Scott topology are exactly the _densely
injective_ $T_{0}$ topological spaces, namely the $T_{0}$ spaces $Z$ such
that, for every dense subset $X$ of any space $Y$, every continuous map
$f\colon X\to Z$ extends to a continuous map from the whole of $Y$ to $Z$
[Gierz et al., 2003, Proposition II-3.11]. There is even a pointwise largest
such extension $f^{*}$, defined by
$f^{*}(y)\mathrel{\buildrel\text{def}\over{=}}\sup_{U\in{\mathcal{O}}Y,y\in
U}\inf_{x\in U\cap X}f(x)$ [Gierz et al., 2003, Proposition II-3.9]. The
latter formula makes sense and defines a continuous map $f^{*}$ even when $f$
is not continuous, but in that case $f^{*}$ will fail to extend $f$.

One can check that
$\left\llbracket{\boldsymbol{\mathtt{unit}}}\right\rrbracket$,
$\left\llbracket{\boldsymbol{\mathtt{void}}}\right\rrbracket$,
$\left\llbracket{\boldsymbol{\mathtt{int}}}\right\rrbracket$,
$\left\llbracket{\boldsymbol{\mathtt{real}}}\right\rrbracket$, and in fact
$\left\llbracket{\tau}\right\rrbracket$ for any type $\tau$ that does not
contain the $D$ operator, are bc-domains. In particular, every continuous map
$g\colon\mathbb{R}\to\mathbb{R}$ induces a continuous map
$\hat{g}\mathrel{\buildrel\text{def}\over{=}}(i\circ
g)^{*}\colon\mathbf{I}\mathbb{R}_{\bot}\to\mathbf{I}\mathbb{R}_{\bot}$ that
extends $i\circ g$, namely: $\hat{g}([x,x])=[g(x),g(x)]$ for every
$x\in\mathbb{R}$. In doing so, we silently equate $\mathbb{R}$ with a subspace
of $\mathbf{I}\mathbb{R}_{\bot}$ through $i$, and it is easy to realize that
$\mathbb{R}$ is indeed dense in $\mathbf{I}\mathbb{R}_{\bot}$.

This applies to $\sin$, $\cos$, $\exp$, notably. The case of $\log$ is
slightly different, since it is only defined on
$\mathbb{R}_{+}\setminus\\{0\\}$. In that case, the map
$f\colon\mathbb{R}\to\mathbf{I}\mathbb{R}_{\bot}$ that sends every positive
real number $x$ to $i(\log x)=[\log x,\log x]$, and all other numbers to
$\bot$, is continuous, and it is natural to define
$\log\colon\mathbf{I}\mathbb{R}_{\bot}\to\mathbf{I}\mathbb{R}_{\bot}$ as its
largest continuous extension. The notation $|\mathbf{a}|$, as used in the
semantics of $\boldsymbol{\mathtt{score}}\;M$ (where $\mathbf{a}$ is
$\left\llbracket{M}\right\rrbracket\rho$), is equal to $f^{*}$ where $f$ is
the absolute value map from $\mathbb{R}$ to $\mathbb{R}$, and therefore
extends it to $\mathbf{I}\mathbb{R}_{\bot}$. The semantics pos of
$\underline{\text{pos}}$ is $f^{*}$, where $f$ is the non-continuous map that
sends every positive number to $\mathrm{true}$ and all other numbers to
$\mathrm{false}$. Hence $f^{*}$ does not extend $f$, but we still have
$f^{*}([a,a])=f(a)$ if $a\neq 0$.

It is clear that for each derivable judgment $\vdash M\colon\tau$, for every
environment $\rho$, $\left\llbracket{M}\right\rrbracket\rho$ is a well-defined
element of $\left\llbracket{\tau}\right\rrbracket$. In particular, the least
fixed point $\mathop{\text{lfp}}(\left\llbracket{M}\right\rrbracket\rho)$ is
well-defined in the definition of
$\left\llbracket{\boldsymbol{\mathtt{rec}}\;M}\right\rrbracket\rho$, because
$\left\llbracket{\tau}\right\rrbracket$ is a pointed dcpo; this is shown by
induction on $\tau$, and the least element of
$\left\llbracket{D\tau}\right\rrbracket$ is the constant zero valuation. We
also mention the following case, which shows where tensorial strengths are
required. There is a morphism:

$\textstyle{TX\times[X\to
TY]\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{t^{\prime}_{X,Y}}$$\textstyle{T(X\times[X\to
TY])\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathrm{App}^{\dagger}}$$\textstyle{TY}$

where
$X\mathrel{\buildrel\text{def}\over{=}}\left\llbracket{\sigma}\right\rrbracket$,
$Y\mathrel{\buildrel\text{def}\over{=}}\left\llbracket{\tau}\right\rrbracket$,
$T$ is the $\mathbf{V}_{m}$ monad, $t^{\prime}$ is its dual tensorial
strength, and $\mathrm{App}$ is application. Applying this to
$(\left\llbracket{M}\right\rrbracket\rho,\left\llbracket{\lambda
x_{\sigma}.N}\right\rrbracket\rho)$ yields the semantic value
$\left\llbracket{\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x_{\sigma}\leftarrow
M};N}\right\rrbracket\rho$.

######  Remark 8.1.

By standard category-theoretic arguments, since $\mathbf{V}_{m}$ is
commutative, the following equation holds when $x$ is not free in $N$ and $y$
is not free in $M$:

$\mskip-40.0mu\left\llbracket{\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x\leftarrow
M};\mathop{\boldsymbol{\mathtt{do}}}\nolimits{y\leftarrow
N};P}\right\rrbracket\rho=\left\llbracket{\mathop{\boldsymbol{\mathtt{do}}}\nolimits{y\leftarrow
N};\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x\leftarrow
M};P}\right\rrbracket\rho.$

It was already argued [Vákár et al., 2019, Comments after Corollary 6.11] that
this semantic equation is crucial in program transformation techniques such as
disintegration-based Bayesian inference [Shan and Ramsey, 2017] as implemented
in the Hakaru system [Narayanan et al., 2016]. As in [Vákár et al., 2019],
this equation is valid at all types in our semantics.

##  9 Examples

###  9.1 The call-by-value versus call-by-name question

A recurring paradox in the theory of higher-order probabilistic programming
languages is the following: what should the value of $(\lambda
x.x=x)(\mathtt{rand}())$ be, where $\mathtt{rand}()$ returns a random number?
Since $x=x$ is universally true, one expects this program to always return
true. In call-by-name, one also expects $\beta$-reduction to be a sound
reduction rule, so that this value should also be equal to
$\mathtt{rand}()=\mathtt{rand}()$. Unfortunately, the latter draws _two_
independent random numbers, and may return false.

This problem is avoided in _call-by-value_ languages, which force
$\mathtt{rand}()$ to be evaluated first, and only once.

This need not be a problem in call-by-name languages such as ISPCF. This is
well-known, but we would like this point to be clear. In the call-by-name
language PPCF, the issue is solved by using a $\mathtt{let}(x,M,N)$ construct
that evaluates $M$, binds the resulting value to $x$ and then evaluates $N$
[Ehrhard et al., 2018, Example 3.10]. In ISPCF,
$\mathop{\boldsymbol{\mathtt{do}}}\nolimits$ may serve a similar purpose, as
we now demonstrate.

Let us build a simple uniform random number generator $\mathtt{randbool}$ on
$\boldsymbol{\mathtt{bool}}$. We recall that
$\boldsymbol{\mathtt{bool}}\mathrel{\buildrel\text{def}\over{=}}\boldsymbol{\mathtt{unit}}+\boldsymbol{\mathtt{unit}}$.
We define $\underline{\mathrm{true}}$ as $\iota_{1}\underline{*}$; its
semantics is $\mathrm{true}=(1,*)$; and $\underline{\mathrm{false}}$ as
$\iota_{2}\underline{*}$, whose semantics is $\mathrm{false}=(2,*)$. If $M$
has type $\boldsymbol{\mathtt{bool}}$, we also define
$\boldsymbol{\mathtt{if}}MNP$ as an abbreviation for
$\boldsymbol{\mathtt{case}}M(\lambda x_{1}.\allowbreak N)(\lambda x_{2}.P)$,
where $x_{1}$ and $x_{2}$ are fresh variables.

In order to implement $\mathtt{randbool}$, we assume we have a term
$\boldsymbol{\mathtt{sample}}[\lambda_{1}]$, where $\lambda_{1}$ is the
uniform measure on $[0,1]$, namely: for every measurable subset $E$ of
$\mathbb{R}$,
$\lambda_{1}(E)\mathrel{\buildrel\text{def}\over{=}}\lambda(E\cap[0,1])$. We
also assume the $\underline{\text{pos}}$ primitive, and subtraction $-$. We
define $\mathtt{randbool}$ as follows.

$\displaystyle\mathtt{randbool}$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x_{\boldsymbol{\mathtt{real}}}\leftarrow\boldsymbol{\mathtt{sample}}[\lambda_{1}]};\mathop{\boldsymbol{\mathtt{ret}}}\nolimits(\underline{\text{pos}}(x-\underline{0.5}))$

For every environment $\rho$,
$\left\llbracket{\mathtt{randbool}}\right\rrbracket\rho$ is the continuous
valuation
$\frac{1}{2}\delta_{\mathrm{true}}+\frac{1}{2}\delta_{\mathrm{false}}$.

Let $\mathtt{eqbool}\mathrel{\buildrel\text{def}\over{=}}\lambda x.\lambda
y.\boldsymbol{\mathtt{if}}\;x\;{(\boldsymbol{\mathtt{if}}\;y\;\underline{\mathrm{true}}\;\underline{\mathrm{false}})}\;{(\boldsymbol{\mathtt{if}}\;y\;\underline{\mathrm{false}}\;\underline{\mathrm{true}})}$,
and we abbreviate $\mathtt{eqbool}\;MN$ as $M=N$, for all
$M,N\colon\boldsymbol{\mathtt{bool}}$. One cannot write $(\lambda
x_{\boldsymbol{\mathtt{bool}}}.x=x)(\mathtt{randbool})$ directly, because
$\mathtt{randbool}$ has type $D\boldsymbol{\mathtt{bool}}$, not
$\boldsymbol{\mathtt{bool}}$. Sampling from a distribution must be done
through $\mathop{\boldsymbol{\mathtt{do}}}\nolimits$, and we have (at least)
two choices. The term:

$\displaystyle\mathop{\boldsymbol{\mathtt{do}}}\nolimits{b_{\boldsymbol{\mathtt{bool}}}\leftarrow\mathtt{randbool}};\;{\mathop{\boldsymbol{\mathtt{ret}}}\nolimits((\lambda
x_{\boldsymbol{\mathtt{bool}}}.x=x)b)}$

first samples, obtaining a random Boolean value $b$, which is then passed to
$\lambda x_{\boldsymbol{\mathtt{bool}}}.x=x$. This term has semantics
$\delta_{\mathrm{true}}$; in other words, it is a probabilistic process that
returns $\mathrm{true}$ with probability one. Or we may defer sampling as
follows:

$\displaystyle(\lambda
x_{D\boldsymbol{\mathtt{bool}}}.\mathop{\boldsymbol{\mathtt{do}}}\nolimits{b_{1}\leftarrow
x};\mathop{\boldsymbol{\mathtt{do}}}\nolimits{b_{2}\leftarrow
x};\mathop{\boldsymbol{\mathtt{ret}}}\nolimits(b_{1}=b_{2}))\mathtt{randbool}.$

The semantics of that term is
$\frac{1}{2}\delta_{\mathrm{true}}+\frac{1}{2}\delta_{\mathrm{false}}$: the
probability that the two independent Boolean values $b_{1}$ and $b_{2}$ are
equal is only $1/2$.

###  9.2 Rejection sampling

Let us imagine that you have a probability measure $\mu$ on a space $X$, let
$A$ be a measurable subset of $X$ such that $\mu(A)\neq 0$. Then there is a
conditional probability measure $\mu_{A}$, defined by
$\mu_{A}(E)\mathrel{\buildrel\text{def}\over{=}}\mu(E)/\mu(A)$ for every
measurable subset $E$ of $A$. Rejection sampling allows one to draw an element
at random in $A$ with probability $\mu_{A}$, by drawing an element in $X$ with
probability $\mu$ until we find one in $A$. This terminates with probability
$1$, and in fact in $1/\mu(A)$ trials on average.

Let $\tau$ be any type. We consider the following ISPCF term:

$\displaystyle\mathtt{rej}$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}\lambda p_{D\tau}.\lambda
sel_{\tau\to D\boldsymbol{\mathtt{bool}}}.$
$\displaystyle\qquad\boldsymbol{\mathtt{rec}}(\lambda
r_{D\tau}.\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x_{\tau}\leftarrow p};$
$\displaystyle\qquad\qquad\qquad\quad\mathop{\boldsymbol{\mathtt{do}}}\nolimits{b_{\boldsymbol{\mathtt{bool}}}\leftarrow
sel\;x};$
$\displaystyle\qquad\qquad\qquad\quad\boldsymbol{\mathtt{if}}\;{b}\;{(\mathop{\boldsymbol{\mathtt{ret}}}\nolimits
x)}\;{r}).$

Intuitively, $\mathtt{rej}$ takes a distribution $p$ as input, a selection
function $sel$, and draws $x$ at random with probability $p$ until $sel\;x$
returns $\mathrm{true}$. We allow $sel$ to return an object of type
$D\boldsymbol{\mathtt{bool}}$, not $\boldsymbol{\mathtt{bool}}$, in order to
allow $sel$ to do some random computations as well.

For every environment $\rho$,
$\left\llbracket{\mathtt{rej}}\right\rrbracket\rho$ is a function that takes a
minimal valuation $\mu$ (bound to the variable $p$) and a selection function
$s\in\left\llbracket{\tau\to D\boldsymbol{\mathtt{bool}}}\right\rrbracket$
(bound to $sel$) to a minimal valuation $\nu_{|sel}$, which we now elucidate.
By definition, $\nu_{|sel}$ is the least minimal valuation such that
$\nu_{|sel}=\Phi(\nu_{|sel})$, where:

$\displaystyle\Phi(\nu)$
$\displaystyle=\left\llbracket{\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x\leftarrow
p};\mathop{\boldsymbol{\mathtt{do}}}\nolimits{b\leftarrow
sel\;x};\boldsymbol{\mathtt{if}}\;b\;{(\mathop{\boldsymbol{\mathtt{ret}}}\nolimits
x)}\;r}\right\rrbracket\rho[p\mapsto\mu,sel\mapsto s,r\mapsto\nu]$

For every selection function $s\in\left\llbracket{\tau\to
D\boldsymbol{\mathtt{bool}}}\right\rrbracket$, for every
$x\in\left\llbracket{\tau}\right\rrbracket$, we may write $s(x)$ as
$s_{\mathrm{true}}(x).\delta_{\mathrm{true}}+s_{\mathrm{false}}(x).\delta_{\mathrm{false}}+s_{(1,\bot)}(x).\delta_{(1,\bot)}+s_{(2,\bot)}.\delta_{(2,\bot)}+s_{\bot}(x).\delta_{\bot}$.
For simplicity, let us assume that
$s_{\bot}(x)=s_{(1,\bot)}(x)=s_{(2,\bot)}(x)=0$. In other words, the
probability of $s(x)$ returning a non-terminating Boolean is zero. Expanding
the semantics shows that $\Phi(\nu)$ is the continuous valuation such that,
for every $U\in{\mathcal{O}}{\left\llbracket{\tau}\right\rrbracket}$,

$\displaystyle\Phi(\nu)(U)$
$\displaystyle=\int_{x\in\left\llbracket{\tau}\right\rrbracket}(s_{\mathrm{true}}(x).\chi_{U}(x)+s_{\mathrm{false}}(x).\nu(U))d\mu.$

Given any space $X$, any continuous valuation $\nu$ on $X$, and any continuous
map $g\colon X\to\overline{\mathbb{R}}_{+}$, there is a continuous valuation
$g\cdot\nu$ on $X$ defined by
$(g\cdot\nu)(U)\mathrel{\buildrel\text{def}\over{=}}\int_{x\in
X}g(x)\chi_{U}(x)d\nu$, for every $U\in{\mathcal{O}}X$. This formula
characterizes $g\cdot\nu$ as the continuous valuation obtained from $\nu$ by
applying the _density function_ $g$; a notation that is sometimes used for
$g\cdot\nu$ is $gd\nu$.

This abbreviation allows us to rewrite $\Phi(\nu)(U)$ as follows. The value
$(s_{\mathrm{false}}\cdot\mu)(\left\llbracket{\tau}\right\rrbracket)$ is the
total mass
$\int_{x\in\left\llbracket{\tau}\right\rrbracket}s_{\mathrm{false}}(x)d\mu$ of
$s_{\mathrm{false}}\cdot\mu$ on $\left\llbracket{\mu}\right\rrbracket$.

$\displaystyle\Phi(\nu)$
$\displaystyle=s_{\mathrm{true}}\cdot\mu+(s_{\mathrm{false}}\cdot\mu)(\left\llbracket{\tau}\right\rrbracket).\nu.$

Let us solve the equation $\nu=\Phi(\nu)$ for $\nu$. One may compute the least
solution as $\sup_{n\in\mathbb{N}}\Phi^{n}(0)$, where $0$ denotes the zero
valuation, but it is easier to solve the equation directly.

If $(s_{\mathrm{false}}\cdot\mu)(\left\llbracket{\tau}\right\rrbracket)<1$,
then there are at most two solutions to the equation $\nu=\Phi(\nu)$. The
smaller one is:

$\displaystyle\frac{1}{1-(s_{\mathrm{false}}\cdot\mu)(\left\llbracket{\tau}\right\rrbracket)}s_{\mathrm{true}}\cdot\mu,$

and this is the value of
$\left\llbracket{\mathtt{rej}}\right\rrbracket\rho(\mu)(s)$. When
$0<(s_{\mathrm{false}}\cdot\mu)(\left\llbracket{\tau}\right\rrbracket)<1$,
there is another solution, and that is the continuous valuation that maps
every non-empty open subset of $\left\llbracket{\tau}\right\rrbracket$ to
$+\infty$, the _largest_ continuous valuation on
$\left\llbracket{\tau}\right\rrbracket$. (Yes, that is a minimal valuation,
since it is simply the directed supremum of all simple valuations whatsoever.)

If $(s_{\mathrm{false}}\cdot\mu)(\left\llbracket{\tau}\right\rrbracket)=1$,
then we are typically in the case of sampling with respect to a set of measure
zero. The sitation is more complicated in general, since
$s_{\mathrm{false}}+s_{\mathrm{true}}$ may not be equal to $1$: the condition
$(s_{\mathrm{false}}\cdot\mu)(\left\llbracket{\tau}\right\rrbracket)=1$
imposes no constraint on $s_{\mathrm{true}}\cdot\mu$.

The general case where
$(s_{\mathrm{false}}\cdot\mu)(\left\llbracket{\tau}\right\rrbracket)\geq 1$ is
probably even less intuitive. Let
$A\mathrel{\buildrel\text{def}\over{=}}(s_{\mathrm{false}}\cdot\mu)(\left\llbracket{\tau}\right\rrbracket)$.
The equation $\nu=\Phi(\nu)$ reduces to $\nu=s_{\mathrm{true}}\cdot\mu+A.\nu$.
The largest continuous valuation is always a solution, but there is smaller
one. For every open subset $U$ of $\left\llbracket{\tau}\right\rrbracket$, the
possible values $x$ for $\nu(U)$ satisfy
$x=(s_{\mathrm{true}}\cdot\mu)(U)+A.x$: if $(s_{\mathrm{true}}\cdot\mu)(U)=0$,
then the least value for $x$ is $0$ (this is the only possible value if $A>1$;
if $A=1$, every element of $\overline{\mathbb{R}}_{+}$ is a possible value);
otherwise, the only possible value for $x$ is $+\infty$. This suggests that
the least solution $\nu$ to $\nu=\Phi(\nu)$ is defined by:

$\displaystyle\nu(U)$ $\displaystyle=\left\\{\begin{array}[]{ll}0&\text{if
}(s_{\mathrm{true}}\cdot\mu)(U)=0\\\
+\infty&\text{otherwise.}\end{array}\right.$

This is just the continuous valuation $(+\infty).(s_{\mathrm{true}}\cdot\mu)$.
It is a minimal valuation by Lemma 5.4. Hence the desired semantics
$\left\llbracket{\mathtt{rej}}\right\rrbracket\rho$ is
$(+\infty).(s_{\mathrm{true}}\cdot\mu)$ if
$(s_{\mathrm{false}}\cdot\mu)(\left\llbracket{\tau}\right\rrbracket)\geq 1$.

In the special case where $s$ is deterministic, namely that
$s_{\mathrm{true}}=\chi_{U}$ and $s_{\mathrm{false}}=\chi_{V}$ for two
disjoint open subsets $U$ and $V$ of $\left\llbracket{\tau}\right\rrbracket$,
then $s_{\mathrm{true}}\cdot\mu$ maps every open set $W$ to $\mu(U\cap W)$,
and is therefore equal to the restriction $\mu_{|U}$ of $\mu$ to $U$, as
introduced by Heckmann [Heckmann, 1996]. In that case,
$\left\llbracket{\mathtt{rej}}\right\rrbracket\rho$ is equal to
$\frac{1}{1-\mu(V)}\mu_{|U}$ if $\mu(V)<1$, and to $(+\infty).\mu_{|U}$
otherwise.

###  9.3 Using $\boldsymbol{\mathtt{score}}$

Using $\boldsymbol{\mathtt{score}}$ instead of recursion, we can implement
rejection sampling by the following ISPCF term:

$\displaystyle\mathtt{rej}^{\prime}$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}\lambda p_{D\tau}.\lambda
sel_{\tau\to D\boldsymbol{\mathtt{bool}}}.$
$\displaystyle\qquad\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x_{\tau}\leftarrow
p};$
$\displaystyle\qquad\mathop{\boldsymbol{\mathtt{do}}}\nolimits{b_{\boldsymbol{\mathtt{bool}}}\leftarrow
sel\;x};$
$\displaystyle\qquad\quad\boldsymbol{\mathtt{score}}(\boldsymbol{\mathtt{if}}\;b\;\underline{1.0}\;\underline{0.0});$
$\displaystyle\qquad\quad\mathop{\boldsymbol{\mathtt{ret}}}\nolimits\;x.$

Let $\mu\in\left\llbracket{D\tau}\right\rrbracket$,
$s\in\left\llbracket{\tau\to D\boldsymbol{\mathtt{bool}}}\right\rrbracket$. We
again assume that $s(x)$ as
$s_{\mathrm{true}}(x).\delta_{\mathrm{true}}+s_{\mathrm{false}}(x).\delta_{\mathrm{false}}$
for every $x\in\left\llbracket{\tau}\right\rrbracket$. Then, for every
$W\in{\mathcal{O}}{\left\llbracket{\tau}\right\rrbracket}$,

$\displaystyle\left\llbracket{\mathtt{rej}^{\prime}}\right\rrbracket\rho(\mu)(s)(W)$
$\displaystyle=\int_{x\in X}s_{\mathrm{true}}(x)\chi_{W}(x)d\mu,$

so that $\left\llbracket{\mathtt{rej}^{\prime}}\right\rrbracket\rho(\mu)(s)$
is simply $s_{\mathrm{true}}\cdot\mu$.

In other words,
$\left\llbracket{\mathtt{rej}^{\prime}}\right\rrbracket\rho(\mu)(s)$ computes
the valuation obtained from $\mu$ by applying the density function
$s_{\mathrm{true}}$. When $s_{\mathrm{true}}=\chi_{U}$, this is $\mu_{|U}$.
Hence we retrieve the same result as for
$\left\llbracket{\mathtt{rej}}\right\rrbracket\rho$, up to a renormalization
factor, which may be infinite.

It is practical to abbreviate the form
$\boldsymbol{\mathtt{score}}(\boldsymbol{\mathtt{if}}\;b\;\underline{1.0}\;\underline{0.0})$,
where $b\colon\boldsymbol{\mathtt{bool}}$, as $\mathtt{observe}\;b$. This is a
familiar operation, implemented in Anglican [Wood et al., 2014], as a derived
operator in Hakaru [Shan and Ramsey, 2017], or as the third argument of
$\mathtt{lex\text{-}query}$ clauses in Church [Goodman et al., 2008].

###  9.4 Generating normal distributions

Let us imagine that we do not have a term
$\boldsymbol{\mathtt{sample}}[\mathcal{N}(0,1)]$ for the normal (Gaussian)
distribution $\mathcal{N}(0,1)$ with mean $0$ and standard deviation $1$. We
will give several different possible implementations in ISPCF of well-known
algorithms.

For every measure map $f\colon\mathbb{R}\to\overline{\mathbb{R}}_{+}$,
$\mathcal{N}(0,1)$ is such that:

$\displaystyle\int_{x\in\mathbb{R}}f(x)d\mathcal{N}(0,1)$
$\displaystyle=\int_{x\in\mathbb{R}}f(x)\sqrt{\frac{1}{2\pi}}e^{-\frac{1}{2}x^{2}}dx.$

This is a measure defined from Lebesgue measure $\lambda$ on $\mathbb{R}$ by
applying the density map $x\mapsto\sqrt{\frac{1}{2\pi}}e^{-\frac{1}{2}x^{2}}$.
As such, we can implement it as follows, assuming a term
$\boldsymbol{\mathtt{sample}}[\lambda]$, as well as primitives for
multiplication, division, exponential $\underline{\text{exp}}$, square root
$\underline{\text{sqrt}}$, and various numerical constants, all with their
intended semantics. We agree that product is written with an infix $\times$,
and we remember that $M;N$ abbreviates
$\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x\leftarrow M};N$, where $x$ is a
fresh variable.

$\displaystyle\mathtt{normal}$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x_{\boldsymbol{\mathtt{real}}}\leftarrow\boldsymbol{\mathtt{sample}}[\lambda]};$
$\displaystyle\qquad\boldsymbol{\mathtt{score}}(\underline{\text{sqrt}}(\underline{0.5}/\underline{\pi})\times\underline{\text{exp}}(\underline{-0.5}\times
x\times x));\mathop{\boldsymbol{\mathtt{ret}}}\nolimits x.$

This is the original purpose of $\boldsymbol{\mathtt{score}}$: to define a
distribution from another one through a density function. We check that this
gives us the intended result. For every environment $\rho$, for every open
subset $W$ of $\mathbf{I}\mathbb{R}_{\bot}$,

$\displaystyle\left\llbracket{\mathtt{normal}}\right\rrbracket\rho(W)$
$\displaystyle=\int_{\mathbf{x}\in\mathbf{I}\mathbb{R}_{\bot}}|\overline{g}(\mathbf{x})|.\delta_{\mathbf{x}}(W)di[\lambda]$

where
$\overline{g}(\mathbf{x})\mathrel{\buildrel\text{def}\over{=}}\left\llbracket{\underline{\text{sqrt}}(\underline{0.5}/\underline{\pi})\times\underline{\text{exp}}(\underline{-0.5}\times
x\times x)}\right\rrbracket\rho[x\mapsto\mathbf{x}]$; we check that
$\overline{g}([x,x])=[g(x),g(x)]$ where
$g(x)\mathrel{\buildrel\text{def}\over{=}}\sqrt{\frac{1}{2\pi}}e^{-\frac{1}{2}x^{2}}$.
By the change-of-variables formula, and the fact that
$\delta_{[x,x]}(W)=\chi_{i^{-1}(W)}(x)$,

$\displaystyle\left\llbracket{\mathtt{normal}}\right\rrbracket\rho(W)$
$\displaystyle=\int_{x\in\mathbb{R}}g(x).\chi_{i^{-1}(W)}(x)d\lambda=\mathcal{N}(0,1)(i^{-1}(W)).$

Therefore
$\left\llbracket{\mathtt{normal}}\right\rrbracket\rho=i[\mathcal{N}(0,1)]$.

Another way of implementing $\mathcal{N}(0,1)$ is the _Box-Muller algorithm_
[Box and Muller, 1958], which produces pairs of two independent normally
distributed variables, from two independent uniformly distributed variables in
$[0,1]$.

In order to implement this in ISPCF, we assume a term
$\boldsymbol{\mathtt{sample}}[\lambda_{1}]$, where $\lambda_{1}$ is the
uniform measure on $[0,1]$. We also assume we have primitives
$\underline{\sin}$, $\underline{\cos}$, $\underline{\log}$, and
$\underline{\text{sqrt}}$, as well as addition, subtraction, opposite, and
multiplication, with the expected semantics. We consider the following ISPCF
term of type $D(\boldsymbol{\mathtt{real}}\times\boldsymbol{\mathtt{real}})$.
We use the shorthand
$\boldsymbol{\mathtt{let}}\;{x=u}\;\boldsymbol{\mathtt{in}}\;{v}$ for
$(\lambda x.v)u$.

$\displaystyle\mathtt{box\\_muller}$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x_{\boldsymbol{\mathtt{real}}}\leftarrow\boldsymbol{\mathtt{sample}}[\lambda_{1}]};$
$\displaystyle\qquad\mathop{\boldsymbol{\mathtt{do}}}\nolimits{y_{\boldsymbol{\mathtt{real}}}\leftarrow\boldsymbol{\mathtt{sample}}[\lambda_{1}]};$
$\displaystyle\qquad\boldsymbol{\mathtt{let}}\;{c_{\boldsymbol{\mathtt{real}}}=\underline{\cos}(\underline{2.0}\times\underline{\pi}\times
y)}\;\boldsymbol{\mathtt{in}}\;{}$
$\displaystyle\qquad\boldsymbol{\mathtt{let}}\;{s_{\boldsymbol{\mathtt{real}}}=\underline{\sin}(\underline{2.0}\times\underline{\pi}\times
y)}\;\boldsymbol{\mathtt{in}}\;{}$
$\displaystyle\qquad\boldsymbol{\mathtt{let}}\;{m_{\boldsymbol{\mathtt{real}}}=\underline{\text{sqrt}}(\underline{-2.0}\times\underline{\log}\;x)}\;\boldsymbol{\mathtt{in}}\;{}$
$\displaystyle\qquad\qquad\mathop{\boldsymbol{\mathtt{ret}}}\nolimits(\langle
m\times c,m\times s\rangle).$

This is a non-recursive definition, and as a consequence,
$\left\llbracket{\mathtt{box\\_muller}}\right\rrbracket\rho$ is a probability
distribution on $\mathbf{I}\mathbb{R}_{\bot}\times\mathbf{I}\mathbb{R}_{\bot}$
that is actually concentrated on the subspace $\mathbb{R}\times\mathbb{R}$.
Explicitly, for every open subset $W$ of
$\mathbf{I}\mathbb{R}_{\bot}\times\mathbf{I}\mathbb{R}_{\bot}$,

$\displaystyle\left\llbracket{\mathtt{box\\_muller}}\right\rrbracket\rho(W)$
$\displaystyle=\int_{\mathbf{x}\in\mathbf{I}\mathbb{R}_{\bot}}\left(\int_{\mathbf{y}\in\mathbf{I}\mathbb{R}_{\bot}}\delta_{f(\mathbf{x},\mathbf{y})}(W)di[\lambda_{1}]\right)di[\lambda_{1}],$

where $f(\mathbf{x},\mathbf{y})$ is
$\left\llbracket{\boldsymbol{\mathtt{let}}\;{c_{\boldsymbol{\mathtt{real}}}=\underline{\cos}(\underline{2.0}\times\underline{\pi}\times
y)}\;\boldsymbol{\mathtt{in}}\;{\cdots\boldsymbol{\mathtt{in}}\;\langle
m\times c,m\times
s\rangle}}\right\rrbracket\rho[x\mapsto\mathbf{x},y\mapsto\mathbf{y}]$. By the
change-of-variables formula, we have:

$\displaystyle\left\llbracket{\mathtt{box\\_muller}}\right\rrbracket\rho(W)$
$\displaystyle=\int_{x\in\mathbb{R}}\left(\int_{y\in\mathbb{R}}\delta_{f([x,x],[y,y])}(W)d\lambda_{1}\right)d\lambda_{1},$

and $f([x,x],[y,y])=[g(x,y),g(x,y)]$, where $g(x,y)=(\sqrt{-2\log x}\cos(2\pi
y),\allowbreak\sqrt{-2\log x}\sin(2\pi y))$. It follows that
$f([x,x],[y,y])\in W$ if and only if $g(x,y)\in i^{-1}(W)$, so that:

$\displaystyle\left\llbracket{\mathtt{box\\_muller}}\right\rrbracket\rho(W)$
$\displaystyle=\int_{x\in\mathbb{R}}\left(\int_{y\in\mathbb{R}}\chi_{i^{-1}(W)}(g(x,y))d\lambda_{1}\right)d\lambda_{1},$

We now use the familiar argument subtending the Box-Muller algorithm, which we
recapitulate for completeness. For every measurable map
$h\colon\mathbb{R}^{2}\to\overline{\mathbb{R}}_{+}$ (the integrals are
ordinary Lebesgue integrals),

$\displaystyle\int_{(s,t)\in\mathbb{R}^{2}}h(s,t)d\mathcal{N}(0,1)\otimes\mathcal{N}(0,1)$
$\displaystyle=\int_{(s,t)\in\mathbb{R}^{2}}\frac{1}{2\pi}h(s,t)e^{-\frac{1}{2}(s^{2}+t^{2})}ds\;dt$
$\displaystyle=\int_{r\in\mathbb{R}_{+},\theta\in[0,2\pi]}\frac{1}{2\pi}h(r\cos\theta,r\sin\theta)e^{-\frac{1}{2}r^{2}}r\;dr\;d\theta$
using the change of variables $s=r\cos\theta$, $t=r\sin\theta$
$\displaystyle=\int_{x,y\in[0,1]}h(\sqrt{-2\log x}\cos(2\pi y),\sqrt{-2\log
x}\sin(2\pi y))\;dx\;dy$ $\displaystyle\text{by letting
$x\mathrel{\buildrel\text{def}\over{=}}e^{-\frac{1}{2}r^{2}}$,
$y\mathrel{\buildrel\text{def}\over{=}}\theta/(2\pi)$}.$

By taking $h\mathrel{\buildrel\text{def}\over{=}}\chi_{i^{-1}(W)}$, it follows
that
$(\mathcal{N}(0,1)\otimes\mathcal{N}(0,1))(i^{-1}(W))=\left\llbracket{\mathtt{box\\_muller}}\right\rrbracket\rho(W)$.
Therefore $\mathtt{box\\_muller}$ implements the product
$\mathcal{N}(0,1)\otimes\mathcal{N}(0,1)$, in the sense that:

$\displaystyle\left\llbracket{\mathtt{box\\_muller}}\right\rrbracket\rho$
$\displaystyle=i[\mathcal{N}(0,1)\otimes\mathcal{N}(0,1)].$

######  Remark 9.1.

The valuation $\lambda_{1}$ has compact support $[0,1]$. Since only continuous
maps can be defined in ISPCF, it might seem intuitive that any continuous
valuation defined by ISPCF terms that only use
$\boldsymbol{\mathtt{sample}}[\lambda_{1}]$ as sampler should also have
compact support, enforcing a necessary limitation on the kind of distributions
that one can define. The example of the term $\mathtt{box\\_muller}$ shows
that this is not the case. We will see another example in Section 9.5.

A more efficient variant of this algorithm combines it with rejection
sampling, and is due to Marsaglia and Bray [Marsaglia and Bray, 1964]:

$\displaystyle\mathtt{box\\_muller^{\prime}}$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}\mathop{\boldsymbol{\mathtt{do}}}\nolimits{\langle
x_{\boldsymbol{\mathtt{real}}},y_{\boldsymbol{\mathtt{real}}}\rangle\leftarrow\mathtt{rej}\;(\mathtt{prod}_{\boldsymbol{\mathtt{real}},\boldsymbol{\mathtt{real}}}\;\mathtt{L}\;\mathtt{L})\;\mathtt{discp}};$
$\displaystyle\qquad\boldsymbol{\mathtt{let}}\;{u_{\boldsymbol{\mathtt{real}}}=x\times
x+y\times y}\;\boldsymbol{\mathtt{in}}\;{}$
$\displaystyle\qquad\boldsymbol{\mathtt{let}}\;{m_{\boldsymbol{\mathtt{real}}}=\underline{\text{sqrt}}(\underline{-2.0}\times\underline{\log}\;u/u)}\;\boldsymbol{\mathtt{in}}\;{}$
$\displaystyle\qquad\quad\mathop{\boldsymbol{\mathtt{ret}}}\nolimits\langle
m\times x,m\times y\rangle,$

where $\mathtt{prod}_{\sigma,\tau}$ implements the product of two minimal
valuations on $\left\llbracket{\sigma}\right\rrbracket$ and
$\left\llbracket{\tau}\right\rrbracket$, $\mathtt{L}$ implements the uniform
measure on $[-1,1]$ (namely, half of the restriction of Lebesgue measure to
$[-1,1]$), and $\mathtt{discp}$ tests whether a point lies on the unit disc:

$\displaystyle\mathtt{prod}_{\sigma,\tau}$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}\lambda p_{D\sigma}.\lambda
q_{D\tau}.$
$\displaystyle\qquad\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x_{\sigma}\leftarrow
p};\mathop{\boldsymbol{\mathtt{do}}}\nolimits{y_{\tau}\leftarrow
q};\mathop{\boldsymbol{\mathtt{ret}}}\nolimits\langle x,y\rangle$
$\displaystyle\mathtt{L}$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x_{\boldsymbol{\mathtt{real}}}\leftarrow\boldsymbol{\mathtt{sample}}[\lambda_{1}]};\mathop{\boldsymbol{\mathtt{ret}}}\nolimits(\underline{2.0}\times
x-\underline{1.0})$ $\displaystyle\mathtt{discp}$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}\lambda\langle
x_{\boldsymbol{\mathtt{real}}},y_{\boldsymbol{\mathtt{real}}}\rangle.\mathop{\boldsymbol{\mathtt{ret}}}\nolimits(\underline{\text{pos}}(\underline{1.0}-x\times
x-y\times y).$

We also use the convenient abbreviation $\lambda\langle
x_{\sigma},y_{\tau}\rangle.M$ for $\lambda
p_{\sigma\times\tau}.\boldsymbol{\mathtt{let}}\;{x_{\sigma}=\pi_{1}p}\;\boldsymbol{\mathtt{in}}\;{}\allowbreak\boldsymbol{\mathtt{let}}\;{y_{\tau}=\pi_{2}p}\;\boldsymbol{\mathtt{in}}\;{M}$,
where $p$ is not free in $M$, and similarly for
$\mathop{\boldsymbol{\mathtt{do}}}\nolimits{\langle
x_{\sigma},y_{\tau}\rangle\leftarrow M};N$.

######  Remark 9.2.

We could have defined $\mathtt{prod}_{\sigma,\tau}$ as $\lambda
p_{D\sigma}.\lambda
q_{D\tau}.\mathop{\boldsymbol{\mathtt{do}}}\nolimits{y_{\tau}\leftarrow
q};\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x_{\sigma}\leftarrow
p};\mathop{\boldsymbol{\mathtt{ret}}}\nolimits\langle x,y\rangle$ instead.
Since the monad of minimal valuations is commutative, this would not make any
semantical difference.

We let the reader check that
$\left\llbracket{\mathtt{box\\_muller^{\prime}}}\right\rrbracket\rho$ is also
equal to $i[\mathcal{N}(0,1),\mathcal{N}(0,1)]$. We only give a sketch of an
argument. The semantics of
$\mathtt{rej}\;(\mathtt{prod}_{\boldsymbol{\mathtt{real}},\boldsymbol{\mathtt{real}}}\;\mathtt{L}\;\mathtt{L})\;\mathtt{discp}$
is $\frac{1}{1-i[\mu](\mathcal{V})}i[\mu]_{|\mathcal{U}}$, where:

  * •

$\mu$ is the uniform measure on the square $[-1,1]\times[-1,1]$;

  * •

$\mathcal{U}$ is the Scott-open set of pairs
$([a,b],[c,d])\in\mathbf{I}\mathbb{R}^{2}$ such that
$[x,y]\mathrel{\buildrel\text{def}\over{=}}[a,b]\times[a,b]+[c,d]\times[c,d]$
satisfies $y<1$; in particular,
$U\mathrel{\buildrel\text{def}\over{=}}i^{-1}(\mathcal{U})$ is the open unit
disc $\\{(x,y)\in\mathbb{R}^{2}\mid x^{2}+y^{2}<1\\}$;

  * •

$\mathcal{V}$ is a similar Scott-open set, with the property that
$V\mathrel{\buildrel\text{def}\over{=}}i^{-1}(\mathcal{V})$ is the complement
of the closed unit disc, namely $V=\\{(x,y)\in\mathbb{R}^{2}\mid
x^{2}+y^{2}>1\\}$.

Then $i[\mu](\mathcal{V})=\mu(V)=1-\pi/4=1-\mu(U)$, so that the semantics of
$\mathtt{rej}\;(\mathtt{prod}_{\boldsymbol{\mathtt{real}},\boldsymbol{\mathtt{real}}}\;\mathtt{L}\;\mathtt{L})\;\mathtt{discp}$
is $i[\mu^{\prime}]$, where $\mu^{\prime}$ is the uniform measure on the
(open) unit disc. The rest of the argument follows similar lines as with the
original Box-Muller algorithm.

Here is a fourth and final implementation of $\mathcal{N}(0,1)$. Let
$\mathtt{box\\_muller^{\prime}}^{\prime}$ be obtained from
$\mathtt{box\\_muller^{\prime}}$ by replacing $\mathtt{rej}$ by
$\mathtt{rej}^{\prime}$. The semantics of
$\mathtt{rej}^{\prime}\;(\mathtt{prod}_{\boldsymbol{\mathtt{real}},\boldsymbol{\mathtt{real}}}\;\mathtt{L}\;\mathtt{L})\;\mathtt{discp}$
is equal to $1-i[\mu](\mathcal{V})=\pi/4$ times the semantics of
$\mathtt{rej}\;(\mathtt{prod}_{\boldsymbol{\mathtt{real}},\boldsymbol{\mathtt{real}}}\;\mathtt{L}\;\mathtt{L})\;\mathtt{discp}$.
It follows that
$\left\llbracket{\mathtt{box\\_muller^{\prime}}^{\prime}}\right\rrbracket\rho=\frac{\pi}{4}\;i[\mathcal{N}(0,1),\mathcal{N}(0,1)]=i\left[\frac{\pi}{4}\mathcal{N}(0,1),\frac{\pi}{4}\mathcal{N}(0,1)\right]$.
This yields the same result as before, up to a renormalization factor.

###  9.5 Generating Lebesgue measure on $\mathbb{R}$

We have noticed that one can define measures with unbounded support from just
$\boldsymbol{\mathtt{sample}}[\lambda_{1}]$, although $\lambda_{1}$ has
bounded support (see Remark 9.1). We now show that we can define measures with
unbounded support and whose total mass is infinite as well. This requires the
use of $\boldsymbol{\mathtt{score}}$. What may be intriguing is that
$\boldsymbol{\mathtt{score}}$ multiplies the current ‘probability’ by a real
number different from $+\infty$. Still, this can be used to increase the total
mass from $1$ to $+\infty$.

Hence, we imagine that the term $\boldsymbol{\mathtt{sample}}[\lambda_{1}]$ is
available, where $\lambda_{1}$ is Lebesgue measure on $[0,1]$, but that
$\boldsymbol{\mathtt{sample}}[\lambda]$ is not, where $\lambda$ is Lebesgue
measure on $\mathbb{R}$. Assuming constants $\underline{\pi}$,
$\underline{1.0}$, $\underline{2.0}$, $\underline{\tan}$,
$\underline{\arctan}$, and some constants for addition, subtraction,
multiplication and division, we define:

$\displaystyle\mathtt{uniform}$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}\lambda
a_{\boldsymbol{\mathtt{real}}}.\lambda
b_{\boldsymbol{\mathtt{real}}}.\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x_{\boldsymbol{\mathtt{real}}}\leftarrow\boldsymbol{\mathtt{sample}}[\lambda_{1}]};\mathop{\boldsymbol{\mathtt{ret}}}\nolimits{(a+(b-a)\times
x)}$ $\displaystyle\mathtt{lebesgue}$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}\mathop{\boldsymbol{\mathtt{do}}}\nolimits{z_{\boldsymbol{\mathtt{real}}}\leftarrow\mathtt{uniform}(-\underline{\pi}/\underline{2.0})(\underline{\pi}/\underline{2.0})};$
$\displaystyle\qquad\boldsymbol{\mathtt{score}}(\underline{1.0}/(\underline{1.0}+z\times
z));$
$\displaystyle\qquad\mathop{\boldsymbol{\mathtt{ret}}}\nolimits(\underline{\arctan}\;z).$

We claim that $\mathtt{lebesgue}$ fits the bill. Let $\upsilon_{[a,b]}$ denote
the uniform probability measure on the interval $[a,b]$; up to the embedding
$i\colon\mathbb{R}\to\mathbf{I}\mathbb{R}_{\bot}$, this is what
$\mathtt{uniform}$ applied to $a$ and $b$ computes. Then we use a monotonic,
differentiable homeomorphism $g$ from $\mathbb{R}$ to the open interval
$]a,b[$ in order to transport that to the whole of $\mathbb{R}$. (One may
observe that $]a,b[$ differs from $[a,b]$, but that will not matter, since the
complement of $]a,b[$ in $[a,b]$ has $\upsilon_{[a,b]}$-measure $0$.) We have
chosen $g(u)\mathrel{\buildrel\text{def}\over{=}}\arctan u$, $a=-\pi/2$,
$b=\pi/2$ here.

Let us check our claim formally; this is a paper on semantics, and we need to
check that our semantics produces the intended result. First, for every
environment $\rho$, for all $a,b\in\mathbb{R}$ such that $a<b$,
$\left\llbracket{\mathtt{uniform}}\right\rrbracket\rho(a)(b)$ is the minimal
valuation $(\lambda x.\delta_{a+(b-a)x)})^{\dagger}(i[\lambda_{1}])$. For
every open subset $U$ of $\mathbf{I}\mathbb{R}_{\bot}$, therefore,

$\displaystyle\left\llbracket{\mathtt{uniform}}\right\rrbracket\rho(a)(b)(U)$
$\displaystyle=\int_{\mathbf{u}\in\mathbf{I}\mathbb{R}_{\bot}}\delta_{i(a)+(i(b)-i(a))\times\mathbf{u})}(U)di[\lambda_{1}]$
$\displaystyle=\int_{u\in\mathbb{R}}\delta_{(i(a)+(i(b)-i(a))\times
i(u))}(U)d\lambda_{1}$ by the change-of-variables formula
$\displaystyle=\int_{u\in\mathbb{R}}\delta_{i(a+(b-a)u)}(U)d\lambda_{1}$
$\displaystyle=\int_{0}^{1}\chi_{i^{-1}(U)}(a+(b-a)u)du$
$\displaystyle\text{using the identity }\delta_{c}(U)=\chi_{U}(c)$
$\displaystyle=\frac{1}{b-a}\int_{a}^{b}\chi_{i^{-1}(U)}(v)dv$
$\displaystyle\text{by letting
}v\mathrel{\buildrel\text{def}\over{=}}a+(b-a)u$
$\displaystyle=\upsilon_{[a,b]}(i^{-1}(U)).$

Therefore
$\left\llbracket{\mathtt{uniform}}\right\rrbracket\rho(a)(b)=i[\upsilon_{[a,b]}]$.

Next, we evaluate $\left\llbracket{\mathtt{lebesgue}}\right\rrbracket\rho(U)$
for every open subset $U$ of $\mathbf{I}\mathbb{R}_{\bot}$ as follows. Let us
abbreviate the term
$\boldsymbol{\mathtt{score}}(\underline{1.0}/(\underline{1.0}+z\times
z));\mathop{\boldsymbol{\mathtt{ret}}}\nolimits(\underline{\arctan}\;z)$ as
$M(z)$. For every $u\in\mathbb{R}$, for every open subset $U$ of
$\mathbf{I}\mathbb{R}_{\bot}$, letting
$\nu_{u}\mathrel{\buildrel\text{def}\over{=}}\left\llbracket{M(z)}\right\rrbracket\rho[z\mapsto
i(u)]$, we have the following, where
$g(u)\mathrel{\buildrel\text{def}\over{=}}\arctan u$, and therefore
$g^{\prime}(u)=1/(1+u^{2})$:

$\displaystyle\nu_{u}(U)$
$\displaystyle=(\lambda\\_.\delta_{g(u)})^{\dagger}(g^{\prime}(u)\delta_{*})(U)$
$\displaystyle=\int_{\\_\in\left\llbracket{\boldsymbol{\mathtt{unit}}}\right\rrbracket}\delta_{g(u)}(U)dg^{\prime}(u)\delta_{*}$
$\displaystyle=g^{\prime}(u)\chi_{i^{-1}(U)}(g(u)).$

Therefore,

$\displaystyle\left\llbracket{\mathtt{lebesgue}}\right\rrbracket\rho(U)$
$\displaystyle=\int_{\mathbf{u}\in\mathbf{I}\mathbb{R}_{\bot}}\left\llbracket{M(z)}\right\rrbracket\rho[z\mapsto\mathbf{u}](U)di[\upsilon_{[-\pi/2,\pi/2]}]$
$\displaystyle=\int_{u\in\mathbb{R}}\left\llbracket{M(z)}\right\rrbracket\rho[z\mapsto
i(u)](U)d\upsilon_{[-\pi/2,\pi/2]}$ by the change-of-variables formula
$\displaystyle=\int_{u\in\mathbb{R}}\nu_{u}(U)d\upsilon_{[-\pi/2,\pi/2]}$
$\displaystyle=\int_{u\in\mathbb{R}}g^{\prime}(u)\chi_{i^{-1}(U)}(g(u))d\upsilon_{[-\pi/2,\pi/2]}$
$\displaystyle=\int_{-\pi/2}^{\pi/2}g^{\prime}(u)\chi_{i^{-1}(U)}(g(u))du$
$\displaystyle=\int_{-\infty}^{+\infty}\chi_{i^{-1}(U)}(t)dt$
$\displaystyle\text{by letting }t\mathrel{\buildrel\text{def}\over{=}}g(u)$
$\displaystyle=\lambda(i^{-1}(U)).$

Therefore, as promised,
$\left\llbracket{\mathtt{lebesgue}}\right\rrbracket\rho$ is the image measure
$i[\lambda]$ of Lebesgue measure $\lambda$ on $\mathbb{R}$.

###  9.6 Generating exponential distributions

Generating an exponential distribution is another classical example. The
novelty is that this is defined from Lebesgue measure $\lambda$ by a density
function that is _not_ continuous. Although ISPCF can only express continuous
functions, we show that this will not prevent us from defining the exponential
distribution.

For simplicity, we consider the exponential distribution with parameter $1$.
The density map is:

$\displaystyle g(x)$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}\left\\{\begin{array}[]{ll}e^{-x}&\text{if
}x\geq 0\\\ 0&\text{otherwise}\end{array}\right.$

We note that $g$ is not continuous at $0$. However, we have the following
candidate ISPCF term, assuming the relevant primitives:

$\displaystyle\mathtt{exp\\_density}$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}\lambda
x_{\boldsymbol{\mathtt{real}}}.\boldsymbol{\mathtt{if}}\;{(\underline{\text{pos}}\;x)}\;(\underline{\exp}(-x))\;\underline{0.0}.$

For every environment $\rho$, we see that
$\overline{g}\mathrel{\buildrel\text{def}\over{=}}\left\llbracket{\mathtt{exp\\_density}}\right\rrbracket$
maps $\bot$ to $\bot$, and every interval $[a,b]$ to $[e^{-b},e^{-a}]$ if
$a>0$, to $[0,0]$ if $b<0$, and to $\bot$ otherwise. In particular,
$\left\llbracket{\mathtt{exp\\_density}}\right\rrbracket(i(a))$ coincides with
$i(g(a))$ for all points of continuity of $g$, namely for every $a\neq 0$.

The most obvious way to implement the exponential distribution is by using
$\boldsymbol{\mathtt{score}}$. We assume a term
$\boldsymbol{\mathtt{sample}}[\lambda]$, where $\lambda$ is Lebesgue measure
on $\mathbb{R}$.

$\displaystyle\mathtt{expo}$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x_{\boldsymbol{\mathtt{real}}}\leftarrow\boldsymbol{\mathtt{sample}}[\lambda]};\boldsymbol{\mathtt{score}}(\mathtt{exp\\_density}\;x);\mathop{\boldsymbol{\mathtt{ret}}}\nolimits
x.$

For every open subset $W$ of $\mathbf{I}\mathbb{R}_{\bot}$, we compute:

$\displaystyle\left\llbracket{\mathtt{expo}}\right\rrbracket\rho(W)$
$\displaystyle=\int_{\mathbf{x}\in\mathbf{I}\mathbb{R}_{\bot}}|\overline{g}(\mathbf{x})|.\delta_{\mathbf{x}}(W)di[\lambda]$
$\displaystyle=\int_{x\in\mathbb{R}}|\overline{g}(i(x))|.\delta_{i(x)}(W)d\lambda$
by the change-of-variables formula
$\displaystyle=\int_{x\in\mathbb{R}}g(x).\chi_{i^{-1}(W)}(x)d\lambda.$

The last line is justified by the fact that
$\delta_{i(x)}(W)=\chi_{i^{-1}(W)}(x)$, and more importantly, by the fact that
$|\overline{g}(i(x))|$ and $g(x)$ coincide for every $x\in\mathbb{R}$ except
on a set of Lebesgue measure $0$. (Namely, when $x=0$, in which case $g(x)=1$
and $|\overline{g}(i(x))|=0$.)

It follows that $\left\llbracket{\mathtt{expo}}\right\rrbracket\rho$ is
exactly $i[g\cdot\lambda]$, the image by $i$ of the exponential distribution
$g\cdot\lambda$.

Another way of implementing the exponential distribution is as:

$\displaystyle\mathtt{expo}^{\prime}$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x_{\boldsymbol{\mathtt{real}}}\leftarrow\boldsymbol{\mathtt{sample}}[\lambda_{1}]};\mathop{\boldsymbol{\mathtt{ret}}}\nolimits(-\underline{\log}\;x),$

assuming a term $\boldsymbol{\mathtt{sample}}[\lambda_{1}]$ for sampling along
the Lebesgue measure $\lambda_{1}$ on $[0,1]$. We check that this also gives
the correct result. For every open subset $W$ of
$\mathbf{I}\mathbb{R}_{\bot}$,

$\displaystyle\left\llbracket{\mathtt{expo}^{\prime}}\right\rrbracket\rho(W)$
$\displaystyle=\int_{\mathbf{x}\in\mathbf{I}\mathbb{R}_{\bot}}\delta_{-\left\llbracket{\underline{\log}}\right\rrbracket\rho(\mathbf{x})}(W)di[\lambda_{1}]$
$\displaystyle=\int_{0}^{1}\chi_{W}(-\log x)dx,$

by the change-of-variables formula, the fact that integrating along
$\lambda_{1}$ means integrating on $[0,1]$, and the equality
$\delta_{a}(W)=\chi_{W}(a)$. We now let
$x\mathrel{\buildrel\text{def}\over{=}}e^{-t}$. The latter integral is then
equal to $\int_{0}^{+\infty}\chi_{W}(t)e^{-t}dt=(g\cdot\lambda)(W)$. Therefore
$\left\llbracket{\mathtt{expo}^{\prime}}\right\rrbracket\rho=\left\llbracket{\mathtt{expo}}\right\rrbracket\rho=i[g\cdot\lambda]$.

A final implementation of the exponential distribution, due to von Neumann,
consists in simulating a distribution with density
$(1-x)+(\frac{x^{2}}{2!}-\frac{x^{3}}{3!})+\cdots+(\frac{x^{2n}}{(2n)!}-\frac{x^{2n+1}}{(2n+1)!})+\cdots=e^{-x}$.
We will leave the verification that the term $\mathtt{von\\_neumann}$ below
again has the same semantics $i[g\cdot\lambda]$ as $\mathtt{expo}$ and
$\mathtt{expo}^{\prime}$, as an exercise. We first define:

$\displaystyle\mathtt{longest\\_decreasing\\_run}$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}\boldsymbol{\mathtt{rec}}(\lambda
f_{\boldsymbol{\mathtt{real}}\to\boldsymbol{\mathtt{int}}\to
D\boldsymbol{\mathtt{int}}}.\lambda x_{\boldsymbol{\mathtt{real}}}.\lambda
n_{\boldsymbol{\mathtt{int}}}.$
$\displaystyle\qquad\qquad\mathop{\boldsymbol{\mathtt{do}}}\nolimits{u\leftarrow\boldsymbol{\mathtt{sample}}[\lambda_{1}]};$
$\displaystyle\qquad\qquad\boldsymbol{\mathtt{if}}\;{(\underline{\text{pos}}(u-x))}\;$
$\displaystyle\qquad\qquad\qquad\mathop{\boldsymbol{\mathtt{ret}}}\nolimits n$
$\displaystyle\qquad\qquad\qquad(f\;u\;(n+\underline{1})))$

Given any $x\in[0,1]$,
$\left\llbracket{\mathtt{longest\\_decreasing\\_run}}\right\rrbracket\rho(x)(0)$
returns the largest $n$ such that $x>u_{1}>u_{2}>\cdots>u_{n}$ ($\leq
u_{n+1}$) for randomly uniformly distributed real numbers $u_{1}$, $u_{2}$, …,
in $[0,1]$. It is a standard exercice to show that
$\left\llbracket{\mathtt{longest\\_decreasing\\_run}}\right\rrbracket\rho(x)(0)$
is the distribution on $\mathbb{Z}_{\bot}$ 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}}(\frac{x^{n}}{n!}-\frac{x^{n+1}}{(n+1)!})=e^{-x}$.
Assuming a term
$\underline{\text{odd}}\colon\boldsymbol{\mathtt{int}}\to\boldsymbol{\mathtt{bool}}$
testing whether its argument is odd, one then defines:

$\displaystyle\mathtt{von\\_neumann}$
$\displaystyle\mathrel{\buildrel\text{def}\over{=}}\mathop{\boldsymbol{\mathtt{do}}}\nolimits{x_{\boldsymbol{\mathtt{real}}}\leftarrow\boldsymbol{\mathtt{sample}}[\lambda_{1}]};$
$\displaystyle\qquad\boldsymbol{\mathtt{rec}}(\lambda
f_{\boldsymbol{\mathtt{real}}\to
D\boldsymbol{\mathtt{real}}}.\lambda\ell_{\boldsymbol{\mathtt{real}}}.$
$\displaystyle\qquad\qquad\boldsymbol{\mathtt{if}}\;(\underline{\text{odd}}(\mathtt{longest\\_decreasing\\_run}\;x\;0))$
$\displaystyle\qquad\qquad\qquad f\;(\ell+\underline{1.0})$
$\displaystyle\qquad\qquad\qquad\mathop{\boldsymbol{\mathtt{ret}}}\nolimits\ell)x$

The $\boldsymbol{\mathtt{rec}}$ expression in the middle maps every real