LONG SHORT

# A Lambda-Calculus Foundation for
Universal Probabilistic Programming††thanks: The first author is supported by
the Swedish Research Council grant 2013-4853. The second author is partially
supported by the ANR project 12IS02001 PACE and the ANR project 14CE250005
ELICA. The fourth author was supported by Microsoft Research through its PhD
Scholarship Programme.

Johannes Borgström111Uppsala University Ugo Dal Lago222University of Bologna &
INRIA Andrew D. Gordon333Microsoft Research and University of Edinburgh Marcin
Szymczak444University of Edinburgh

###### Abstract

We develop the operational semantics of an untyped probabilistic
$\lambda$-calculus with continuous distributions, and both hard and soft
constraints, as a foundation for universal probabilistic programming languages
such as Church, Anglican, and Venture. Our first contribution is to adapt the
classic operational semantics of $\lambda$-calculus to a continuous setting
via creating a measure space on terms and defining step-indexed
approximations. We prove equivalence of big-step and small-step formulations
of this _distribution-based semantics_. To move closer to inference
techniques, we also define the _sampling-based semantics_ of a term as a
function from a trace of random samples to a value. We show that the
distribution induced by integration over the space of traces equals the
distribution-based semantics. Our second contribution is to formalize the
implementation technique of trace _Markov chain Monte Carlo_ (MCMC) for our
calculus and to show its correctness. A key step is defining sufficient
conditions for the distribution induced by trace MCMC to converge to the
distribution-based semantics. To the best of our knowledge, this is the first
rigorous correctness proof for trace MCMC for a higher-order functional
language, or for a language with soft constraints.

###### Contents

  1. 1 Introduction
    1. 1.1 Universal Probabilistic Programming in Church
    2. 1.2 Problem 1: Semantics of Church Queries
    3. 1.3 Problem 2: Correctness of Trace MCMC
    4. 1.4 Contributions of the Paper
    5. 1.5 Structure of the Paper
  2. 2 A Foundational Calculus for Church
    1. 2.1 Syntax of the Calculus
    2. 2.2 Big-step Sampling-based Semantics
    3. 2.3 Encoding Church
    4. 2.4 Example: Geometric Distribution
    5. 2.5 Soft Constraints and score
    6. 2.6 Example: Linear Regression
  3. 3 Sampling-Based Operational Semantics
    1. 3.1 Small-step Sampling-based Semantics
    2. 3.2 Some Measure-Theoretic Preliminaries.
    3. 3.3 Measure Space of Program Traces
    4. 3.4 Distributions $\langle\\!\langle M\rangle\\!\rangle$ and $\llbracket M\rrbracket_{\mathbb{S}}$ Given by Sampling-Based Semantics
  4. 4 Distribution-Based Operational Semantics
    1. 4.1 Sub-Probability Kernels
    2. 4.2 Approximation Small-Step Semantics
    3. 4.3 Approximation Big-Step Semantics
    4. 4.4 Beyond Approximations
    5. 4.5 Geometric Distribution, Revisited
    6. 4.6 Distribution-based and Sampling-based Semantics are Equivalent
    7. 4.7 An Application of the Distribution-Based Semantics
    8. 4.8 Rejection Sampling
    9. 4.9 Motivation for 1-Bounded Scores
  5. 5 Inference
    1. 5.1 A Metropolis-Hastings Sampling Algorithm
    2. 5.2 Proposal Density
    3. 5.3 A Metropolis-Hastings Proposal Kernel
    4. 5.4 Transition Kernel of the Markov Chain
    5. 5.5 Correctness of Inference
    6. 5.6 Examples
  6. 6 Related Work
  7. 7 Conclusions and Remarks
  8. A Proofs of Measurability
    1. A.1 Deterministic reduction as a measurable function
    2. A.2 Small- step reduction as a measurable function
    3. A.3 Measurability of $\mathbf{P}$ and $\mathbf{O}$
    4. A.4 Measurability of $\mathtt{peval}$
    5. A.5 Measurability of $q$ and $Q$

##  1 Introduction

In computer science, probability theory can be used for models that enable
system abstraction, and also as a way to compute in a setting where having
access to a source of randomness is essential to achieve correctness, as in
randomised computation or cryptography [11]. Domains in which probabilistic
models play a key role include robotics [37], linguistics [24], and especially
machine learning [31]. The wealth of applications has stimulated the
development of concrete and abstract programming languages, that most often
are extensions of their deterministic ancestors. Among the many ways
probabilistic choice can be captured in programming, a simple one consists in
endowing the language of programs with an operator modelling the sampling from
(one or many) distributions. This renders program evaluation a probabilistic
process, and under mild assumptions the language becomes universal for
probabilistic computation. Particularly fruitful in this sense has been the
line of work in the functional paradigm.

In _probabilistic programming_ , programs become a way to specify
probabilistic models for observed data, on top of which one can later do
inference. This has been a source of inspiration for AI researchers, and has
recently been gathering interest in the programming language community (see
Goodman [12], Gordon et al. [16], and Russell [33]).

###  1.1 Universal Probabilistic Programming in Church

Church [15] introduced _universal probabilistic programming_ , the idea of
writing probabilistic models for machine learning in a Turing-complete
functional programming language. Church, and its descendants Venture [25],
Anglican [39], and Web Church [14] are dialects of Scheme. Another example of
universal probabilistic programming is WebPPL [13], a probabilistic
interpretation of JavaScript.

A probabilistic query in Church has the form:

⬇

(query (define $x_{1}$ $e_{1}$)...(define $x_{n}$ $e_{n}$) $e_{q}$ $e_{c}$)

The query denotes the distribution given by the probabilistic expression
$e_{q}$, given variables $x_{i}$ defined by potentially probabilistic
expressions $e_{i}$, constrained so that the boolean predicate $e_{c}$ is
true.

Consider a coin with bias $p$, that is, $p$ is the probability of heads.
Recall that the _geometric distribution_ of the coin is the distribution over
the number of flips in a row before it comes up heads. An example of a Church
query is as follows: it denotes the geometric distribution for a fair coin,
constrained to be greater than one.

⬇

(query

(define flip (lambda (p) (< (rnd) p)))

(define geometric (lambda (p)

(if (flip p) 0 (+ 1 (geometric p))))

(define n (geometric .5))

n

(> n 1))

The query defines three variables: (1) flip is a function that flips a coin
with bias p, by calling (rnd) to sample a probability from the uniform
distribution on the unit interval; (2) geometric555See
http://forestdb.org/models/geometric.html. is a function that samples from the
geometric distribution of a coin with bias p; and (3) n denotes the geometric
distribution with bias 0.5. Here are samples from this query:

⬇

(5 5 5 4 2 2 2 2 2 3 3 2 2 7 2 2 3 4 2 3)

This example is a discrete distribution with unbounded support (any integer
greater than one may be sampled with some non-zero probability), defined in
terms of a continuous distribution (the uniform distribution on the unit
interval). Queries may also define continuous distributions, such as
regression parameters.

###  1.2 Problem 1: Semantics of Church Queries

The first problem we address in this work is to provide a formal semantics for
universal probabilistic programming languages with constraints. Our example
illustrates the common situation in machine learning that models are based on
continuous distributions (such as (rnd)) and use constraints, but previous
works on formal semantics for untyped probabilistic $\lambda$-calculi do not
rigorously treat the combination of these features.

To address the problem we introduce a call-by-value $\lambda$-calculus with
primitives for random draws from various continuous distributions, and
primitives for both hard and soft constraints. We present an encoding of
Church into our calculus, and some nontrivial examples of probabilistic
models.

We consider two styles of operational semantics for our $\lambda$-calculus, in
which a term is interpreted in two ways, the first closer to inference
techniques, the second more extensional:

Sampling-Based:

A function from a trace to a value and weight.

Distribution-Based:

A distribution over terms of our calculus.

To obtain a thorough understanding of the semantics of the calculus, for each
of these styles we present two inductive definitions of operational semantics,
in small-step and big-step style.

First, we consider the _sampling-based semantics_ : the two inductive
definitions have the forms shown below, where $M$ is a closed term, $s$ is a
finite _trace_ of random real numbers, $w>0$ is a _weight_ (to impose soft
constraints), and $G$ is a _generalized value_ (either a value (constant or
$\lambda$-abstraction) or the exception fail, used to model a failing hard
constraint).

  * •

Figure 6 defines small-step relation
$(M,w,s)\rightarrow(M^{\prime},w^{\prime},s^{\prime})$.

  * •

Figure 2 defines the big-step relation $M\Downarrow^{s}_{w}G$.

For example, if $M$ is the $\lambda$-term for our geometric distribution
example and we have $M\Downarrow^{s}_{w}G$ then there is $n\geq 0$ such that:

  * •

the trace has the form $s=[q_{1},\dots,q_{n+1}]$ where each $q_{i}$ is a
probability, and $q_{i}<0.5$ if and only if $i=n+1$. (A sample $q_{i}\geq 0.5$
is tails; a sample $q_{i}<0.5$ is heads.)

  * •

the result takes the form $G=n$ if $n>1$, and otherwise $G=\mathtt{fail}$ (the
failure of a hard constraint leads to $\mathtt{fail}$);

  * •

and the weight is $w=1$ (the density of the uniform distribution on the unit
interval).

Our first result, Theorem 1, shows equivalence: that the big-step and small-
semantics of a term consume the same traces to produce the same results with
the same weights.

To interpret these semantics probabilistically, we describe a metric space of
$\lambda$-terms and let $\mathscr{D}$ range over _distributions_ , that is,
sub-probability Borel measures on terms of the $\lambda$-calculus. We define
$\llbracket M\rrbracket_{\mathbb{S}}$ to be the distribution induced by the
sampling-based semantics of $M$, by integrating the weight over the space of
traces.

Second, we consider the _distribution-based semantics_ , that directly
associate distributions with terms, without needing to integrate out traces.
The two inductive definitions have the forms shown below, where $n$ is a step-
index:

  * •

Figure 9 defines a family of small-step relations
$M\Rightarrow_{n}\mathscr{D}$.

  * •

Figure 11 defines a family of big-step relations $M\Downarrow_{n}\mathscr{D}$.

These step-indexed families are approximations to their suprema, distributions
written as $\llbracket M\rrbracket_{\Rightarrow}$ and $\llbracket
M\rrbracket_{\Downarrow}$. By Theorem 2 we have $\llbracket
M\rrbracket_{\Rightarrow}=\llbracket M\rrbracket_{\Downarrow}$. The proof of
the theorem needs certain properties (Lemmas 30, 34, and 36) that build on
compositionality results for sub-probability kernels [28] from the measure
theory literature. We apply the distribution-based semantics in Section 4.7 to
show an equation between hard and soft constraints.

Finally, we reconcile the two rather different styles of semantics: Theorem 3
establishes that $\llbracket M\rrbracket_{\mathbb{S}}=\llbracket
M\rrbracket_{\Rightarrow}$.

###  1.3 Problem 2: Correctness of Trace MCMC

The second problem we address is implementation correctness. As recent work
shows [19, 22], subtle errors in inference algorithms for probabilistic
languages are a motivation for correctness proofs for probabilistic inference.

_Markov chain Monte Carlo_ (MCMC) is an important class of inference methods,
exemplified by the Metropolis-Hastings (MH) algorithm [26, 17], that
accumulates samples from a target distribution by exploring a Markov chain.
The original work on Church introduced the implementation technique called
_trace MCMC_ [15]. Given a closed term $M$, trace MCMC generates a Markov
chain of traces, $s_{0}$, $s_{1}$, $s_{2}$, …. The MH algorithm is parametric
in a _proposal kernel_ $Q$: a function that maps a trace $s$ of $M$ to a
probability distribution over traces, used to sample the next trace in the
Markov chain.

Our final result, Theorem 4, asserts that the Markov chain generated by trace
MCMC converges to a stationary distribution, and that the induced distribution
on values is equal to the semantics $\llbracket M\rrbracket_{\Rightarrow}$
conditional on success, that is, that the computation terminates and yields a
value (not $\mathtt{fail}$). We formalize the algorithm rigorously, defining
our proposal kernel as a Lebesgue integral of a corresponding density
function, that we show to be measurable with respect to the $\sigma$-algebra
on program traces. We show that the resulting Markov chain satisfies standard
criteria: _aperiodicity_ and _irreducibility_. Hence, Theorem 4 follows from a
classic result of Tierney [38] together with Theorem 3.

###  1.4 Contributions of the Paper

We make the following original contributions:

  * 1.

Definition of an untyped $\lambda$-calculus with continuous distributions
capable of encoding the core of Church.

  * 2.

Development of both sampling-based and distribution-based semantics, shown
equivalent (Theorems 1, 2, and 3).

  * 3.

First proof of correctness of trace MCMC for a $\lambda$-calculus (Theorem 4).

The only previous work on formal semantics of $\lambda$-calculi with
constraints and continuous distributions is recent work by Staton et al. [35].
Their main contribution is an elegant denotational semantics for a simply
typed $\lambda$-calculus with continuous distributions and both hard and soft
constraints, but without recursion. They do not consider MCMC inference. Their
work does not apply to the recursive functions (such as the geometric
distribution in Section 1.1) or data structures (such as lists) typically
found in Church programs. For our purpose of conferring formal semantics on
Church-family languages, we consider it advantageous to rely on untyped
techniques.

The only previous work on correctness of trace MCMC, and an important
influence on our work, is a recent paper by Hur et al. [19] which proves
correct an algorithm for computing an MH Markov chain. Key differences are
that we work with higher-order languages and soft constraints, and that we
additionally give a proof that our Markov chain always converges, via the
correctness criteria of Tierney [38].

###  1.5 Structure of the Paper

The rest of the paper is organized as follows.

Section 2 defines the syntax of our probabilistic $\lambda$-calculus with
draws from continuous distributions, and defines a deterministic _sampling-
based_ operational semantics for our calculus. The semantics is based on the
explicit consumption of a program trace $s$ of random draws and production of
an explicit weight $w$ for each outcome.

Section 3 is concerned with a more in-depth treatment of sampling-based
semantics, given in two standard styles: big-step semantics,
$M\Downarrow^{s}_{w}G$, and small-step semantics,
$(M,w,s)\rightarrow(M^{\prime},w^{\prime},s^{\prime})$, which are equivalent
by Theorem 1. We define a distribution $\llbracket M\rrbracket$ on outcomes of
$M$ by integrating the weights with respect to a measure on traces and
applying a measure transformation.

Section 4 defines our step-indexed _distribution-based_ operational semantics,
in both small-step ($M\Rightarrow_{n}\mathscr{D}$) and big-step
($M\Downarrow_{n}\mathscr{D}$) styles, which by Theorem 2 are equivalent, and
define the meaning $\llbracket M\rrbracket$ of a term $M$ to be the supremum
of the step-indexed semantics. We end by linking the semantics of this section
with those of Section 3: Theorem 3 establishes that $\llbracket
M\rrbracket_{\mathbb{S}}=\llbracket M\rrbracket$

Section 5 formalizes trace MCMC for our calculus, in the spirit of Hur et al.
[19]. Theorem 4 shows equivalence between the distribution computed by the
algorithm and the semantics of the previous sections. Hence, Theorem 4 is the
first correctness theorem for trace MCMC for a $\lambda$-calculus.

Section 6 describes related work and Section 7 concludes.

Appendix A collects various proofs of measurability.

##  2 A Foundational Calculus for Church

In this section, we describe the syntax of our calculus and equip it with an
intuitive semantics relating program outcomes to the sequences of random
choices made during evaluation. By translating Church constructs to this
calculus, we show that it serves as a foundation for Turing-complete
probabilistic languages.

To simplify the presentation, we do not include primitives for discrete
distributions in the calculus, as they can be encoded using the uniform
distribution on the unit interval and inverse mass functions. However, it
would be easy to extend the calculus with primitive discrete random
distributions, represented by their probability mass functions rather than
densities. In Section 3.3, we explain how the semantics could be adapted in
this case.

###  2.1 Syntax of the Calculus

We represent scalar data as real numbers $c\in\mathbb{R}$. We use $0$ and $1$
to represent $\mathtt{false}$ and $\mathtt{true}$, respectively. Let
$\mathcal{I}$ be a countable set of _distribution identifiers_ (or simply
_distributions_). Metavariables for distributions are $\mathsf{D},\mathsf{E}$.
Each distribution identifier $\mathsf{D}$ has an integer _arity_
$\lvert{\mathsf{D}}\rvert\geq 0$, and defines a density function
$\operatorname{pdf}_{\mathsf{D}}:\mathbb{R}^{\lvert{\mathsf{D}}\rvert+1}\to[0,\infty)$
of a sub-probability kernel. For example, a draw (rnd()) from the uniform
distribution on the unit interval has density
$\operatorname{pdf}_{\textsf{rnd}}(c)=1$ if $c\in[0,1]$ and otherwise 0, while
a draw (Gaussian$(m,v)$) from the Gaussian distribution with mean $m$ and
variance $v$ has density
$\operatorname{pdf}_{\textsf{Gaussian}}(m,v,c)=1/(e^{\frac{(c-m)^{2}}{2v}}\sqrt{2v\pi})$
if $v>0$ and otherwise 0.

Let $g$ be a metavariable ranging over a countable set of _function
identifiers_ each with an integer _arity_ $|g|>0$ and with an interpretation
as a total measurable function $\sigma_{g}:\mathbb{R}^{|g|}\to\mathbb{R}$.
Examples of function identifiers include addition $+$, comparison $>$, and
equality $=$; they are often written in infix notation. We define the _values_
$V$ and _terms_ $M$ as follows, where $x$ ranges over a denumerable set of
variables $\mathcal{X}$.

$\displaystyle V$
$\displaystyle::=c\;\;\mbox{\Large{$\mid$}}\;\;x\;\;\mbox{\Large{$\mid$}}\;\;\lambda
x.M$ $\displaystyle M,N$ $\displaystyle::=V\;\;\mbox{\Large{$\mid$}}\;\;M\
N\;\;\mbox{\Large{$\mid$}}\;\;\mathsf{D}(V_{1},\dots,V_{|\mathsf{D}|})\;\;\mbox{\Large{$\mid$}}\;\;g(V_{1},\dots,V_{|g|})$
$\displaystyle\;\;\mbox{\Large{$\mid$}}\;\;\mathtt{if}\ {V}\ \mathtt{then}\
{M}\ \mathtt{else}\
{N}\;\;\mbox{\Large{$\mid$}}\;\;\mathtt{score}(V)\;\;\mbox{\Large{$\mid$}}\;\;\mathtt{fail}$

The term $\mathtt{fail}$ acts as an exception and models a failed hard
constraint. The term $\mathtt{score}(c)$ models a soft constraint, and is
parametrized on a positive probability $c\in(0,1]$. As usual, free occurrences
of $x$ inside $M$ are bound by $\lambda x.M$. Terms are taken modulo renaming
of bound variables. Substitution of all free occurrences of $x$ by a value $V$
in $M$ is defined as usual, and denoted $M\\{V/x\\}$. This can be easily
generalized to $M\\{\vec{V}/\vec{x}\\}$, where $\vec{x}$ is a sequence of
variables and $\vec{V}$ is a sequence of values (of the same length). Let
$\Lambda$ denote the set of all terms, and $C\Lambda$ the set of _closed_
terms. The set of all _closed values_ is $\mathcal{V}$, and we write
$\mathcal{V}_{\lambda}$ for $\mathcal{V}\setminus\mathbb{R}$. _Generalized
values_ $G$, $H$ are elements of the set
$\mathcal{GV}=\mathcal{V}\cup\\{\mathtt{fail}\\}$, i.e., generalized values
are either values or $\mathtt{fail}$. Finally, _erroneous redexes_ , ranged
over by metavariables like $T,R$, are closed terms in one of the following
five forms:

  * •

$c\ M$.

  * •

$\mathsf{D}(V_{1},\dots,V_{|\mathsf{D}|})$ where at least one of the $V_{i}$
is a $\lambda$-abstraction.

  * •

$g(V_{1},\dots,V_{|g|})$ where at least one of the $V_{i}$ is a
$\lambda$-abstraction.

  * •

$\mathtt{if}\ {V}\ \mathtt{then}\ {M}\ \mathtt{else}\ {N}$, where $V$ is
neither $\mathtt{true}$ nor $\mathtt{false}$.

  * •

$\mathtt{score}(V)$, where $V\notin(0,1]$.

###  2.2 Big-step Sampling-based Semantics

In defining the first semantics of the calculus, we use the classical
observation [23] that a probabilistic program can be interpreted as a
deterministic program parametrized by the sequence of random draws made during
the evaluation. We write $M\Downarrow^{s}_{w}V$ to mean that evaluating $M$
with the outcomes of random draws as listed in the sequence $s$ yields the
value $V$, together with the _weight_ $w$ that expresses how likely this
sequence of random draws would be if the program was just evaluated randomly.
Because our language has continuous distributions, $w$ is a probability
_density_ rather than a probability mass. Similarly,
$M\Downarrow^{s}_{w}\mathtt{fail}$ means that evaluation of $M$ with the
random sequence $s$ fails. In either case, the finite trace $s$ consists of
exactly the random choices made during evaluation, with no unused choices
permitted.

Formally, we define _program traces_ $s$, $t$ to be finite sequences
$[c_{1},\dots,c_{n}]$ of reals of arbitrary length. We let
$M\Downarrow^{s}_{w}G$ be the least relation closed under the rules in Figure
2. The (Eval Random) rule replaces a random draw from a distribution
$\mathsf{D}$ parametrized by a vector $\vec{c}$ with the first (and only)
element $c$ of the trace, presumed to be the outcome of the random draw, and
sets the weight to the value of the density of $\mathsf{D}(\vec{c})$ at $c$.
(Eval Random Fail) throws an exception if $c$ is outside the support of the
corresponding distribution. Meanwhile, (Eval Score), applied to
$\mathtt{score}(c)$, sets the weight to $c$ and returns a dummy value. The
applications of soft constraints using $\mathtt{score}$ are described in
Section 2.5.

$G\in\mathcal{GV}$ $G\Downarrow^{[]}_{1}G$ (Eval Val)
$w=\operatorname{pdf}_{\mathsf{D}}(\vec{c},c)$ $w>0$
$\mathsf{D}(\vec{c})\Downarrow^{[c]}_{w}c$ (Eval Random)
$\operatorname{pdf}_{\mathsf{D}}(\vec{c},c)=0$
$\mathsf{D}(\vec{c})\Downarrow^{[c]}_{0}\mathtt{fail}$ (Eval Random Fail)
$g(\vec{c})\Downarrow^{[]}_{1}\sigma_{g}(\vec{c})$ (Eval Prim)
$M\Downarrow^{s_{1}}_{w_{1}}\lambda x.P$ $N\Downarrow^{s_{2}}_{w_{2}}V$
$P[V/x]\Downarrow^{s_{3}}_{w_{3}}G$ $M\
N\Downarrow^{s_{1}@s_{2}@s_{3}}_{w_{1}\cdot w_{2}\cdot w_{3}}G$ (Eval Appl)
$M\Downarrow^{s}_{w}\mathtt{fail}$ $M\ N\Downarrow^{s}_{w}\mathtt{fail}$ (Eval
Appl Raise1) $M\Downarrow^{s}_{w}c$ $M\ N\Downarrow^{s}_{w}\mathtt{fail}$
(Eval Appl Raise2) $M\Downarrow^{s_{1}}_{w_{1}}\lambda x.P$
$N\Downarrow^{s_{2}}_{w_{2}}\mathtt{fail}$ $M\
N\Downarrow^{s_{1}@s_{2}}_{w_{1}\cdot w_{2}}\mathtt{fail}$ (Eval Appl Raise3)
$M\Downarrow^{s}_{w}G$ $\mathtt{if}\ {\mathtt{true}}\ \mathtt{then}\ {M}\
\mathtt{else}\ {N}\Downarrow^{s}_{w}G$ (Eval If True) $N\Downarrow^{s}_{w}G$
$\mathtt{if}\ {\mathtt{false}}\ \mathtt{then}\ {M}\ \mathtt{else}\
{N}\Downarrow^{s}_{w}G$ (Eval If False) $c\in(0,1]$
$\mathtt{score}(c)\Downarrow^{[]}_{c}\mathtt{true}$ (Eval Score) $T$ is an
erroneous redex $T\Downarrow^{[]}_{1}\mathtt{fail}$ (Eval Fail)

Figure 1: Sampling-Based Big Step Semantics

$G\in\mathcal{GV}$ $G\Downarrow^{[]}_{1}G$ (Eval Val)
$w=\operatorname{pdf}_{\mathsf{D}}(\vec{c},c)$ $w>0$
$\mathsf{D}(\vec{c})\Downarrow^{[c]}_{w}c$ (Eval Random)
$\operatorname{pdf}_{\mathsf{D}}(\vec{c},c)=0$
$\mathsf{D}(\vec{c})\Downarrow^{[c]}_{0}\mathtt{fail}$ (Eval Random Fail)
$g(\vec{c})\Downarrow^{[]}_{1}\sigma_{g}(\vec{c})$ (Eval Prim)
$M\Downarrow^{s_{1}}_{w_{1}}\lambda x.P$ $N\Downarrow^{s_{2}}_{w_{2}}V$
$P[V/x]\Downarrow^{s_{3}}_{w_{3}}G$ $M\
N\Downarrow^{s_{1}@s_{2}@s_{3}}_{w_{1}\cdot w_{2}\cdot w_{3}}G$ (Eval Appl)
$M\Downarrow^{s}_{w}\mathtt{fail}$ $M\ N\Downarrow^{s}_{w}\mathtt{fail}$ (Eval
Appl Raise1) $M\Downarrow^{s}_{w}c$ $M\ N\Downarrow^{s}_{w}\mathtt{fail}$
(Eval Appl Raise2) $M\Downarrow^{s_{1}}_{w_{1}}\lambda x.P$
$N\Downarrow^{s_{2}}_{w_{2}}\mathtt{fail}$ $M\
N\Downarrow^{s_{1}@s_{2}}_{w_{1}\cdot w_{2}}\mathtt{fail}$ (Eval Appl Raise3)
$M\Downarrow^{s}_{w}G$ $\mathtt{if}\ {\mathtt{true}}\ \mathtt{then}\ {M}\
\mathtt{else}\ {N}\Downarrow^{s}_{w}G$ (Eval If True) $N\Downarrow^{s}_{w}G$
$\mathtt{if}\ {\mathtt{false}}\ \mathtt{then}\ {M}\ \mathtt{else}\
{N}\Downarrow^{s}_{w}G$ (Eval If False) $c\in(0,1]$
$\mathtt{score}(c)\Downarrow^{[]}_{c}\mathtt{true}$ (Eval Score) $T$ is an
erroneous redex $T\Downarrow^{[]}_{1}\mathtt{fail}$ (Eval Fail)

Figure 2: Sampling-Based Big Step Semantics

All the other rules are standard for a call-by-value lambda-calculus, except
that they allow the traces to be split between subcomputations and they
multiply the weights yielded by subcomputations to obtain the overall weight.

###  2.3 Encoding Church

We now demonstrate the usefulness and expressive power of the calculus via a
translation of Church, an untyped higher-order functional probabilistic
language.

The syntax of Church’s _expressions_ , _definitions_ and _queries_ is
described as follows:

$\displaystyle e\;::=\;$ $\displaystyle
c\;\;\mbox{\Large{$\mid$}}\;\;x\;\;\mbox{\Large{$\mid$}}\;\;\texttt{(}g\
e_{1}\dots e_{n}\texttt{)}\;\;\mbox{\Large{$\mid$}}\;\;\texttt{(}\mathsf{D}\
e_{1}\dots e_{n}\texttt{)}\;\;\mbox{\Large{$\mid$}}\;\;\texttt{(if}\ e_{1}\
e_{2}\ e_{3}\texttt{)}$ $\mid$ $\displaystyle\texttt{(lambda}\ (x_{1}\dots
x_{n})\ e\texttt{)}\;\;\mbox{\Large{$\mid$}}\;\;\texttt{(}e_{1}\ e_{2}\dots
e_{n}\texttt{)}$ $\displaystyle\texttt{d}\;::=\;$
$\displaystyle\texttt{(define}\ x\ e\texttt{)}$
$\displaystyle\texttt{q}\;::=\;$ $\displaystyle\texttt{(query}\ d_{1}\dots
d_{n}\ e\ e_{cond}\texttt{)}$

To make the translation more intuitive, it is convenient to add to the target
language a let-expression of the form $\mathtt{let}\ x=M\ \mathtt{in}\ N$,
that can be interpreted as syntactic sugar for $(\lambda x.N)\ M$, and
sequencing $M;N$ that stands for $\lambda\\!\star\\!.N\ M$ where $\star$ as
usual stands for a variable that does not appear free in any of the terms
under consideration.

$\begin{array}[t]{@{}l@{}}\langle c\rangle_{e}=c\\\ \langle x\rangle_{e}=x\\\
\langle g\ e_{1},\dots,e_{n}\rangle_{e}=\\\ \qquad\mathtt{let}\ x_{1}=e_{1}\
\mathtt{in}\ \dots\mathtt{let}\ x_{n}=e_{n}\ \mathtt{in}\
g(x_{1},\dots,x_{n})\\\ \qquad\text{where}\
x_{1},\dots,x_{n}\notin\mathit{fv}(e_{1})\cup\dots\cup\mathit{fv}(e_{n})\\\
\langle\mathsf{D}\ e_{1},\dots e_{n}\rangle_{e}=\\\ \qquad\mathtt{let}\
x_{1}=e_{1}\ \mathtt{in}\ \dots\mathtt{let}\ x_{n}=e_{n}\ \mathtt{in}\
\mathsf{D}(x_{1},\dots,x_{n})\\\ \qquad\text{where}\
x_{1},\dots,x_{n}\notin\mathit{fv}(e_{1})\cup\dots\cup\mathit{fv}(e_{n})\\\
\langle\mathtt{lambda}\ ()\ e\rangle_{e}=\lambda x.\langle
e\rangle_{e}\quad\text{where}\ x\notin\mathit{fv}(e)\\\
\langle\mathtt{lambda}\ x\ e\rangle_{e}=\lambda x.\langle e\rangle_{e}\\\
\langle\mathtt{lambda}\ (x_{1}\ \dots\ x_{n})\ e\rangle_{e}=\lambda
x_{1}.\langle\mathtt{lambda}\ (x_{2}\ \dots\ x_{n})\ e\rangle_{e}\\\ \langle
e_{1}\ e_{2}\rangle_{e}=\langle e_{1}\rangle_{e}\ \langle e_{2}\rangle_{e}\\\
\langle e_{1}\ e_{2}\ \dots\ e_{n}\rangle_{e}=\langle(e_{1}\ e_{2})\ \dots\
e_{n}\rangle_{e}\\\ \langle\mathtt{if}\ e_{1}\ e_{2}\
e_{3}\rangle_{e}=\mathtt{let}\ x=e_{1}\ \mathtt{in}\ (\mathtt{if}\ {x}\
\mathtt{then}\ {\langle e_{2}\rangle_{e}}\ \mathtt{else}\ {\langle
e_{3}\rangle_{e}})\\\ \qquad\text{where}\
x\notin\mathit{fv}(e_{2})\cup\mathit{fv}(e_{3})\\\ \\\ \langle\mathtt{query}\
(\mathtt{define}\ x_{1}\ e_{1})\dots(\mathtt{define}\ x_{n}\ e_{n})\ e_{out}\
e_{cond}\rangle=\\\ \qquad\mathtt{let}\ x_{1}=(\mathit{fix}\ x_{1}.\langle
e_{1}\rangle_{e})\ \mathtt{in}\\\ \dots\\\ \qquad\mathtt{let}\
x_{n}=(\mathit{fix}\ x_{n}.\langle e_{n}\rangle_{e})\ \mathtt{in}\\\
\qquad\mathtt{let}\ b=e_{cond}\ \mathtt{in}\\\ \qquad\mathtt{if}\ {b}\
\mathtt{then}\ {e_{out}}\ \mathtt{else}\ {\mathtt{fail}}\end{array}$

Figure 3: Translation of Church

$\begin{array}[t]{@{}l@{}}\langle c\rangle_{e}=c\\\ \langle x\rangle_{e}=x\\\
\langle g\ e_{1},\dots,e_{n}\rangle_{e}=\\\ \qquad\mathtt{let}\ x_{1}=e_{1}\
\mathtt{in}\ \dots\mathtt{let}\ x_{n}=e_{n}\ \mathtt{in}\
g(x_{1},\dots,x_{n})\\\ \qquad\text{where}\
x_{1},\dots,x_{n}\notin\mathit{fv}(e_{1})\cup\dots\cup\mathit{fv}(e_{n})\\\
\langle\mathsf{D}\ e_{1},\dots e_{n}\rangle_{e}=\\\ \qquad\mathtt{let}\
x_{1}=e_{1}\ \mathtt{in}\ \dots\mathtt{let}\ x_{n}=e_{n}\ \mathtt{in}\
\mathsf{D}(x_{1},\dots,x_{n})\\\ \qquad\text{where}\
x_{1},\dots,x_{n}\notin\mathit{fv}(e_{1})\cup\dots\cup\mathit{fv}(e_{n})\\\
\langle\mathtt{lambda}\ ()\ e\rangle_{e}=\lambda x.\langle
e\rangle_{e}\quad\text{where}\ x\notin\mathit{fv}(e)\\\
\langle\mathtt{lambda}\ x\ e\rangle_{e}=\lambda x.\langle e\rangle_{e}\\\
\langle\mathtt{lambda}\ (x_{1}\ \dots\ x_{n})\ e\rangle_{e}=\lambda
x_{1}.\langle\mathtt{lambda}\ (x_{2}\ \dots\ x_{n})\ e\rangle_{e}\\\ \langle
e_{1}\ e_{2}\rangle_{e}=\langle e_{1}\rangle_{e}\ \langle e_{2}\rangle_{e}\\\
\langle e_{1}\ e_{2}\ \dots\ e_{n}\rangle_{e}=\langle(e_{1}\ e_{2})\ \dots\
e_{n}\rangle_{e}\\\ \langle\mathtt{if}\ e_{1}\ e_{2}\
e_{3}\rangle_{e}=\mathtt{let}\ x=e_{1}\ \mathtt{in}\ (\mathtt{if}\ {x}\
\mathtt{then}\ {\langle e_{2}\rangle_{e}}\ \mathtt{else}\ {\langle
e_{3}\rangle_{e}})\\\ \qquad\text{where}\
x\notin\mathit{fv}(e_{2})\cup\mathit{fv}(e_{3})\\\ \\\ \langle\mathtt{query}\
(\mathtt{define}\ x_{1}\ e_{1})\dots(\mathtt{define}\ x_{n}\ e_{n})\ e_{out}\
e_{cond}\rangle=\\\ \qquad\mathtt{let}\ x_{1}=(\mathit{fix}\ x_{1}.\langle
e_{1}\rangle_{e})\ \mathtt{in}\\\ \dots\\\ \qquad\mathtt{let}\
x_{n}=(\mathit{fix}\ x_{n}.\langle e_{n}\rangle_{e})\ \mathtt{in}\\\
\qquad\mathtt{let}\ b=e_{cond}\ \mathtt{in}\\\ \qquad\mathtt{if}\ {b}\
\mathtt{then}\ {e_{out}}\ \mathtt{else}\ {\mathtt{fail}}\end{array}$

Figure 4: Translation of Church

The rules for translating Church expressions to the calculus are shown in
Figure 4, where $\mathit{fv}(e)$ denotes the set of free variables in
expression $e$ and $\mathit{fix}\ x.M$ is a call-by-value fixpoint combinator
$\lambda y.N_{\mathit{fix}}N_{\mathit{fix}}(\lambda x.M)y$ where
$N_{\mathit{fix}}$ is $\lambda z.\lambda w.w(\lambda y.((zz)w)y)$. Observe
that $(\mathit{fix}\ x.M)V$ evaluates to $M\\{(\mathit{fix}\ x.M)/x\\}V$
deterministically. We assume that for each distribution identifier
$\mathsf{D}$ of arity $k$, there is a deterministic function
$\operatorname{pdf}_{\mathsf{D}}$ of arity $k+1$ that calculates the
corresponding density at the given point.

In addition to expressions presented here, Church also supports _stochastic
memoization_ [15] by means of a mem function, which, applied to any given
function, produces a version of it that always returns the same value when
applied to the same arguments. This feature allows for functions of integers
to be treated as infinite lazy lists of random values, and is useful in
defining some nonparametric models, such as the Dirichlet Process.

It would be straightforward to add support for memoization in our encoding by
changing the translation to state-passing style, but we omit this standard
extension for the sake of brevity.

###  2.4 Example: Geometric Distribution

To illustrate the sampling-based semantics, recall the geometric distribution
example from Section 1. It translates to the following program in the core
calculus:

let flip = λx. (rnd() ¡ x) inlet geometric =(fix g.λp. (let y = rnd() ¡ p inif
y then 0 else 1 + (g p)) ) inlet n = fix n’.geometric 0.5 inlet b = n ¿ 1 inif
b then n else fail

Suppose we want to evaluate this program on the random trace
$s=[0.7,0.8,0.3]$. By (Eval Appl), we can substitute the definitions of flip
and geometric in the remainder of the program, without consuming any elements
of the trace nor changing the weight of the sample. Then we need to evaluate
$\textit{geometric}\ 0.5$.

It can be shown (by repeatedly applying (Eval Appl)) that for any lambda-
abstraction $\lambda x.M$, $M\\{(\mathit{fix}\ x.M)/x\\}\
V\Downarrow^{s}_{w}G$ if and only if $(\mathit{fix}\ x.M)\
V\Downarrow^{s}_{w}G$, which allows us to unfold the recursion. Applying the
unfolded definition of geometric to the argument $0.5$ yields an expression of
the form

let y = rnd() ¡ 0.5 inif y then 0 else 1 + (…).

For the first random draw, we have rnd$()\Downarrow^{[0.7]}_{1}0.7$ by (Eval
Random) (because the density of rnd is $1$ on the interval $[0,1]$) and so
(Eval Prim) gives rnd$()<0.5\Downarrow^{[0.7]}_{1}~{}\mathtt{false}$. After
unfolding the recursion two more times, evaluating the subsequent “flips”
yields rnd$()<0.5\Downarrow^{[0.8]}_{1}~{}\mathtt{false}$ and
rnd$()<0.5\Downarrow^{[0.3]}_{1}~{}\mathtt{true}$. By (Eval If True), the last
if-statement evaluates to $0$, terminating the recursion. Combining the
results by (Eval Appl), (Eval If False) and (Eval Prim), we arrive at
$\textit{geometric}\ 0.5\Downarrow^{[0.7,0.8,0.3]}_{1}~{}2$.

At this point, it is straightforward to see that the condition in the if-
statement on the final line is satisfied, and hence the program reduces with
the given trace to the value $2$ with weight $1$.

This program actually yields weight $1$ for every trace that returns an
integer value. This may seem counter-intuitive, because clearly not all
outcomes have the same probability. However, the probability of a given
outcome is given by an integral over the space of traces, as described in
Section 3.4.

###  2.5 Soft Constraints and score

The geometric distribution example in Section 2.4 uses a _hard constraint_ :
program execution fails and the value of $n$ is discarded whenever the Boolean
predicate $n>1$ is not satisfied. In many machine learning applications we
want to use a different kind of constraint that models noisy data. For
instance, if $c$ is the known output of a sensor that shows an approximate
value of some unknown quantity $x$ that is computed by the program, we want to
assign higher probabilities to values of $x$ that are closer to $c$. This is
sometimes known as a _soft constraint_.

One naive way to implement a soft constraint is to use a hard constraint with
a success probability based on $\lvert x-c\rvert$, for instance,

$\textit{condition}\ x\ c\ M:=\mathtt{if}\
{\textit{flip}(\textit{exp}({-(x-c)^{2}}))}\ \mathtt{then}\ {M}\
\mathtt{else}\ {\mathtt{fail}}.$

Then $\textit{condition}\ x\ c\ M$ has the effect of continuing as $M$ with
probability $\textit{exp}({-(x-c)^{2}})$, and otherwise terminating execution.
In the context of a sampling-based semantics, it has the effect of adding a
uniform sample from $[0,\textit{exp}({-(x-c)^{2}}))$ to any successful trace,
in addition to introducing more failing traces.

Instead, our calculus includes a primitive score, that avoids both adding
dummy samples and introducing more failing traces. It also admits the
possibility of using efficient gradient-based methods of inference (e.g.,
Homan and Gelman [18]). Using score, the above conditioning operator can be
redefined as

$\textit{score-condition}\ x\ c\
M:=\mathtt{score}(\textit{exp}({-(x-c)^{2}}));M$

###  2.6 Example: Linear Regression

For an example of soft constraints, consider the ubiquitous linear regression
model $y=m\cdot x+b+\mathit{noise}$, where $x$ is often a known feature and
$y$ an observable outcome variable. We can model the noise as drawn from a
Gaussian distribution with mean 0 and variance 1/2 by letting the success
probability be given by the function squash below.

The following query666Cf. http://forestdb.org/models/linear-regression.html.
predicts the $y$-coordinate for $x=4$, given observations of four points:
$(0,0)$, $(1,1)$, $(2,4)$, and $(3,6)$. (We use the abbreviation (define ($f$
$x_{1}$ $\dots$ $x_{n}$) $e$) for (define $f$ (lambda ($x_{1}$ $\dots$
$x_{n}$) $e$), and use and for multiadic conjunction.)

⬇

(query

(define (sqr x) (* x x)))

(define (squash x y) (exp(- (sqr(- x y)))))

(define (flip p) (< (rnd) p))

(define (softeq x y) (flip (squash x y))))

(define m (gaussian 0 2))

(define b (gaussian 0 2))

(define (f x) (+ (* m x) b))

(f 4) ;; predict y for x=4

(and (softeq (f 0) 0) (softeq (f 1) 1)

(softeq (f 2) 4) (softeq (f 3) 6))

The model described above puts independent Gaussian priors on $m$ and $b$. The
condition of the query states that all observed $y$s are (soft) equal to
$k\cdot x+m$. Assuming that softeq is used only to define constraints (i.e.,
positively), we can avoid the nuisance parameter that arises from each flip by
redefining softeq as follows (given a score primitive in Church, mapped to
$\mathtt{score}(-)$ in our $\lambda$-calculus):

⬇

(define (softeq x y) (score (squash x y)))

##  3 Sampling-Based Operational Semantics

In this section, we further investigate sampling-based semantics for our
calculus. First, we introduce _small_ -step sampling-based semantics and prove
it equivalent to its big-step sibling as introduced in Section 2.2. Then, we
associate to any closed term $M$ two sub-probability distributions: one on the
set of random traces, and the other on the set of return values. This requires
some measure theory, recalled in Section 3.2.

###  3.1 Small-step Sampling-based Semantics

We define small-step call-by-value evaluation. _Evaluation contexts_ are
defined as follows:

$E::=[\cdot]\;\;\mbox{\Large{$\mid$}}\;\;EM\;\;\mbox{\Large{$\mid$}}\;\;(\lambda
x.M)E$

We let $\mathcal{C}$ be the set of all closed evaluation contexts, i.e., where
every occurrence of a variable $x$ is as a subterm of $\lambda x.M$. The term
obtained by replacing the only occurrence of $[\cdot]$ in $E$ by $M$ is
indicated as $E[M]$. _Redexes_ are generated by the following grammar:

$\displaystyle R\;::=\;$ $\displaystyle(\lambda
x.M)V\;\;\mbox{\Large{$\mid$}}\;\;\mathsf{D}(\vec{c})\;\;\mbox{\Large{$\mid$}}\;\;g({\vec{c}})\;\;\mbox{\Large{$\mid$}}\;\;\mathtt{score}(c)$
$\displaystyle\;\;\mbox{\Large{$\mid$}}\;\;\mathtt{fail}\;\;\mbox{\Large{$\mid$}}\;\;\mathtt{if}\
{\mathtt{true}}\ \mathtt{then}\ {M}\ \mathtt{else}\ {N}$
$\displaystyle\;\;\mbox{\Large{$\mid$}}\;\;\mathtt{if}\ {\mathtt{false}}\
\mathtt{then}\ {M}\ \mathtt{else}\ {N}\;\;\mbox{\Large{$\mid$}}\;\;T$

_Reducible terms_ are those closed terms $M$ that can be written as $E[R]$.

###### Lemma 1

For every closed term $M$, either $M$ is a generalized value or there are
unique $E,R$ such that $M=E[R]$. Moreover, if $M$ is not a generalized value
and $R=\mathtt{fail}$, then $E$ is proper, that is, $E\neq[\cdot]$.

  * Proof.

This is an easy induction on the structure of $M$. $\Box$

_Deterministic reduction_ is the relation $\xrightarrow{\text{det}}$ on closed
terms defined in Figure 5.

$\displaystyle E[g(\vec{c})]$
$\displaystyle\xrightarrow{\text{det}}E[\sigma_{g}(\vec{c})]$ $\displaystyle
E[(\lambda x.M)\ V]$ $\displaystyle\xrightarrow{\text{det}}E[M\\{V/x\\}]$
$\displaystyle E[\mathtt{if}\ {1}\ \mathtt{then}\ {M_{2}}\ \mathtt{else}\
{M_{3}}]$ $\displaystyle\xrightarrow{\text{det}}E[M_{2}]$ $\displaystyle
E[\mathtt{if}\ {0}\ \mathtt{then}\ {M_{2}}\ \mathtt{else}\ {M_{3}}]$
$\displaystyle\xrightarrow{\text{det}}E[M_{3}]$ $\displaystyle E[T]$
$\displaystyle\xrightarrow{\text{det}}E[\mathtt{fail}]$ $\displaystyle
E[\mathtt{fail}]$
$\displaystyle\xrightarrow{\text{det}}\mathtt{\mathtt{fail}}\quad\text{if $E$
is not $[\cdot]$}$

Figure 5: Deterministic Reduction.

###### Lemma 2

If $M\xrightarrow{\text{det}}M^{\prime}$ and
$M\xrightarrow{\text{det}}M^{\prime\prime}$ then
$M^{\prime}=M^{\prime\prime}$.

  * Proof.

Since $M\xrightarrow{\text{det}}M^{\prime}$ implies that $M$ is not a
generalized value, Lemma 1 states that $M=E[R]$ for some unique $E$, $R$. If
$R=\mathtt{fail}$, then $E$ is proper and $E[R]$ can only reduce to
$\mathtt{fail}$. Otherwise, it follows immediately by inspection of the
reduction rules that $E[R]\xrightarrow{\text{det}}E[N]$ for some $N$ that is
uniquely determined by the redex $R$. $\Box$

Let us define composition of contexts $E\circ E^{\prime}$ inductively as:

$\displaystyle[\ ]\circ E^{\prime}$
$\displaystyle\mathrel{\smash[t]{\triangleq}}$ $\displaystyle E^{\prime}$
$\displaystyle(E\ M)\circ E^{\prime}$
$\displaystyle\mathrel{\smash[t]{\triangleq}}$ $\displaystyle(E\circ
E^{\prime})\ M$ $\displaystyle((\lambda x.M)\ E)\circ E^{\prime}$
$\displaystyle\mathrel{\smash[t]{\triangleq}}$ $\displaystyle(\lambda x.M)\
(E\circ E^{\prime})$

###### Lemma 3

$(E\circ E^{\prime})[M]=E[E^{\prime}[M]]$.

  * Proof.

By induction on the structure of $E$. $\Box$

###### Lemma 4

If $E[R]\xrightarrow{\text{det}}E[N]$, then $R\xrightarrow{\text{det}}N$.

  * Proof.

By case analysis on the deterministic reduction rules.

###### Lemma 5

For any $E$ and $M$ such that $M\neq E^{\prime}[\mathtt{fail}]$, if
$M\xrightarrow{\text{det}}M^{\prime}$ then
$E[M]\xrightarrow{\text{det}}E[M^{\prime}]$.

  * Proof.

Standard, using Lemmas 1 and 2.

Since $M\xrightarrow{\text{det}}M^{\prime}$, $M$ is not a generalized value.
By Lemma 1, $M=E^{\prime}[R]$ for some $E^{\prime}$, $R$.

By assumption, $R\neq\mathtt{fail}$, so by inspection of the reduction rules
$E^{\prime}[R]\xrightarrow{\text{det}}E^{\prime}[N]$ for some $N$. By Lemma 2,
$E^{\prime}[N]=M^{\prime}$. By Lemma 3, $E[M]=(E\circ E^{\prime})[R]$ and
$E[M^{\prime}]=(E\circ E^{\prime})[N]$.

Since Lemma 4 gives $R\xrightarrow{\text{det}}N$, by case analysis on the
derivation of $R\xrightarrow{\text{det}}N$ we can show that $(E\circ
E^{\prime})[R]\xrightarrow{\text{det}}(E\circ E^{\prime})[N]$, which implies
$E[M]\xrightarrow{\text{det}}E[M^{\prime}]$.

$\Box$

$M\xrightarrow{\text{det}}N$ $(M,w,s)\rightarrow(N,w,s)$ (Red Pure)
$c\in(0,1]$ $(E[\mathtt{score}(c)],w,s)\rightarrow(E[\mathtt{true}],c\cdot
w,s)$ (Red Score) $w^{\prime}=\operatorname{pdf}_{\mathsf{D}}(\vec{c},c)$
$w^{\prime}>0$
$(E[\mathsf{D}(\vec{c})],w,c\mathrel{::}s)\rightarrow(E[c],w\cdot
w^{\prime},s)$ (Red Random) $\operatorname{pdf}_{\mathsf{D}}(\vec{c},c)=0$
$(E[\mathsf{D}(\vec{c})],w,c\mathrel{::}s)\rightarrow(E[\mathtt{fail}],0,s)$
(Red Random Fail)

Figure 6: Small-step sampling-based operational semantics

###### Lemma 6

If $(M,w,s)\rightarrow(M^{\prime},w^{\prime},s^{\prime})$ and
$(M,w,s)\rightarrow(M^{\prime\prime},w^{\prime\prime},s^{\prime\prime})$, then
$M^{\prime}=M^{\prime\prime}$, $w^{\prime}=w^{\prime\prime}$ and
$s^{\prime\prime}=s^{\prime}$.

  * Proof.

By case analysis. Since there is no rule that reduces generalized values,
$(M,w,s)\rightarrow(M^{\prime},w^{\prime},s^{\prime})$ implies that
$M\notin\mathcal{GV}$, so by Lemma 1, $M=E[R]$ for some unique $E$, $R$.

    * •

If $(M,w,s)\rightarrow(M^{\prime},w^{\prime},s^{\prime})$ was derived with
(Red Pure), then $M=E[R]$, where $R\neq\mathsf{D}(\underline{c})$ and
$R\neq\mathtt{score}(c)$, which implies that
$(M,w,s)\rightarrow(M^{\prime\prime},w^{\prime\prime},s^{\prime\prime})$ must
also have been derived with (Red Pure). Hence, we have
$w^{\prime\prime}=w^{\prime}=w$, $s^{\prime\prime}=s^{\prime}=s$,
$M\xrightarrow{\text{det}}M^{\prime}$ and
$M\xrightarrow{\text{det}}M^{\prime\prime}$. By Lemma 2,
$M^{\prime\prime}=M^{\prime}$, as required.

    * •

If $(M,w,s)\rightarrow(M^{\prime},w^{\prime},s^{\prime})$ was derived with
(Red Random), then $M=E[\mathsf{D}(\vec{c})]$, $s=c\mathrel{::}s^{*}$ and
$\operatorname{pdf}_{\mathsf{D}}(\vec{c},c)>0$. Hence,
$(M,w,s)\rightarrow(M^{\prime\prime},w^{\prime\prime},s^{\prime\prime})$ must
also have been derived with (Red Random), and so
$M^{\prime\prime}=M^{\prime}=E[c]$, $s^{\prime\prime}=s^{\prime}=s^{*}$ and
$w^{\prime\prime}=w^{\prime}=w\operatorname{pdf}_{\mathsf{D}}(\vec{c},c)$, as
required. The (Red Random Fail) case is analogous.

    * •

If $(M,w,s)\rightarrow(M^{\prime},w^{\prime},s^{\prime})$ was derived with
(Red Score), then $M=E[\mathtt{score}(c)]$ and $c\in(0,1]$, so
$(M,w,s)\rightarrow(M^{\prime\prime},w^{\prime\prime},s^{\prime\prime})$ must
also have been derived with (Red Score). Hence
$M^{\prime\prime}=M^{\prime}=E[\mathtt{true}]$,
$w^{\prime\prime}=w^{\prime}=c\cdot w$ and $s^{\prime\prime}=s^{\prime}=s$.

$\Box$

Rules of small-step reduction are given in Figure 6. We let _multi-step
reduction_ be the inductively defined relation
$(M,w,s)\Rightarrow(M^{\prime},w^{\prime},s^{\prime})$ if and only if
$(M,w,s)=(M^{\prime},w^{\prime},s^{\prime})$ or
$(M,w,s)\to(M^{\prime\prime},w^{\prime\prime},s^{\prime\prime})\Rightarrow(M^{\prime},w^{\prime},s^{\prime})$
for some $M^{\prime\prime},w^{\prime\prime},s^{\prime\prime}$. As can be
easily verified, the multi-step reduction of a term to a generalized value is
deterministic once the underlying trace is kept fixed:

###### Lemma 7

If both $(M,w,s)\Rightarrow(G^{\prime},w^{\prime},s^{\prime})$ and
$(M,w,s)\Rightarrow(G^{\prime\prime},w^{\prime\prime},s^{\prime\prime})$, then
$G^{\prime}=G^{\prime\prime}$, $w^{\prime}=w^{\prime\prime}$ and
$s^{\prime}=s^{\prime\prime}$.

  * Proof.

By induction on the derivation of
$(M,w,s)\Rightarrow(G^{\prime},w^{\prime},s^{\prime})$, with appeal to Lemma
6.

    * •

Base case: $(M,w,s)=(G^{\prime},w^{\prime},s^{\prime})$. Generalized values do
not reduce, so $G^{\prime\prime}=G^{\prime}=G$,
$w^{\prime\prime}=w^{\prime}=w$ and $s^{\prime\prime}=s^{\prime}=s$.

    * •

Induction step:
$(M,w,s)\rightarrow(\hat{M},\hat{w},\hat{s})\Rightarrow(G^{\prime},w^{\prime},s^{\prime})$.
Since $M\neq G^{\prime\prime}$, we also have
$(M,w,s)\rightarrow(M^{*},w^{*},s^{*})\Rightarrow(G^{\prime\prime},w^{\prime\prime},s^{\prime\prime})$.

By Lemma 6, $(M^{*},w^{*},s^{*})=(\hat{M},\hat{w},\hat{s})$, and so by
induction hypothesis,
$(G^{\prime\prime},w^{\prime\prime},s^{\prime\prime})=(G^{\prime},w^{\prime},s^{\prime})$,
as required.

$\Box$

###### Lemma 8

For any $E$ and $M$ such that $M\neq E^{\prime}[\mathtt{fail}]$, if
$(M,w,s)\rightarrow(M^{\prime},w^{\prime},s^{\prime})$ then
$(E[M],w,s)\rightarrow(E[M^{\prime}],w^{\prime},s^{\prime})$

  * Proof.

By inversion of $\rightarrow$, using Lemma 5.

    * •

If $(M,w,s)\rightarrow(M^{\prime},w^{\prime},s^{\prime})$ was derived with
(Red Pure), then $M\xrightarrow{\text{det}}M^{\prime}$, so by Lemma 5,
$E[M]\xrightarrow{\text{det}}E[M^{\prime}]$, and by (Red Pure),
$(E[M],w,s)\rightarrow(E[M^{\prime}],w^{\prime},s^{\prime})$.

    * •

If $(M,w,s)\rightarrow(M^{\prime},w^{\prime},s^{\prime})$ was derived with
(Red Random), then $M=E^{\prime}[\mathsf{D}(\vec{c})]$,
$M^{\prime}=E^{\prime}[c]$, $s=c\mathrel{::}s^{\prime}$ and
$w^{\prime}=w\operatorname{pdf}_{\mathsf{D}}(\vec{c},c)$, where
$\operatorname{pdf}_{\mathsf{D}}(\vec{c},c)>0$. By (Red Random) and Lemma 3,
we can derive $(E[M],w,s)\rightarrow(E[M^{\prime}],w^{\prime},s^{\prime})$.
Cases (Red Random Fail) and (Red Score) are anaologous.

$\Box$

###### Lemma 9

If $(E[R],w,s)\rightarrow(E[N],w^{\prime},s^{\prime})$ then
$(R,w,s)\rightarrow(N,w^{\prime},s^{\prime})$

  * Proof.

By case analysis.

    * •

If $(E[R],w,s)\rightarrow(E[N],w^{\prime},s^{\prime})$ was derived with (Red
Pure), then $E[R]\xrightarrow{\text{det}}E[N]$, so by Lemma 5,
$R\xrightarrow{\text{det}}N$, which implies
$(M,w,s)\rightarrow(M^{\prime},w^{\prime},s^{\prime})$.

    * •

If $(E[R],w,s)\rightarrow(E[N],w^{\prime},s^{\prime})$ was derived with (Red
Random), then $R=\mathsf{D}(\vec{c})$, $N=c$, $s=c\mathrel{::}s^{\prime}$ and
$w^{\prime}=w\operatorname{pdf}_{\mathsf{D}}(\vec{c},c)$, where
$\operatorname{pdf}_{\mathsf{D}}(\vec{c},c)>0$.

Hence, with (Red Random), we can derive
$(\mathsf{D}(\vec{c}),w,s)\rightarrow(c,w^{\prime},s^{\prime})$

Cases (Red Random Fail) and (Red Score) are anaologous.

Reduction can take place in any evaluation context, provided the result is not
a failure. Moreover, multi-step reduction is a transitive relation. This is
captured by the following lemmas.

###### Lemma 10

For any $E$, if $(M,w,s)\Rightarrow(M^{\prime},w^{\prime},s^{\prime})$ and
$M^{\prime}\neq\mathtt{fail}$, then we have
$(E[M],w,s)\Rightarrow(E[M^{\prime}],w^{\prime},s^{\prime})$.

  * Proof.

By induction on the number of steps in the derivation of
$(M,w,s)\Rightarrow(M^{\prime},w^{\prime},s^{\prime})$, with appeal to Lemma
8.

Since $M^{\prime}\neq\mathtt{fail}$, no expression in the derivation chain
(other than the last one) can be of the form $E^{\prime}[\mathtt{fail}]$.
$\Box$

###### Lemma 11

For any $E$, if $(M,w,s)\Rightarrow(\mathtt{fail},w^{\prime},s^{\prime})$ then
$(E[M],w,s)\Rightarrow(\mathtt{fail},w^{\prime},s^{\prime})$.

  * Proof.

By induction on the number of steps in the derivation, using Lemmas 8 and 10.
If $E=[\ ]$, the result holds trivially, so let us assume $E\neq[\ ]$. If
$(M,w,s)\Rightarrow(\mathtt{fail},w^{\prime},s^{\prime})$ was derived in $0$
steps, then $M=\mathtt{fail}$, $w^{\prime}=w^{\prime}$ and $s^{\prime}=s$, so
by (Red Pure), $(E[\mathtt{fail}],w,s)\rightarrow(\mathtt{fail},w,s)$, as
required.

If $(M,w,s)\Rightarrow(\mathtt{fail},w^{\prime},s^{\prime})$ was derived in
$1$ or more steps, then:

    * •

If $M=E^{\prime}[\mathtt{fail}]$ and $E^{\prime}\neq[\ ]$, then $((E\circ
E^{\prime})[\mathtt{fail}],w,s)\rightarrow(\mathtt{fail},w^{\prime},s^{\prime})$
by (Red Pure).

    * •

Otherwise, there exist $\hat{M}$, $\hat{w}$, $\hat{s}$ such that
$(M,w,s)\rightarrow(\hat{M},\hat{w},\hat{s})\Rightarrow(\mathtt{fail},w^{\prime},s^{\prime})$,
where $M\notin\mathcal{GV}$. By induction hypothesis,
$(E[\hat{M}],\hat{w},\hat{s})\Rightarrow(\mathtt{fail},w^{\prime},s^{\prime})$
for any $E$, and by Lemma 8,
$(E[M],w,s)\rightarrow(E[\hat{M}],\hat{w},\hat{s})$.

$\Box$

###### Lemma 12

If $(M,w,s)\Rightarrow(M^{\prime},w^{\prime},s^{\prime})$ and $w\geq 0$, then
$w^{\prime}\geq 0$.

  * Proof.

By induction on the number of steps in the derivation.

    * •

If $(M,w,s)\Rightarrow(M^{\prime},w^{\prime},s^{\prime})$ was derived in $0$
steps, then $w^{\prime}=w$, so $w^{\prime}\geq 0$.

    * •

If $(M,w,s)\Rightarrow(M^{\prime},w^{\prime},s^{\prime})$ was derived in $1$
or more steps, then
$(M,w,s)\rightarrow(M^{*},w^{*},s^{*})\Rightarrow(M^{\prime},w^{\prime},s^{\prime})$.

If $(M,w,s)\rightarrow(M^{*},w^{*},s^{*})$ was derived with (Red Pure), then
$w^{*}=w\geq 0$.

If $(M,w,s)\rightarrow(M^{*},w^{*},s^{*})$ was derived with (Red Random), then
$w^{*}=w\cdot w^{\prime\prime}$ for some $w^{\prime\prime}>0$, so $w^{*}\geq
0$.

If $(M,w,s)\rightarrow(M^{*},w^{*},s^{*})$ was derived with (Red Score), then
$w^{*}=w\cdot c$ for some $c>0$, so $w^{\prime}\geq 0$.

If $(M,w,s)\rightarrow(M^{*},w^{*},s^{*})$ was derived with (Red Random Fail),
then $w^{*}=0$.

In either case, $w^{*}\geq 0$, so by induction hypothesis, $w^{\prime}\geq 0$.

$\Box$

###### Lemma 13

If $(M,w,s)\rightarrow(M^{\prime},w^{\prime},s^{\prime})$ was not derived with
(Red Random Fail) and $w>0$, then $w^{\prime}>0$.

  * Proof.

By inspection (similar to the inductive step in the proof of Lemma 12).

###### Lemma 14

If $(M,w,s)\rightarrow(M^{\prime},w^{\prime},s^{\prime})$, then for any
$w^{*}\geq 0$,
$(M,ww^{*},s)\rightarrow(M^{\prime},w^{\prime}w^{*},s^{\prime})$

  * Proof.

By case analysis. $\Box$

###### Lemma 15

If $(M,w,s)\rightarrow(M^{\prime},w^{\prime},s^{\prime})$, then for any
$s^{*}$, $(M,w,s@s^{*})\rightarrow(M^{\prime},w^{\prime},s^{\prime}@s^{*})$

  * Proof.

By case analysis. $\Box$

###### Lemma 16

If $(M,w,s)\rightarrow(M^{\prime},w^{\prime},s^{\prime})$, then there is
$s^{*}$ such that $s=s^{*}@s^{\prime}$ and
$(M,w,s^{*})\rightarrow(M^{\prime},w^{\prime},[])$

  * Proof.

By case analysis. $\Box$

###### Lemma 17

If $(M,w,s)\rightarrow^{k}(M^{\prime},w^{\prime},s^{\prime})$, then for any
$w^{*}\geq 0$,
$(M,ww^{*},s)\rightarrow^{k}(M^{\prime},w^{\prime}w^{*},s^{\prime})$

  * Proof.

By induction on $k$, with appeal to Lemma 14. $\Box$

###### Lemma 18

If $(M,w,s)\rightarrow^{k}(M^{\prime},w^{\prime},s^{*})$, then for any
$s^{\prime}$,
$(M,w,s@s^{\prime})\rightarrow^{k}(M^{\prime},w^{\prime},s^{*}@s^{\prime})$

  * Proof.

By induction on $k$, with appeal to Lemma 15.

###### Lemma 19

If both $(M,1,s)\Rightarrow(M^{\prime},w^{\prime},[])$ and
$(M^{\prime},1,s^{\prime})\Rightarrow(M^{\prime\prime},w^{\prime\prime},[])$,
then $(M,1,s@s^{\prime})\Rightarrow(M^{\prime\prime},w^{\prime}\cdot
w^{\prime\prime},[])$.

  * Proof.

By Lemma 18, $(M,1,s@s^{\prime})\Rightarrow(M^{\prime},w^{\prime},s^{\prime})$
and by lemma 12, $w^{\prime}\geq 0$. Hence, by Lemma 17,
$(M^{\prime},w^{\prime},s^{\prime})\Rightarrow(M^{\prime\prime},w^{\prime}w^{\prime\prime},[])$,
which gives
$(M,1,s@s^{\prime})\Rightarrow(M^{\prime\prime},w^{\prime}w^{\prime\prime},[])$.
$\Box$

###### Lemma 20

For any $E$, $E[\mathtt{fail}]\Downarrow^{[]}_{1}\mathtt{fail}$.

  * Proof.

By induction on the structure of $E$.

    * •

Base case: $E=[\ ]$, the result follows by (Eval Val).

    * •

Induction step:

      * •

Case $E=(\lambda x.L)\ E^{\prime}$: By induction hypothesis,
$E^{\prime}[\mathtt{fail}]\Downarrow^{[]}_{1}\mathtt{fail}$, and by (Eval Appl
Raise2), $(\lambda x.L)\
E^{\prime}[\mathtt{fail}]\Downarrow^{[]}_{1}\mathtt{fail}$, as required.

      * •

Case $E=E^{\prime}\ L$: By induction hypothesis,
$E^{\prime}[\mathtt{fail}]\Downarrow^{[]}_{1}\mathtt{fail}$, so by (Eval Appl
Raise1), we get $E^{\prime}[\mathtt{fail}]\
L\Downarrow^{[]}_{1}\mathtt{fail}$.

$\Box$

###### Lemma 21

For any $E$, if $\operatorname{pdf}_{D}(\vec{c},c)=0$, then
$E[D(\vec{c})]\Downarrow^{[c]}_{0}\mathtt{fail}$.

  * Proof.

By induction on the structure of $E$.

    * •

Base case: $E=[\ ]$, the result follows by (Eval Random Fail).

    * •

Induction step:

      * •

Case $E=(\lambda x.L)\ E^{\prime}$: By induction hypothesis,
$E^{\prime}[D(\vec{c})]\Downarrow^{[c]}_{0}\mathtt{fail}$, and by (Eval Appl
Raise2), $(\lambda x.L)\
E^{\prime}[D(\vec{c})]\Downarrow^{[]}_{0}\mathtt{fail}$, as required.

      * •

Case $E=E^{\prime}\ L$: By induction hypothesis,
$E^{\prime}[D(\vec{c})]\Downarrow^{[c]}_{0}\mathtt{fail}$, so by (Eval Appl
Raise1), we get $E^{\prime}[D(\vec{c})]\ L\Downarrow^{[]}_{0}\mathtt{fail}$.

$\Box$

The following directly relates the small-step and big-step semantics, saying
that the latter is invariant on the former:

###### Lemma 22

If $(M,1,s)\rightarrow(M^{\prime},w,[])$ and
$M^{\prime}\Downarrow^{s^{\prime}}_{w^{\prime}}G$, then
$M\Downarrow^{s@s^{\prime}}_{w\cdot w^{\prime}}G$.

  * Proof.

By induction on the structure of $M$.

If $M=E[\mathtt{fail}]$ for some $E\neq[\ ]$, the result follows immediately
by Lemma 20. Now, let us assume that $M\neq E[\mathtt{fail}]$.

    * •

Base case: $M=R$:

      * •

If $M=g(\vec{c})$ or $M=c\ V$ or $M=T$, then $M$ reduces to a generalized
value in 1 step, so the result holds trivially (by one of the evaluation
rules).

      * •

Case $M=\mathtt{if}\ {\mathtt{true}}\ \mathtt{then}\ {M_{2}}\ \mathtt{else}\
{M_{3}}$: We have $(\mathtt{if}\ {\mathtt{true}}\ \mathtt{then}\ {M_{2}}\
\mathtt{else}\ {M_{3}},1,[])\rightarrow(M_{2},1,[])$. By assumption,
$M_{2}\Downarrow^{s^{\prime}}_{w^{\prime}}G$. Thus, the desired result holds
by (Eval If True).

      * •

Case $M=\mathtt{if}\ {\mathtt{false}}\ \mathtt{then}\ {M_{2}}\ \mathtt{else}\
{M_{3}}$: analogous to the previous case.

      * •

Case $M=(\lambda x.N_{1})\ V$: We have $((\lambda x.N_{1})\
V,1,[])\rightarrow(N_{1}\\{V/x\\},1,[])$. Since $(\lambda x.N_{1})$ and $V$
are already values and $N_{1}\\{V/x\\}\Downarrow^{s^{\prime}}_{w^{\prime}}G$
by assumption, (Eval Appl) yields $(\lambda x.N_{1})\
V\Downarrow^{s^{\prime}}_{w^{\prime}}G$.

      * •

Case $M=\mathsf{D}(\vec{c})$: $(M,1,s)\rightarrow(M^{\prime},w,[])$ must have
been derived with (Red Random) or (Red Random Fail). In the former case,
$s=[c]$, $M^{\prime}=c$, and $w=\operatorname{pdf}_{D}(\vec{c},c)$, where
$c>0$. The second assumption then takes the form $c\Downarrow^{[]}_{1}c$, so
the required result follows from (Eval Random). The (Red Random Fail) case is
similar, with the result following from (Eval Random Fail).

      * •

Case $M=\mathtt{score}(c)$, $c\in(0,1]$: $(M,1,s)\rightarrow(M^{\prime},w,[])$
must have been derived with (Red Score).so $M^{\prime}=\mathtt{true}$, $w=c$
and $s=[]$. Thus, the result then follows from (Eval Score).

    * •

Induction step: $M=E[R]$, $E\neq[\ ]$, $R\neq\mathtt{fail}$:

      * •

Case $E=(\lambda x.L)\ E^{\prime}$: $M=(\lambda x.L)\ E^{\prime}[R]$.

We have $((\lambda x.L)\ E^{\prime}[R],1,s)\rightarrow((\lambda x.L)\
E^{\prime}[N],w,[])$ for some $N$, so by lemmas 8 and 9,
$(E^{\prime}[R],1,s)\rightarrow(E^{\prime}[N],w,[])$. By assumption, $(\lambda
x.L)\ E^{\prime}[N]\Downarrow^{s^{\prime}}_{w^{\prime}}G$.

        * •

If $(\lambda x.L)\ E^{\prime}[N]\Downarrow^{s^{\prime}}_{w^{\prime}}G$ was
derived with (Eval Appl), then $E^{\prime}[N]\Downarrow^{s_{1}}_{w_{1}}V$ and
$(\lambda x.L)\ V\Downarrow^{s_{2}}_{w_{2}}G$, where $w^{\prime}=w_{1}w_{2}$
and $s^{\prime}=s_{1}@s_{2}$. By induction hypothesis,
$E^{\prime}[R]\Downarrow^{s@s_{1}}_{ww_{1}}V$, so (Eval Appl) gives $(\lambda
x.L)\ E^{\prime}[R]\Downarrow^{s@s^{\prime}}_{ww^{\prime}}G$, as required.

        * •

If $(\lambda x.L)\ E^{\prime}[N]\Downarrow^{s^{\prime}}_{w^{\prime}}G$ was
derived with (Eval Appl Raise3), then $G=\mathtt{fail}$ and
$E^{\prime}[N]\Downarrow^{s^{\prime}}_{w^{\prime}}\mathtt{fail}$. By induction
hypothesis,
$E^{\prime}[R]\Downarrow^{s@s^{\prime}}_{ww^{\prime}}\mathtt{fail}$, so by
(Eval Appl Raise3), $(\lambda x.L)\
E^{\prime}[R]\Downarrow^{s@s^{\prime}}_{ww^{\prime}}\mathtt{fail}$

      * •

Case $E=E^{\prime}\ L$: $M=E^{\prime}[M^{*}]\ L$:

We have $(E^{\prime}[R]\ L,1,s)\rightarrow(E^{\prime}[N]\ L,w,[])$ for some
$N$, so by lemmas 8 and 9,
$(E^{\prime}[R],1,s)\rightarrow(E^{\prime}[N],w,[])$. By assumption,
$E^{\prime}[N]\ L\Downarrow^{s^{\prime}}_{w^{\prime}}G$.

        * •

If $E^{\prime}[N]\ L\Downarrow^{s^{\prime}}_{w^{\prime}}G$ was derived with
(Eval Appl), then $E^{\prime}[N]\Downarrow^{w_{1}}_{s_{1}}(\lambda
x.N^{\prime})$, $L~{}\Downarrow^{w_{2}}_{s_{2}}~{}V$ and
$N^{\prime}[V/x]\Downarrow^{w_{3}}_{s_{3}}G$, where
$w^{\prime}=w_{1}w_{2}w_{3}$ and $s^{\prime}=s_{1}@s_{2}@s_{3}$. By induction
hypothesis, $E^{\prime}[R]\Downarrow^{s@s_{1}}_{ww_{1}}(\lambda
x.N^{\prime})$, so (Eval Appl) gives $E^{\prime}[R]\
L\Downarrow^{s@s^{\prime}}_{ww^{\prime}}G$, as required.

        * •

If $E^{\prime}[N]\ L\Downarrow^{s^{\prime}}_{w^{\prime}}G$ was derived with
(Eval Appl Raise1), then $G=\mathtt{fail}$ and
$E^{\prime}[N]\Downarrow^{s^{\prime}}_{w^{\prime}}\mathtt{fail}$. By induction
hypothesis,
$E^{\prime}[R]\Downarrow^{s@s^{\prime}}_{ww^{\prime}}\mathtt{fail}$, so by
(Eval Appl Raise1), $E^{\prime}[R]\
L\Downarrow^{s@s^{\prime}}_{ww^{\prime}}\mathtt{fail}$

        * •

If $E^{\prime}[N]\ L\Downarrow^{s^{\prime}}_{w^{\prime}}G$ was derived with
(Eval Appl Raise3), then $E^{\prime}[N]\Downarrow^{s_{1}}_{w_{1}}(\lambda
x.N^{\prime})$ and $L\Downarrow^{s_{2}}_{w_{2}}\mathtt{fail}$, where
$w^{\prime}=w_{1}w_{2}$ and $s^{\prime}=s_{1}@s_{2}$. By induction hypothesis,
$E^{\prime}[R]\Downarrow^{s@s_{1}}_{ww_{1}}(\lambda x.N^{\prime})$, so (Eval
Appl Raise3) gives $E^{\prime}[R]\
L\Downarrow^{s@s^{\prime}}_{ww^{\prime}}\mathtt{fail}$, as required.

        * •

If $E^{\prime}[N]\ L\Downarrow^{s^{\prime}}_{w^{\prime}}G$ was derived with
(Eval Appl Raise1), then $G=\mathtt{fail}$ and
$N_{1}^{\prime}\Downarrow^{s^{\prime}}_{w^{\prime}}c$. By induction
hypothesis, $E^{\prime}[R]\Downarrow^{s@s^{\prime}}_{ww^{\prime}}c$, so by
(Eval Appl Raise1), $E^{\prime}[R]\
L\Downarrow^{s@s^{\prime}}_{ww^{\prime}}\mathtt{fail}$.

$\Box$

Finally, we have all the ingredients to show that the small-step and the big-
step sampling-based semantics both compute the same traces with the same
weights.

###### Theorem 1

$M\Downarrow^{s}_{w}G$ if and only if $(M,1,s)\Rightarrow(G,w,[])$.

  * Proof.

The left to right implication is an induction on the derivation of
$M\Downarrow^{s}_{w}G$. The most interesting case is definitely the following:

$\begin{array}[b]{@{}l@{}}\mbox{({Eval Appl})}\\\
\begin{array}[]{@{}l@{}}M\Downarrow^{s_{1}}_{w_{1}}\lambda x.M^{\prime}\qquad
N\Downarrow^{s_{2}}_{w_{2}}V\qquad
M^{\prime}[V/x]\Downarrow^{s_{3}}_{w_{3}}G\\\
\hline\cr\raisebox{0.0pt}[10.76385pt]{}M\
N\Downarrow^{s_{1}@s_{2}@s_{3}}_{w_{1}\cdot w_{2}\cdot
w_{3}}G\end{array}\end{array}$

By induction hypothesis, $(M,1,s_{1})\Rightarrow(\lambda
x.M^{\prime},w_{1},[])$, $(N,1,s_{2})\Rightarrow(V,w_{2},[])$ and
$(M^{\prime}[V/x],1,s_{3})\Rightarrow(G,w_{3},[])$. By Lemma 10 (for $E=[\ ]\
N$), $(M\ N,1,s_{1})\Rightarrow((\lambda x.M^{\prime})\ N,w_{1},[])$. By Lemma
10 again (for $E=(\lambda x.M^{\prime})\ [\ ]$), $((\lambda x.M^{\prime})\
N,1,s_{2})\Rightarrow((\lambda x.M^{\prime})\ V,w_{2},[])$. By Lemma 19, $(M\
N,1,s_{1}@s_{2})\Rightarrow((\lambda x.M^{\prime})\ V,w_{1}w_{2},[])$ By (Red
Pure), $((\lambda x.M^{\prime})\ V,w_{1}\cdot
w_{2},[])\rightarrow(M^{\prime}[V/x],w_{1}\cdot w_{2},[])$, which implies $(M\
N,1,s_{1}@s_{2})\Rightarrow((\lambda x.M^{\prime})\ V,w_{1}w_{2},[])$ Thus,
the desired result follows by Lemma 19.

    * •

Case: $\begin{array}[b]{@{}l@{}}\mbox{({Eval Val})}\\\
\begin{array}[]{@{}l@{}}G\in\mathcal{GV}\\\
\hline\cr\raisebox{0.0pt}[10.76385pt]{}G\Downarrow^{[]}_{1}G\end{array}\end{array}$

Here, $M=V$, $w=1$ and $s=[]$. so $(M,w_{0},s_{0})$ reduces to
$(V,w_{0},s_{0})$ in 0 steps by the small-step semantics.

    * •

Case: $\begin{array}[b]{@{}l@{}}\mbox{({Eval Random})}\\\
\begin{array}[]{@{}l@{}}w=\operatorname{pdf}_{\mathsf{D}}(\vec{c},c)\\\ w>0\\\
\hline\cr\raisebox{0.0pt}[10.76385pt]{}\mathsf{D}(\vec{c})\Downarrow^{[c]}_{w}c\end{array}\end{array}$

By (Red Random) (taking $E=[\ ]$),
$(\mathsf{D}(\vec{c}),1,[c])\rightarrow(c,w,[])$.

    * •

Case: $\begin{array}[b]{@{}l@{}}\mbox{({Eval Random Fail})}\\\
\begin{array}[]{@{}l@{}}\operatorname{pdf}_{\mathsf{D}}(\vec{c},c)=0\\\
\hline\cr\raisebox{0.0pt}[10.76385pt]{}\mathsf{D}(\vec{c})\Downarrow^{[c]}_{0}\mathtt{fail}\end{array}\end{array}$

By (Red Random Fail) (taking $E=[\ ]$),
$(\mathsf{D}(\vec{c}),1,[c])\rightarrow(\mathtt{fail},0,[])$.

    * •

Case: $\begin{array}[b]{@{}l@{}}\mbox{({Eval Prim})}\\\
\begin{array}[]{@{}l@{}}\\\
\hline\cr\raisebox{0.0pt}[10.76385pt]{}g(\vec{c})\Downarrow^{[]}_{1}\sigma_{g}(\vec{c})\end{array}\end{array}$

By (Red Pure) (taking $E=[\ ]$),
$(g(\vec{c}),1,[])\rightarrow(\sigma_{g}(\vec{c}),1,[])$.

    * •

Case: $\begin{array}[b]{@{}l@{}}\mbox{({Eval Score})}\\\
\begin{array}[]{@{}l@{}}c\in(0,1]\\\
\hline\cr\raisebox{0.0pt}[10.76385pt]{}\mathtt{score}(c)\Downarrow^{[]}_{c}\mathtt{true}\end{array}\end{array}$

By (Red Score) (taking $E=[\ ]$),
$(\mathsf{D}(\vec{c}),1,[])\rightarrow(c,w,[])$.

    * •

Case: $\begin{array}[b]{@{}l@{}}\mbox{({Eval Appl})}\\\
\begin{array}[]{@{}l@{}}M\Downarrow^{s_{1}}_{w_{1}}\lambda x.M^{\prime}\\\
N\Downarrow^{s_{2}}_{w_{2}}V\\\ M^{\prime}[V/x]\Downarrow^{s_{3}}_{w_{3}}G\\\
\hline\cr\raisebox{0.0pt}[10.76385pt]{}M\
N\Downarrow^{s_{1}@s_{2}@s_{3}}_{w_{1}\cdot w_{2}\cdot
w_{3}}G\end{array}\end{array}$

By induction hypothesis, $(M,1,s_{1})\Rightarrow(\lambda
x.M^{\prime},w_{1},[])$, $(N,1,s_{2})\Rightarrow(V,w_{2},[])$ and
$(M^{\prime}[V/x],1,s_{3})\Rightarrow(G,w_{3},[])$.

By Lemma 10 (for $E=[\ ]\ N$), $(M\ N,1,s_{1})\Rightarrow((\lambda
x.M^{\prime})\ N,w_{1},[])$.

By Lemma 10 again (for $E=(\lambda x.M^{\prime})\ [\ ]$), $((\lambda
x.M^{\prime})\ N,1,s_{2})\Rightarrow((\lambda x.M^{\prime})\ V,w_{2},[])$.

By Lemma 19, $(M\ N,1,s_{1}@s_{2})\Rightarrow((\lambda x.M^{\prime})\
V,w_{1}w_{2},[])$

By (Red Pure), $((\lambda x.M^{\prime})\ V,w_{1}\cdot
w_{2},[])\rightarrow(M^{\prime}[V/x],w_{1}\cdot w_{2},[])$, which implies $(M\
N,1,s_{1}@s_{2})\Rightarrow((\lambda x.M^{\prime})\ V,w_{1}w_{2},[])$

Thus, the desired result follows by Lemma 19.

    * •

Case: $\begin{array}[b]{@{}l@{}}\mbox{({Eval Appl Raise1})}\\\
\begin{array}[]{@{}l@{}}M\Downarrow^{s}_{w}\mathtt{fail}\\\
\hline\cr\raisebox{0.0pt}[10.76385pt]{}M\
N\Downarrow^{s}_{w}\mathtt{fail}\end{array}\end{array}$

By induction hypothesis, $(M,1,s)\Rightarrow(\mathtt{fail},w,[])$.

By Lemma 11 (with $E=[\ ]\ N)$), $(M\ N,1,s)\Rightarrow(\mathtt{fail},w,[])$.

    * •

Case: $\begin{array}[b]{@{}l@{}}\mbox{({Eval Appl Raise2})}\\\
\begin{array}[]{@{}l@{}}M\Downarrow^{s}_{w}c\\\
\hline\cr\raisebox{0.0pt}[10.76385pt]{}M\
N\Downarrow^{s}_{w}\mathtt{fail}\end{array}\end{array}$

By induction hypothesis, $(M,1,s)\Rightarrow(c,w,[])$. By Lemma 10 (with $E=[\
]\ N)$), $(M\ N,1,s)\Rightarrow(c\ N,w,[])$.

By (Red Pure), $(c\ N,w,[])\rightarrow(\mathtt{fail},w,[])$.

Thus, $(M\ N,1,s)\Rightarrow(\mathtt{fail},w,[])$.

    * •

Case: $\begin{array}[b]{@{}l@{}}\mbox{({Eval Appl Raise3})}\\\
\begin{array}[]{@{}l@{}}M\Downarrow^{s_{1}}_{w_{1}}\lambda x.M^{\prime}\\\
N\Downarrow^{s_{2}}_{w_{2}}\mathtt{fail}\\\
\hline\cr\raisebox{0.0pt}[10.76385pt]{}M\
N\Downarrow^{s_{1}@s_{2}}_{w_{1}\cdot
w_{2}}\mathtt{fail}\end{array}\end{array}$

By induction hypothesis, $(M,1,s_{1})\Rightarrow(\lambda
x.M^{\prime},w_{1},[])$, and $(N,1,s_{2})\Rightarrow(\mathtt{fail},w_{2},[])$.

By Lemma 10, $(M\ N,1,s_{1})\Rightarrow((\lambda x.M^{\prime})\ N,w_{1},[])$.

By Lemma 11, $((\lambda x.M^{\prime})\
N,1,s_{2})\Rightarrow(\mathtt{fail},w_{2},[])$.

Thus, by Lemma 19, $(M\ N,1,s_{1}@s_{2})\Rightarrow(\mathtt{fail},w_{1}\cdot
w_{2},[])$.

    * •

Case: $\begin{array}[b]{@{}l@{}}\mbox{({Eval If True})}\\\
\begin{array}[]{@{}l@{}}M_{2}\Downarrow^{s}_{w}G\\\
\hline\cr\raisebox{0.0pt}[10.76385pt]{}\mathtt{if}\ {\mathtt{true}}\
\mathtt{then}\ {M_{2}}\ \mathtt{else}\
{M_{3}}\Downarrow^{s}_{w}G\end{array}\end{array}$

By (Red Pure) (taking $E=[\ ]$), $(\mathtt{if}\ {\mathtt{true}}\
\mathtt{then}\ {M_{2}}\ \mathtt{else}\ {M_{3}},1,s)\rightarrow(M_{2},1,s)$. By
induction hypothesis, $(M_{2},1,s)\Rightarrow(G,w,[])$.

Hence $(\mathtt{if}\ {1}\ \mathtt{then}\ {M_{2}}\ \mathtt{else}\
{M_{3}},1,s)\Rightarrow(G,w,[])$

    * •

Case (Eval If False): analogous to (Eval If True)

    * •

Case: $\begin{array}[b]{@{}l@{}}\mbox{({Eval Fail})}\\\
\begin{array}[]{@{}l@{}}\\\
\hline\cr\raisebox{0.0pt}[10.76385pt]{}T\Downarrow^{[]}_{1}\mathtt{fail}\end{array}\end{array}$

By (Red Pure), $(T,1,[])\rightarrow(\mathtt{fail},1,[])$.

The right to left implication can be proved by an induction on the length of
the derivation of $(M,1,s)\Rightarrow(G,w,[])$.

    * •

Base case: If $(M,1,s)=(G,w,[])$, then $M\Downarrow^{w}_{s}G$ by (Eval Val).

    * •

Induction step: assume
$(M,1,s)\rightarrow(M^{\prime},w^{\prime},s^{\prime})\rightarrow^{n}(G,w,[])$.
If $(M,1,s)\rightarrow(M^{\prime},w^{\prime},s^{\prime})$ was derived with
(Red Random Fail), then $M=E[D(\vec{c})]$, $n=1$, $s=[c]$, $G=\mathtt{fail}$
and $w=w^{\prime}=\operatorname{pdf}_{D}(\vec{c},c)=0$. By Lemma 21, we have
$M\Downarrow^{[}c]_{0}\mathtt{fail}$, as required.

Otherwise, by Lemma 13, $w^{\prime}>0$, so by Lemma 17,
$(M^{\prime},1,s^{\prime})\rightarrow^{n}(G,w/w^{\prime},[])$. By induction
hypothesis, $M^{\prime}\Downarrow^{s^{\prime}}_{w/w^{\prime}}G$. By Lemma 16,
$(M,1,s^{*})\rightarrow(M^{\prime},w^{\prime},[])$, where
$s=s^{*}@s^{\prime}$.

Therefore, by Lemma 22, $M\Downarrow^{s^{*}@s^{\prime}}_{w}G$, and so
$M\Downarrow^{s}_{w}G$. $\Box$

As a corollary of Theorem 1 and Lemma 7 we obtain:

###### Lemma 23

If $M\Downarrow^{s}_{w}G$ and $M\Downarrow^{s}_{w^{\prime}}G^{\prime}$ then
$w=w^{\prime}$ and $G=G^{\prime}$.

At this point, we have defined intuitive operational semantics based on the
consumption of an explicit trace of randomness, but we have defined no
distributions. In the rest of this section we show that this semantics indeed
associates a sub-probability distribution with each term. Before proceeding,
however, we need some measure theory.

###  3.2 Some Measure-Theoretic Preliminaries.

We begin by recapitulating some standard definitions for sub-probability
distributions and kernels over metric spaces. For a more complete, tutorial-
style introduction to measure theory, see Billingsley [2], Panangaden [29], or
another standard textbook or lecture notes.

A $\sigma$-algebra (over a set $X$) is a set $\Sigma$ of subsets of $X$ that
contains $\varnothing$, and is closed under complement and countable union
(and hence is closed under countable intersection). Let the $\sigma$-algebra
_generated_ by $S$, written $\sigma(S)$, be the set $\sigma(S)$
$S\subseteq\mathcal{P}(X)$, that is the least $\sigma$-algebra over $\cup S$
that is a superset of $S$. In other words, $\sigma(S)$ is the least set such
that:

  1. 1.

we have $S\subseteq\sigma(S)$ and $\varnothing\in\sigma(S)$; and

  2. 2.

$((\cup S)\setminus A)\in\sigma(S)$ if $A\in\sigma(S)$; and

  3. 3.

$\cup_{i\in\mathbb{N}}A_{i}\in\sigma(S)$ if each $A_{i}\in\sigma(S)$.

An equivalent definition is that
$\sigma(S)\mathrel{\smash[t]{\triangleq}}\bigcap\\{\Sigma\mid\mbox{$S\subseteq\Sigma$
and $\Sigma$ is a $\sigma$-algebra}\\}$.

We write $\mathbb{R}_{+}$ for $[0,\infty]$ and $\mathbb{R}_{[0,1]}$ for the
interval $[0,1]$. A _metric space_ is a set $X$ with a symmetric _distance
function_ $\delta:X\times X\to\mathbb{R}_{+}$ that satisfies the triangle
inequality $\delta(x,z)\leq\delta(x,y)+\delta(y,z)$ and the axiom
$\delta(x,x)=0$. We write
$\mathbf{B}(x,r)\mathrel{\smash[t]{\triangleq}}\\{y\mid\delta(x,y)<r\\}$ for
the open ball around $x$ of radius $r$. We equip $\mathbb{R}_{+}$ and
$\mathbb{R}_{[0,1]}$ with the standard metric $\delta(x,y)=\lvert{x-y}\rvert$,
and products of metric spaces with the Manhattan metric (e.g.,
$\delta((x_{1},x_{2}),(y_{1},y_{2}))=\delta(x_{1},y_{1})+\delta(x_{2},y_{2})$).
The _Borel_ $\sigma$-_algebra_ on a metric space $(X,\delta)$ is
$\mathcal{B}(X,\delta)\mathrel{\smash[t]{\triangleq}}\sigma(\\{\mathbf{B}(x,r)\mid
x\in X\land r>0\\})$. We often omit the arguments to $\mathcal{B}$ when they
are clear from the context.

A _measurable space_ is a pair $(X,\Sigma)$ where $X$ is a set of possible
outcomes, and $\Sigma\subseteq\mathcal{P}(X)$ is a $\sigma$-algebra of
_measurable sets_. As an example, consider the extended positive real numbers
$\mathbb{R}_{+}$ equipped with the Borel $\sigma$-algebra $\mathcal{R}$, i.e.
the set $\sigma(\\{(a,b)\mid a,b\geq 0\\})$ which is the smallest
$\sigma$-algebra containing all open (and closed) intervals. We can create
finite products of measurable spaces by iterating the construction
$(X,\Sigma)\times(X^{\prime},\Sigma^{\prime})=(X\times
X^{\prime},\sigma(A\times B\mid A\in\Sigma\land B\in\Sigma^{\prime}))$. If
$(X,\Sigma)$ and $(X^{\prime},\Sigma^{\prime})$ are measurable spaces, then
the function $f:X\to X^{\prime}$ is _measurable_ if and only if for all
$A\in\Sigma^{\prime}$, $f^{-1}(A)\in\Sigma$, where the _inverse image_
$f^{-1}:\mathcal{P}(X^{\prime})\to\mathcal{P}(X)$ is given by
$f^{-1}(A)\mathrel{\smash[t]{\triangleq}}\\{x\in X\mid f(x)\in A\\}$.

A _measure_ $\mu$ on $(X,\Sigma)$ is a function from $\Sigma$ to
$\mathbb{R}_{+}$, that is (1) zero on the empty set, that is,
$\mu(\varnothing)=0$, and (2) countably additive, that is,
$\mu(\cup_{i}A_{i})=\Sigma_{i}\mu(A_{i})$ if $A_{1},A_{2},\dots$ are pair-wise
disjoint. The measure $\mu$ is called a _(sub-probability) distribution_ if
$\mu(X)\leq 1$ and _finite_ if $\mu(X)\neq\infty$. If $\mu,\nu$ are finite
measures and $c\geq 0$, we write $c\cdot\mu$ for the finite measure $A\mapsto
c\cdot(\mu(A))$ and $\mu+\nu$ for the finite measure $A\mapsto\mu(A)+\nu(A)$.
We write $\mathbf{0}$ for the zero measure $A\mapsto 0$. For any element $x$
of $X$, the Dirac measure $\delta(x)$ is defined as follows:

$\delta(x)(A)=\left\\{\begin{array}[]{ll}1&\mbox{if $x\in A$;}\\\
0&\mbox{otherwise.}\end{array}\right.$

A _measure space_ is a triple $\mathscr{M}=(X,\Sigma,\mu)$ where $\mu$ is a
measure on the measurable space $(X,\Sigma)$. Given a measurable function
$f:X\to\mathbb{R}_{+}$, the _integral_ of $f$ over $\mathscr{M}$ can be
defined following Lebesgue’s theory and denoted as either of

$\int\\!f\;d\mu=\int\\!f(x)\;\mu(dx)\in\mathbb{R}_{+}.$

The Iverson brackets $[P]$ are 1 if predicate $P$ is true, and 0 otherwise. We
then write

$\int_{A}f\;d\mu\mathrel{\smash[t]{\triangleq}}\int\\!f(x)\cdot{[{x}\in{A}]}\,\mu(dx).$

We equip some measurable spaces $(X,\Sigma)$ with a _stock measure_ $\mu$. We
then write $\int\\!f(s)\,ds$ (or shorter, $\int\\!f$) for $\int\\!f\,d\mu$
when $f$ is measurable $f:X\to\mathbb{R}_{+}$. In particular, we let the stock
measure on $(\mathbb{R}^{n},\mathcal{B})$ be the Lebesgue measure
$\lambda_{n}$.

A function $f$ is a _density_ of a measure $\nu$ (with respect to the measure
$\mu$) if $\nu(A)=\int_{A}f\,d\mu$ for all measurable $A$.

Given a measurable set $A$ from $(X,\Sigma)$, we write ${\Sigma}\rvert_{A}$
for the _restriction_ of $\Sigma$ to elements _in_ $A$, i.e.,
${\Sigma}\rvert_{A}=\\{B\cap A\mid B\in\Sigma\\}$. Then
$(A,{\Sigma}\rvert_{A})$ is a measurable space. Any distribution $\mu$ on
$(X,\Sigma)$ trivially yields a distribution ${\mu}\rvert_{A}$ on
$(A,{\Sigma}\rvert_{A})$ by ${\mu}\rvert_{A}(B)=\mu(B)$.

###  3.3 Measure Space of Program Traces

In this section, we construct a measure space on the set $\mathbb{S}$ of
program traces: (1) we define a measurable space $(\mathbb{S},{\cal S})$ and
(2) we equip it with a stock measure $\mu$ to obtain our measure space
$(\mathbb{S},{\cal S},\mu)$.

#### The Measurable Space of Program Traces

To define the semantics of a program as a measure on the space of random
choices, we first need to define a measurable space of program traces. Since a
program trace is a sequence of real numbers of an arbitrary length (possibly
0), the set of all program traces is
$\mathbb{S}=\biguplus_{n\in\mathbb{N}}\mathbb{R}^{n}$. Now, let us define the
$\sigma$-algebra $\mathcal{S}$ on $\mathbb{S}$ as follows: let
$\mathcal{B}_{n}$ be the Borel $\sigma$-algebra on $\mathbb{R}^{n}$ (we take
$\mathcal{B}_{0}$ to be $\\{\\{[]\\},\\{\\}\\}$). Consider the class of sets
$\mathcal{S}$ of the form:

$A=\biguplus_{n\in\mathbb{N}}H_{n}$

where $H_{n}\in\mathcal{B}_{n}$ for all $n$. Then $\mathcal{S}$ is a
$\sigma$-algebra, and so $(\mathbb{S},\mathcal{S})$ is a measurable space.

###### Lemma 24

$\mathcal{S}$ is a $\sigma$-algebra on $\mathbb{S}$.

  * Proof.

We have $\mathbb{S}=\biguplus_{n\in\mathbb{N}}\mathbb{R}^{n}$ and
$\mathbb{R}^{n}\in\mathcal{R}^{n}$ for all $n$, so $\mathbb{S}\in\mathcal{S}$.

If $A$ is defined as above, then
$\mathbb{S}-A=\biguplus_{n\in\mathbb{N}}(\mathbb{R}^{n}-H_{n})$, where
$\mathbb{R}^{n}-H_{n}\in\mathcal{R}^{n}$ for all $n$, so
$\mathbb{S}-A\in\mathcal{S}$.

For closure under countable union, take
$A_{i}=\biguplus_{n\in\mathbb{N}}H_{in}$ for all $i\in\mathbb{N}$, where
$H_{in}\in\mathcal{R}^{n}$ for all $i$, $n$. Then
$\bigcup_{i\in\mathbb{N}}A_{i}=\bigcup_{i\in\mathbb{N}}\biguplus_{n\in\mathbb{N}}H_{in}=\biguplus_{n\in\mathbb{N}}(\bigcup_{i\in\mathbb{N}}H_{in})\in\mathcal{S}$,
because $\bigcup_{i\in\mathbb{N}}H_{in}\in\mathcal{R}^{n}$.

Thus, $\mathcal{S}$ is a $\sigma$-algebra on $E$. $\Box$

#### Stock Measure on Program Traces

Since each primitive distribution $\mathsf{D}$ has a density, the probability
of each random value (and thus of each trace of random values) is zero.
Instead, we define the trace and transition probabilities in terms of
densities, with respect to the stock measure $\mu$ on
$(\mathbb{S},\mathcal{S})$ defined as follows:

$\mu\left(\biguplus_{n\in\mathbb{N}}H_{n}\right)=\sum_{n\in\mathbb{N}}\lambda_{n}(H_{n})$

where $\lambda_{0}=\delta({[]})$ and $\lambda_{n}$ is the Lebesgue measure on
$\mathbb{R}^{n}$ for $n>0$.

###### Lemma 25

$\mu$ is a measure on $(\mathbb{S},\mathcal{S})$.

  * Proof.

We check the three properties:

    1. 1.

Since for all $n\in\mathbb{N}$ and $H_{n}\in\mathcal{R}^{n}$, we have
$\lambda_{n}(H_{n})\in[0,\infty]$, obviously
$\mu(\biguplus_{n\in\mathbb{N}}H_{n})=\sum_{n=1}^{\infty}\lambda_{n}(H_{n})\in[0,\infty]$

    2. 2.

If $H=\biguplus_{n\in\mathbb{N}}H_{n}=\varnothing$, then $H_{n}=\varnothing$
for all $n$, so $\mu(H)=\sum_{n=1}^{\infty}\lambda_{n}(\varnothing)=0$.

    3. 3.

Countable additivity: if
$H_{1}=\biguplus_{n\in\mathbb{N}}H_{1n},H_{2}=\biguplus_{n\in\mathbb{N}}H_{2n},\dots$
is a sequence of disjoint sets in $\mathcal{S}$, then:

$\displaystyle\mu(\biguplus_{m=1}^{\infty}H_{m})$ $\displaystyle=$
$\displaystyle\mu(\biguplus_{m=1}^{\infty}\biguplus_{n=0}^{\infty}H_{mn})$
$\displaystyle=$
$\displaystyle\mu(\biguplus_{n=0}^{\infty}\biguplus_{m=1}^{\infty}H_{mn})$
$\displaystyle=$
$\displaystyle\sum_{n=0}^{\infty}\lambda_{n}(\biguplus_{m=1}^{\infty}H_{mn})$
$\displaystyle=$
$\displaystyle\sum_{n=0}^{\infty}\sum_{m=1}^{\infty}\lambda_{n}(H_{mn})$
$\displaystyle=$
$\displaystyle\sum_{m=1}^{\infty}\sum_{n=0}^{\infty}\lambda_{n}(H_{mn})$
$\displaystyle=$ $\displaystyle\sum_{m=1}^{\infty}\mu(H_{m})$

where the equality
$\sum_{n=0}^{\infty}\sum_{m=1}^{\infty}\lambda_{n}(H_{mn})=\sum_{m=1}^{\infty}\sum_{n=0}^{\infty}\lambda_{n}(H_{mn})$
follows from Tonelli’s theorem for series (see [36]).

$\Box$

A measure $\mu$ on $(X,\Sigma)$ is $\sigma$-finite if $X=\bigcup_{i}A_{i}$ for
some countable (finite or infinite) sequence of sets $A_{i}\in\Sigma$ such
that $\mu(A_{i})<\infty$. If $\mu$ is a $\sigma$-finite measure on
$(X,\Sigma)$, the measure space $(X,\Sigma,\mu)$ is also called
$\sigma$-finite. $\sigma$-finite measure spaces behave better with respect to
integration than those who are not.

In the following, let $[a,b]^{n}=\\{(x_{1},\dots,x_{n})\ |\
x_{i}\in[a,b]\quad\forall i\in 1..n\\}$.

###### Lemma 26

The measure $\mu$ on $(\mathbb{S},\mathcal{S})$ is $\sigma$-finite.

  * Proof.

For every $n\in\mathbb{N}$, we have that
$\mathbb{R}^{n}=\bigcup_{k\in\mathbb{N}}[-k,k]^{n}$. Hence,
$\mathbb{S}=\biguplus_{n\in\mathbb{N}}\mathbb{R}^{n}=\biguplus_{n\in\mathbb{N}}\bigcup_{k\in\mathbb{N}}[-k,k]^{n}$
is a countable union of sets in $\mathcal{S}$ of the form $[-k,k]^{n}$.
Finally, for all $k,n\in\mathbb{N}$ we have
$\mu([-k,k]^{n})=\lambda_{n}([-k,k]^{n})=(2k)^{n}<\infty$. $\Box$

It follows that $(\mathbb{S},\mathcal{S},\mu)$ is a $\sigma$-finite measure
space.

#### Discrete Random Variables

We have taken the sample space to be the real numbers, but any complete
separable metric space will do. For example, in order to add discrete
distributions to the language we can change $\mathbb{S}$ to
$\biguplus_{n\in\mathbb{N}}(\mathbb{R}\uplus\mathbb{N})^{n}$. The measurable
sets $H_{n}$ become $(\mathcal{R}\uplus\mathcal{P}(\mathbb{N}))^{n}$. The
stock measure $\mu$ would become
$\sum_{n=0}^{\infty}(\lambda,\mu_{\\#})^{n}(H_{n})$, where $\mu_{\\#}$ is the
counting measure on $\mathbb{N}$ (that is, $\mu_{\\#}(A)=|A|$ if $A$ is
finite, otherwise $\mu_{\\#}(A)=\infty$).

Discrete distributions have probability mass functions, that is, densities
with respect to the counting measure on $\mathbb{N}$, which are trivially
zero-extended to densities with respect to $\mu$. Given a measurable injection
function $\lceil{\cdot}\rceil:\mathbb{R}\uplus\mathbb{N}\to\mathcal{V}$ (e.g.,
mapping natural numbers to the corresponding reals, or to Church numerals), it
is easy to update the different semantics to a more general sample space,
e.g.,

$w=\operatorname{pdf}_{\mathsf{D}}(\vec{c},z)$ $w>0$
$\mathsf{D}(\vec{c})\Downarrow^{[z]}_{w}\lceil{z}\rceil$ (Eval Random)

###  3.4 Distributions $\langle\\!\langle M\rangle\\!\rangle$ and $\llbracket
M\rrbracket_{\mathbb{S}}$ Given by Sampling-Based Semantics

The result of a closed term $M$ on a given trace is

$\displaystyle\mathbf{O}_{M}(s)$
$\displaystyle=\left\\{\begin{array}[]{ll}G&\mbox{if $M\Downarrow^{s}_{w}G$
for some $w\in\mathbb{R}_{+}$}\\\
\mathtt{fail}&\mbox{otherwise.}\end{array}\right.$

The density of termination of a closed term $M$ on a given trace is defined as
follows.

$\displaystyle\mathbf{P}_{\\!M}(s)$
$\displaystyle=\left\\{\begin{array}[]{ll}w&\mbox{if $M\Downarrow^{s}_{w}G$
for some $G\in\mathcal{GV}$}\\\ 0&\mbox{otherwise}\end{array}\right.$

This density function induces a distribution $\langle\\!\langle
M\rangle\\!\rangle$ on traces defined as $\langle\\!\langle
M\rangle\\!\rangle(A):=\int_{A}\mathbf{P}_{M}$.

By inverting the result function $\mathbf{O}_{M}$, we also obtain a
distribution $\llbracket M\rrbracket_{\mathbb{S}}$ over generalised values
(also called a _result distribution_). It can be computed by integrating the
density of termination over all traces that yield the generalised values of
interest.

$\llbracket M\rrbracket_{\mathbb{S}}(A):=\langle\\!\langle
M\rangle\\!\rangle(\mathbf{O}^{-1}_{M}(A))=\int\mathbf{P}_{\\!M}(s)\cdot{[{\mathbf{O}_{M}(s)}\in{A}]}\,ds.$

As an example, for the geometric distribution example of Section 2.4 we have
$\mathbf{O}_{\mathit{geometric}\ 0.5}(s)=n$ if $s\in[0.5,1]^{n}[0,0.5)$, and
otherwise $\mathbf{O}_{\mathit{geometric}\ 0.5}(s)=\mathtt{fail}$. Similarly,
we have $\mathbf{P}_{\\!\mathit{geometric}\ 0.5}(s)=1$ if
$s\in[0.5,1]^{n}[0,0.5)$ for some $n$, and otherwise $0$. We then obtain

$\displaystyle\langle\\!\langle\mathit{geometric}\ 0.5\rangle\\!\rangle(A)={}$
$\displaystyle\sum_{n\in\mathbb{N}}\lambda_{n+1}(A\cap\\{[0.5,1]^{n}[0,0.5)\\})\text{~{}and~{}}$
$\displaystyle\llbracket\mathit{geometric}\
0.5\rrbracket_{\mathbb{S}}(\\{n\\})={}$
$\displaystyle\int\\![s\in\\{[0.5,1]^{n}[0,0.5)\\}]\,ds=\frac{1}{2^{n+1}}.$

As seen above, we use the exception $\mathtt{fail}$ to model the failure of a
hard constraint. To restrict attention to normal termination, we modify
$\mathbf{P}_{M}$ as follows.

$\displaystyle\mathbf{P}^{\mathcal{V}}_{\\!M}(s)$
$\displaystyle=\left\\{\begin{array}[]{ll}w&\mbox{if $M\Downarrow^{s}_{w}V$
for some $V\in\mathcal{V}$}\\\ 0&\mbox{otherwise.}\end{array}\right.$

As above, this density function generates distributions over traces and values
as, respectively

$\langle\\!\langle
M\rangle\\!\rangle^{\\!\mathcal{V}}(A):=\int_{A}\mathbf{P}^{\mathcal{V}}_{M}=\langle\\!\langle
M\rangle\\!\rangle(A\cap\mathbf{O}_{M}^{-1}(\mathcal{V}))$ ${(\llbracket
M\rrbracket_{\mathbb{S}})}\rvert_{\mathcal{V}}(A):=\langle\\!\langle
M\rangle\\!\rangle^{\\!\mathcal{V}}(\mathbf{O}^{-1}_{M}(A))=\int\mathbf{P}^{\mathcal{V}}_{\\!M}(s)\cdot[\mathbf{O}_{M}(s)\in
A]\,ds$

$\displaystyle d(x,x)$ $\displaystyle{}=0$ $\displaystyle d(c,d)$
$\displaystyle{}=\lvert{c-d}\rvert$ $\displaystyle d(MN,LP)$
$\displaystyle{}=d({M},{L})+d({N},{P})$ $\displaystyle
d(g(V_{1},\dots,V_{n}),$ $\displaystyle g(W_{1},\dots,W_{n}))$
$\displaystyle{}=d(V_{1},W_{1})+\dots+d(V_{n},W_{n})$ $\displaystyle d(\lambda
x.M,\lambda x.N)$ $\displaystyle{}=d({M},{N})$ $\displaystyle
d(\mathsf{D}(V_{1},\dots,V_{n}),$
$\displaystyle\mathsf{D}({W_{1},\dots,W_{n}}))$
$\displaystyle{}=d(V_{1},W_{1})+\dots+d(V_{n},W_{n})$ $\displaystyle
d(\mathtt{score}(V),\mathtt{score}(W))$ $\displaystyle{}=d(V,W)$
$\displaystyle d(\mathtt{if}\ {V}\ \mathtt{then}\ {M}\ \mathtt{else}\ {N},$
$\displaystyle\mathtt{if}\ {W}\ \mathtt{then}\ {L}\ \mathtt{else}\ {P})$
$\displaystyle{}=d(V,W)+d(M,L)+d(N,P)$ $\displaystyle
d(\mathtt{fail},\mathtt{fail})$ $\displaystyle{}=0$ $\displaystyle d({M},{N})$
$\displaystyle{}=\infty\text{ otherwise}$

Figure 7: Metric $d$ on terms.

To show that the above definitions make sense measure-theoretically, we first
define the measurable space of terms $(\Lambda,\mathcal{M})$, where
$\mathcal{M}$ is the set of Borel-measurable sets of terms with respect to the
recursively defined metric $d$ in Figure 7.

###### Lemma 27

For any closed term $M$, the functions $\mathbf{P}_{M}$, $\mathbf{O}_{M}$ and
$\mathbf{P}_{M}^{\mathcal{V}}$ are all measurable; $\langle\\!\langle
M\rangle\\!\rangle$ and $\langle\\!\langle
M\rangle\\!\rangle^{\\!\mathcal{V}}$ are measures on
$(\mathbb{S},\mathcal{S})$; $\llbracket M\rrbracket_{\mathbb{S}}$ is a measure
on $(\mathcal{GV},{\mathcal{M}}\rvert_{\mathcal{GV}})$; and ${(\llbracket
M\rrbracket_{\mathbb{S}})}\rvert_{\mathcal{V}}$ is a measure on
$(\mathcal{V},{\mathcal{M}}\rvert_{\mathcal{V}})$.

  * Proof.

See Appendix A. $\Box$

##  4 Distribution-Based Operational Semantics

In this section we introduce small- and big-step distribution-based
operational semantics, where the small-step semantics is a generalisation of
Jones [20] to continuous distributions. We prove correspondence between the
semantics using some non-obvious properties of kernels. Moreover, we will
prove that the distribution-based semantics are equivalent to the sampling-
based semantics from Section 3. A term will correspond to a distribution over
generalised values, below called a result distribution. A term $M$ is said to
be _skeleton_ iff no real number occurs in $M$, and each variable occurs _at
most once_ in $M$. The set of skeletons is $\mathsf{SK}$. Any closed term $M$
can be written as $N\\{\vec{c}/\vec{x}\\}$, where $N$ is a skeleton. The set
of closed terms corresponding this way to a skeleton $M\in\mathsf{SK}$ is
denoted as $\mathsf{TM}(M)$. If the underlying term is a skeleton,
substitution can be defined also when the substituted terms are _sets_ of
values rather than mere values, because variables occurs at most once; in that
case, we will used the notation $M\\{X/x\\}$, where $X$ is any set of values.

###  4.1 Sub-Probability Kernels

If $(X,\Sigma)$ and $(Y,\Sigma^{\prime})$ are measurable spaces, then a
function $Q:X\times\Sigma^{\prime}\rightarrow\mathbb{R}_{[0,1]}$ is called a
_(sub-probability) kernel_ (from $(X,\Sigma)$ to $(Y,\Sigma^{\prime})$) if

  * 1.

for every $x\in X$, $Q(x,\cdot)$ is a sub-probability distribution on
$(Y,\Sigma^{\prime})$; and

  * 2.

for every $A\in\Sigma^{\prime}$, $Q(\cdot,A)$ is a non-negative measurable
function $X\to\mathbb{R}_{[0,1]}$.

The measurable function $q:X\times Y\to\mathbb{R}_{+}$ is said to be a
_density_ of kernel $Q$ with respect to a measure $\mu$ on
$(Y,\Sigma^{\prime})$ if $Q(v,A)=\int_{A}q(v,y)\,\mu(dy)$ for all $v\in X$ and
$A\in\Sigma^{\prime}$. When $Q$ is a kernel, note that $\int\\!f(y)\,Q(x,dy)$
denotes the integral of $f$ with respect to the measure $Q(x,\cdot)$.

Kernels can be composed in the following ways: If $Q_{1}$ is a kernel from
$(X_{1},\Sigma_{1})$ to $(X_{2},\Sigma_{2})$ and $Q_{2}$ is a kernel from
$(X_{2},\Sigma_{2})$ to $(X_{3},\Sigma_{3})$, then $Q_{2}\circ
Q_{1}:(x,A)\mapsto\int Q_{2}(y,A)\,Q_{1}(x,dy)$ is a kernel from
$(X_{1},\Sigma_{1})$ to $(X_{3},\Sigma_{3})$. Moreover, if $Q_{1}$ is a kernel
from $(X_{1},\Sigma_{1})$ to $(X_{2},\Sigma_{2})$ and $Q_{2}$ is a kernel from
$(X^{\prime}_{1},\Sigma^{\prime}_{1})$ to
$(X^{\prime}_{2},\Sigma^{\prime}_{2})$, then $Q_{1}\times
Q_{2}:((x,y),(A\times B))\mapsto Q_{1}(x,A)\cdot Q_{2}(y,B)$ uniquely extends
to a kernel from
$(X_{1},\Sigma_{1})\times(X^{\prime}_{1},\Sigma^{\prime}_{1})$ to
$(X_{2},\Sigma_{2})\times(X^{\prime}_{2},\Sigma^{\prime}_{2})$.

###  4.2 Approximation Small-Step Semantics

The first thing we need to do is to generalize deterministic reduction into a
relation between closed terms and term _distributions_. If $\mu$ is a measure
on terms and $E$ is an evaluation context, we let $E\\{\mu\\}$ be the push-
forward measure $A\mapsto\mu(\\{M\mid E[M]\in A\\})$.

_One-step evaluation_ is a relation $M\rightarrow\mathscr{D}$ between closed
terms $M$ and distributions $\mathscr{D}$ on terms, defined as follows:

$\displaystyle E[\mathsf{D}(\vec{c})]$ $\displaystyle\rightarrow
E\\{\mu_{\mathsf{D}(\vec{c})}\\}$ $\displaystyle E[M]$
$\displaystyle\rightarrow\delta(E[N])\text{~{}if~{}}M\xrightarrow{\text{det}}N$
$\displaystyle E[\mathtt{score}(c)]$ $\displaystyle\rightarrow
c\cdot\delta(E[\texttt{true}])\text{~{}if~{}}0<c\leq 1$

We first of all want to show that one-step reduction is essentially
deterministic, and that we have a form of deadlock-freedom.

###### Lemma 28

For every closed term $M$, either $M$ is a generalized value or there is a
unique $\mathscr{D}$ such that $M\rightarrow\mathscr{D}$.

  * Proof.

An easy consequence of Lemma 1. $\Box$

We need to prove the just introduced notion of one-step reduction to support
composition. This is captured by the following result.

###### Lemma 29

$\rightarrow$ is a sub-probability kernel.

Let $R\Lambda_{P}=\\{E[R]\in C\Lambda\\}$ be the set of all closed reducible
terms.

  * Proof.

Lemma 28 already tells us that $\rightarrow$ can be seen as a function
$\hat{\rightarrow}$ defined as follows:

$\hat{\rightarrow}(M,A)=\left\\{\begin{array}[]{ll}\mathscr{D}(A)&\mbox{if
$M\rightarrow\mathscr{D}$;}\\\ $0$&\mbox{otherwise.}\end{array}\right.$

The fact that $\hat{\rightarrow}(M,\cdot)$ is a distribution is easily
verified. On other hand, the fact that $\hat{\rightarrow}(\cdot,A)$ is
measurable amounts to proving that
$\mathit{OS}(A,B)=(\hat{\rightarrow}(\cdot,A))^{-1}(B)$ is a measurable set of
terms whenever $B$ is a measurable set of real numbers. We will do that by
showing that for every skeleton $N$, the set
$\mathit{OS}(A,B)\cap\mathsf{TM}(N)$ is measurable. The thesis then follows by
observing that

$\mathit{OS}(A,B)=\bigcup_{N\in\mathsf{SK}}\mathit{OS}(A,B)\cap\mathsf{TM}(N)$

and that $\mathsf{SK}$ is countable. Now, let us observe that for every
skeleton $N$, the nature of any term $L$ in $\mathsf{TM}(N)$ as for if being a
value, or containing a deterministic redex, or containing a sampling redex,
only depends on $N$ and not on the term $L$. As an example, terms in
$\mathsf{TM}(xy)$ are nothing but deterministic redexes (actually, all of them
rewrites deterministically to $\delta(\mathtt{fail})$. This allows us to
proceed by distinguishing three cases:

    * •

If all terms in $\mathsf{TM}(N)$ are values, then it can be easily verified
that

$\mathit{OS}(A,B)\cap\mathsf{TM}(N)=\left\\{\begin{array}[]{ll}\mathsf{TM}(N)&\mbox{
if $0\in B$;}\\\ \varnothing&\mbox{ if $0\not\in B$.}\end{array}\right.$

Both when $0\in B$ and when $0\not\in B$, then,
$\mathit{OS}(A,B)\cap\mathsf{TM}(N)$ is indeed measurable.

    * •

If all terms in $\mathsf{TM}(N)$ contain deterministic redexes, then

$\mathit{OS}(A,B)\cap\mathsf{TM}(N)=\left\\{\begin{array}[]{ll}\rightarrow^{-1}(A)\cap\mathsf{TM}(N)&\mbox{
if $1\in B$}\\\ \varnothing&\mbox{ if $1\not\in B$.}\end{array}\right.$

Since deterministic reduction $\rightarrow$ is known to be measurable, then
both when $1\in B$ and when $1\not\in B$, the set
$\mathit{OS}(A,B)\cap\mathsf{TM}(N)$ is measurable.

    * •

The hardest case is when $N$ is of the form $G[\mathsf{D}(\vec{x})]$, where
$G$ is an evaluation context. In this case, however, we can proceed by
decomposing the function we want to prove measurable into three measurable
functions:

      * •

The function $\mathit{app}:\mathcal{C}\times C\Lambda\rightarrow C\Lambda$,
that given an evaluation context $E$ and a term $M$, returns the term $E[M]$.
This is proved measurable in the Appendix.

      * •

The function $\mathit{deapp}:R\Lambda_{P}\rightarrow\mathcal{C}\times
C\Lambda$ that “splits” a term in $R\Lambda_{P}$ into an evaluation context
$E$ and a closed term $M$. This is proved measurable in the Appendix.

      * •

For every distribution identifier $\mathsf{D}$, the function
$\mathit{distapp}_{\mathsf{D}}:\mathbb{R}^{n}\rightarrow C\Lambda$ (where $n$
is the arity of $\mathsf{D}$) that, given a tuple of real numbers $x$, returns
the term $\mathsf{D}(x)$. This function is a continuous function between two
metric spaces, so measurable.

      * •

We know that for every distribution identifier $\mathsf{D}$, there is a kernel
$\mu_{\mathsf{D}}:\mathbb{R}^{n}\times\Sigma_{\mathbb{R}}\rightarrow\mathbb{R}_{[0,1]}$.
Moreover, one can also consider the Dirac kernel on evaluation contexts,
namely $I:\mathcal{C}\times\Sigma_{\mathcal{C}}\rightarrow\mathbb{R}_{[0,1]}$
where $I(E,A)={[{A}\in{E}]}$. Then, the product $\mu_{\mathsf{D}}\times I$ is
also a kernel, so measurable.

This concludes the proof. $\Box$

Given a family $\\{\mathscr{D}_{M}\\}_{M\in A}$ of distributions indexed by
terms in a measurable set $A$ of terms, and a measurable set $B$, we often
write, with an abuse of notation, $\mathscr{D}_{M}(B)$ for the function that
assigns to any term $M\in A$ the real number $\mathscr{D}_{M}(B)$. The _step-
indexed approximation small-step semantics_ is the family of $n$-indexed
relations $M\Rightarrow_{n}\mathscr{D}$ between terms and result distributions
inductively defined in Figure 9.

$n>0$ $G\Rightarrow_{n}\delta(G)$ (DRed Val) $M\Rightarrow_{0}\mathbf{0}$
(DRed Empty) $M\rightarrow\mathscr{D}$
$\\{N\Rightarrow_{n}\mathscr{E}_{N}\\}_{N\in\operatorname{supp}(\mathscr{D})}$
$M\Rightarrow_{n+1}A\mapsto\int\mathscr{E}_{N}(A)\;\mathscr{D}(dN)$ (DRed
Step)

Figure 8: Step-Indexed Approximation Small-Step Semantics.

$n>0$ $G\Rightarrow_{n}\delta(G)$ (DRed Val) $M\Rightarrow_{0}\mathbf{0}$
(DRed Empty) $M\rightarrow\mathscr{D}$
$\\{N\Rightarrow_{n}\mathscr{E}_{N}\\}_{N\in\operatorname{supp}(\mathscr{D})}$
$M\Rightarrow_{n+1}A\mapsto\int\mathscr{E}_{N}(A)\;\mathscr{D}(dN)$ (DRed
Step)

Figure 9: Step-Indexed Approximation Small-Step Semantics.

Since generalised values have no transitions (there is no $\mathscr{D}$ such
that $G\to\mathscr{D}$), the rules above are disjoint and so there is at most
one $\mathscr{D}$ such that $M\to_{n}\mathscr{D}$. Compared to the discrete
case [20], the step-index $n$ is needed to ensure that the integral in (DRed
Step) is defined.

###### Lemma 30

For every $n\in\mathbb{N}$, the function $\Rightarrow_{n}$ is a kernel.

  * Proof.

By induction on $n$:

    * •

$\Rightarrow_{0}$ can be seen as the function $\hat{\rightarrow}_{0}$ that
attributes $0$ to any pair $(M,A)$. This is clearly a kernel.

    * •

$\Rightarrow_{n+1}$ can be seen as the function $\hat{\Rightarrow_{n+1}}$
defined as follows:

$\hat{\rightarrow}_{n+1}(M,A)=\left\\{\begin{array}[]{ll}1&\mbox{if
$M\in\mathcal{GV}$ and $M\in A$};\\\ 0&\mbox{if $M\in\mathcal{GV}$ and
$M\not\in A$};\\\ (\int\hat{\rightarrow}_{n}(N,A)\,\mathscr{D}(dN))&\mbox{if
$M\rightarrow\mathscr{D}$}.\end{array}\right.$

The fact that $\hat{\rightarrow}_{n+1}(M,\cdot)$ is a measure for every $M$ is
clear, and can be proved by case distinction on $M$. On the other hand, if $B$
is a measurable set of reals, then:

$\displaystyle(\hat{\rightarrow}_{n+1}(\cdot,A))^{-1}(B)=$
$\displaystyle\;(\hat{\rightarrow}_{n+1}(\cdot,A))^{-1}(B)\cap\mathcal{GV}\;\cup$
$\displaystyle\;(\hat{\rightarrow}_{n+1}(\cdot,A))^{-1}(B)\cap(C\Lambda-\mathcal{GV}).$

Now, the fact that
$(\hat{\rightarrow}_{n+1}(\cdot,A))^{-1}(B)\cap\mathcal{GV}$ is a measurable
set of terms is clear: it is $A\cap\mathcal{GV}$ if $1\in B$ and $\varnothing$
otherwise. But how about
$(\hat{\rightarrow}_{n+1}(\cdot,A))^{-1}(B)\cap(C\Lambda-\mathcal{GV})$? In
that case, we just need to notice that

$(\hat{\rightarrow}_{n+1}(\cdot,A))^{-1}(B)\cap(C\Lambda-\mathcal{GV})=(\hat{\rightarrow}_{n}\circ\rightarrow)^{-1}(B)$

where $\hat{\rightarrow}_{n}$ and $\rightarrow$ are kernels (the former by
induction hypothesis, the latter by Lemma 29). Since kernels compose, this
concludes the proof.

$\Box$

###### Lemma 31

For every closed term $M$ and for every $n\in\mathbb{N}$ there is a unique
distribution $\mathscr{D}$ such that $M\Rightarrow_{n}\mathscr{D}$.

  * Proof.

This is an easy consequence of Lemma 30. $\Box$

###  4.3 Approximation Big-Step Semantics

The _step-indexed approximation big-step semantics_
$M\Downarrow_{n}\mathscr{D}$ is the $n$-indexed family of relations between
terms and result distributions inductively defined by the rules in Figure 11.

$n>0$ $G\Downarrow_{n}\delta(G)$ (DEval Val) $M\Downarrow_{0}\mathbf{0}$
(DEval Empty) $n>0$ $T\Downarrow_{n}\delta(\mathtt{fail})$ (DEval Fail) $n>0$
$\mathsf{D}(\vec{c})\Downarrow_{n}\mu_{\mathsf{D}(\vec{c})}$ (DEval Samp)
$n>0$ $g(\vec{c})\Downarrow_{n}\delta(\sigma_{g}(\vec{c}))$ (DEval Fun)
$0<c\leq 1$ $n>0$ $\mathtt{score}(c)\Downarrow_{n}c\cdot\delta(\texttt{true})$
(DEval Score) $M\Downarrow_{n}\mathscr{D}$ $\mathtt{if}\ {\mathtt{true}}\
\mathtt{then}\ {M}\ \mathtt{else}\ {N}\Downarrow_{n+1}\mathscr{D}$ (DEval If
True) $N\Downarrow_{n}\mathscr{D}$ $\mathtt{if}\ {\mathtt{false}}\
\mathtt{then}\ {M}\ \mathtt{else}\ {N}\Downarrow_{n+1}\mathscr{D}$ (DEval If
False) $M\Downarrow_{n}\mathscr{D}$ $N\Downarrow_{n}\mathscr{E}$
$\\{L\\{V/x\\}\Downarrow_{n}\mathscr{E}_{L,V}\\}_{(\lambda
x.L)\in\operatorname{supp}(\mathscr{D}),V\in\operatorname{supp}(\mathscr{E})}$
$MN\Downarrow_{n+1}A\mapsto{\mathscr{D}}\rvert_{\\{\mathtt{fail}\\}}(A)+\mathscr{D}(\mathbb{R})\cdot{[{\mathtt{fail}}\in{A}]}+\mathscr{D}(\mathcal{V}_{\lambda})\cdot{\mathscr{E}}\rvert_{\\{\mathtt{fail}\\}}(A)+\iint\mathscr{E}_{L,V}(A)\,{\mathscr{D}}\rvert_{\mathcal{V}_{\lambda}}(\lambda
x.dL)\,{\mathscr{E}}\rvert_{\mathcal{V}}(dV)$ (DEval Appl)

Figure 10: Step Indexed Approximation Big-Step Semantics.

$n>0$ $G\Downarrow_{n}\delta(G)$ (DEval Val) $M\Downarrow_{0}\mathbf{0}$
(DEval Empty) $n>0$ $T\Downarrow_{n}\delta(\mathtt{fail})$ (DEval Fail) $n>0$
$\mathsf{D}(\vec{c})\Downarrow_{n}\mu_{\mathsf{D}(\vec{c})}$ (DEval Samp)
$n>0$ $g(\vec{c})\Downarrow_{n}\delta(\sigma_{g}(\vec{c}))$ (DEval Fun)
$0<c\leq 1$ $n>0$ $\mathtt{score}(c)\Downarrow_{n}c\cdot\delta(\texttt{true})$
(DEval Score) $M\Downarrow_{n}\mathscr{D}$ $\mathtt{if}\ {\mathtt{true}}\
\mathtt{then}\ {M}\ \mathtt{else}\ {N}\Downarrow_{n+1}\mathscr{D}$ (DEval If
True) $N\Downarrow_{n}\mathscr{D}$ $\mathtt{if}\ {\mathtt{false}}\
\mathtt{then}\ {M}\ \mathtt{else}\ {N}\Downarrow_{n+1}\mathscr{D}$ (DEval If
False) $M\Downarrow_{n}\mathscr{D}$ $N\Downarrow_{n}\mathscr{E}$
$\\{L\\{V/x\\}\Downarrow_{n}\mathscr{E}_{L,V}\\}_{(\lambda
x.L)\in\operatorname{supp}(\mathscr{D}),V\in\operatorname{supp}(\mathscr{E})}$
$MN\Downarrow_{n+1}\begin{array}[t]{@{}l@{}}A\mapsto{\mathscr{D}}\rvert_{\\{\mathtt{fail}\\}}(A)+\mathscr{D}(\mathbb{R})\cdot{[{\mathtt{fail}}\in{A}]}+\mathscr{D}(\mathcal{V}_{\lambda})\cdot{\mathscr{E}}\rvert_{\\{\mathtt{fail}\\}}(A)\\\
\qquad\qquad+\iint\mathscr{E}_{L,V}(A)\,{\mathscr{D}}\rvert_{\mathcal{V}_{\lambda}}(\lambda
x.dL)\,{\mathscr{E}}\rvert_{\mathcal{V}}(dV)\end{array}$ (DEval Appl)

Figure 11: Step Indexed Approximation Big-Step Semantics.

Above, the rule for applications is the most complex, with the resulting
distribution consisting of three exceptional terms in addition to the normal
case. To better understand this rule, one can study what happens if we replace
general applications with a let construct plus application of values to
values. Then we would end up having the following three rules, instead of the
rule for application above:

$M\Downarrow_{n}\mathscr{D}$
$\\{N\\{V/x\\}\Downarrow_{n}\mathscr{E}_{V}\\}_{V\in\operatorname{supp}(\mathscr{D})}$
$\mathtt{let}\;x=M\;\mathtt{in}\;N\Downarrow_{n+1}A\mapsto\left(\begin{array}[]{l}{\mathscr{D}}\rvert_{\\{\mathtt{fail}\\}}(A)+\mathscr{D}(\mathbb{R})\cdot{[{\mathtt{fail}}\in{A}]}\\\
+\int\mathscr{E}_{V}(A)\,{\mathscr{D}}\rvert_{\mathcal{V}}(dV)\end{array}\right)$
$M\\{V/x\\}\Downarrow_{n}\mathscr{E}$ $(\lambda
x.M)V\Downarrow_{n+1}\mathscr{E}$ $n>0$
$c\;V\Downarrow_{n}\delta(\mathtt{fail})$

The existence of the integral in rule (DEval Appl) is guaranteed by a lemma
analogous to Lemma 30.

###### Lemma 32

For every $n\in\mathbb{N}$, the function $\Downarrow_{n}$ is a kernel.

This can be proved by induction on $n$, with the most difficult case being
precisely the one of applications. Composition and product properties of
kernels are the key ingredients there.

###  4.4 Beyond Approximations

The set of result distributions with the pointwise order forms an
$\omega\mathbf{CPO}$, and thus any denumerable, directed set of result
distributions has a least upper bound. One can define the _small-step
semantics_ and the _big-step semantics_ as, respectively, the two
distributions

$\displaystyle\llbracket M\rrbracket_{\Rightarrow}$
$\displaystyle=\sup\\{\mathscr{D}\mid{M}\to_{n}{\mathscr{D}}\\}$
$\displaystyle\qquad\qquad\llbracket M\rrbracket_{\Downarrow}$
$\displaystyle=\sup\\{\mathscr{D}\mid M\Downarrow_{n}\mathscr{D}\\}$

It would be quite disappointing if the two object above were different.
Indeed, this section is devoted to proving the following theorem:

###### Theorem 2

For every term $M$, $\llbracket M\rrbracket_{\Rightarrow}=\llbracket
M\rrbracket_{\Downarrow}$.

The following is a fact which will be quite useful in the following:

######  Lemma 33 (Monotonicity)

If $M\Rightarrow_{n}\mathscr{D}$, $m\geq n$ and $M\Rightarrow_{m}\mathscr{E}$,
then $\mathscr{E}\geq\mathscr{D}$.

Theorem 2 can be proved by showing that any big-step approximation can itself
over-approximated with small-step, and vice versa. Let us start by showing
that, essentially, the big-step rule for applications is small-step-
admissible:

###### Lemma 34

If $M\Rightarrow_{n}\mathscr{D}$, $N\Rightarrow_{m}\mathscr{E}$, and for all
$L$ and $V$, $L\\{V/x\\}\Rightarrow_{p}\mathscr{E}_{L,V}$, then
$MN\Rightarrow_{n+m+p}\mathscr{F}$ such that for all $A$

$\displaystyle\mathscr{F}(A)\geq{}$
$\displaystyle{\mathscr{D}}\rvert_{\\{\mathtt{fail}\\}}(A)+\mathscr{D}(\mathbb{R})\cdot{[{\mathtt{fail}}\in{A}]}+\mathscr{D}(\mathcal{V}_{\lambda})\cdot{\mathscr{E}}\rvert_{\\{\mathtt{fail}\\}}(A)$
$\displaystyle+\iint\mathscr{E}_{L,V}(A)\,{\mathscr{D}}\rvert_{\mathcal{V}_{\lambda}}(\lambda
x.dL)\,{\mathscr{E}}\rvert_{\mathcal{V}}(dV).$

  * Proof.

First of all, one can prove that if $N\Rightarrow_{n}\mathscr{D}$ and
$L\\{V/x\\}\Rightarrow_{m}\mathscr{E}_{V}$ for all $V$ then $(\lambda
x.L)N\Rightarrow_{n+m}\mathscr{F}$ where
$\mathscr{F}(A)\geq{\mathscr{D}}\rvert_{\\{\mathtt{fail}\\}}(A)+\int\mathscr{E}_{V}(A)\,{\mathscr{D}}\rvert_{\mathcal{V}}(dV)$
for all $A$. This is an induction on $n$.

    * •

If $n=0$, then $\mathscr{D}$ is necessarily the zero distribution $A\mapsto
0$. Then $\mathscr{F}(A)\geq
0={\mathscr{D}}\rvert_{\\{\mathtt{fail}\\}}(A)+\int\mathscr{E}_{V}(A)\,{\mathscr{D}}\rvert_{\mathcal{V}}(dV))$.

    * •

Suppose the thesis holds for $n$, and let’s try to prove the thesis for $n+1$.
We proceed by further distinguishing some subcases:

      * •

If $N$ is a value $W$, then $\mathscr{D}=\delta(W)$,
${\mathscr{D}}\rvert_{\\{\mathtt{fail}\\}}$ is the zero distribution and thus

$(\lambda
x.L)N\Rightarrow_{m+1}(A\mapsto{\mathscr{D}}\rvert_{\\{\mathtt{fail}\\}}(A)+\int\mathscr{E}_{V}(A)\,{\mathscr{D}}\rvert_{\mathcal{V}}(dV)).$

The thesis follows by monotonicity.

      * •

If $N$ is an exception $\mathtt{fail}$, then
$\mathscr{D}=\delta(\mathtt{fail})$, and since $(\lambda
x.L)\mathtt{fail}\rightarrow\mathtt{fail}$, we can conclude that, since
${\mathscr{D}}\rvert_{\mathcal{V}}$ is the zero distribution,

$(\lambda
x.L)N\Rightarrow_{2}\delta(\mathtt{fail})=(A\mapsto{\mathscr{D}}\rvert_{\\{\mathtt{fail}\\}}(A)+\int\mathscr{E}_{V}(A)\,{\mathscr{D}}\rvert_{\mathcal{V}}(dV)).$

The thesis again follows by monotonicity.

      * •

If $N$ is not a generalized value, then, necessarily
$\mathscr{D}(A)=\int\mathscr{G}_{P}(A)\,\mathscr{H}(dP)$, where
$N\rightarrow\mathscr{H}$ and $P\Rightarrow_{n}\mathscr{G}_{P}$ for every $P$.
By induction hypothesis, there are distributions $\mathscr{I}_{P}$ such that
$(\lambda x.L)P\Rightarrow_{n+m}\mathscr{I}_{P}$, and, for all $A$,

$\mathscr{I}_{P}(A)\geq{\mathscr{G}_{P}}\rvert_{\\{\mathtt{fail}\\}}+\int\mathscr{E}_{V}(A)\,{\mathscr{G}_{P}}\rvert_{\mathcal{V}}(dV)$

Let now $E$ be the evaluation context $(\lambda x.L)[\cdot]$. Then, it holds
that $(\lambda x.L)N\rightarrow E\\{\mathscr{H}\\}$ and thus:

$(\lambda
x.L)N\Rightarrow_{n+m+1}(A\mapsto\int\mathscr{I}_{P}(A)\,(E\\{\mathscr{H}\\}((\lambda
x.L)dP))).$

We can now observe that:

$\displaystyle\int\mathscr{I}_{P}(A)$
$\displaystyle\,(E\\{\mathscr{H}\\}((\lambda
x.L)dP))=\int\mathscr{I}_{P}(A)\,\mathscr{H}(dP)$
$\displaystyle\geq\int{\mathscr{G}_{P}}\rvert_{\\{\mathtt{fail}\\}}(A)\,\mathscr{H}(dP)+\iint\mathscr{E}_{V}(A)\,{\mathscr{G}_{P}}\rvert_{\mathcal{V}}(dV)\,\mathscr{H}(dP)$
$\displaystyle={\mathscr{D}}\rvert_{\\{\mathtt{fail}\\}}(A)+\iint\mathscr{E}_{V}(A)\,{\mathscr{G}_{P}}\rvert_{\mathcal{V}}(dV)\,\mathscr{H}(dP)$
$\displaystyle={\mathscr{D}}\rvert_{\\{\mathtt{fail}\\}}(A)+\int\mathscr{E}_{V}(A)\,{\mathscr{D}}\rvert_{\mathcal{V}}(dV).$

Then one can prove the statement of the lemma, again by induction on $n$,
following the same strategy as above. $\Box$

###### Lemma 35

If $M\Downarrow_{n}\mathscr{D}$ there is $\mathscr{E}$ s.t.
$M\Rightarrow_{3^{n}}\mathscr{E}$ and $\mathscr{E}\geq\mathscr{D}$.

  * Proof.

By induction on $n$, we can prove that if $M\Downarrow_{n}\mathscr{D}$, then
$M\Rightarrow_{\mathscr{E}}$ where $\mathscr{E}\geq\mathscr{D}$. The only
interesting case is when $M$ is an application, and there we simply use Lemma
34. $\Box$

At this point, we already know that $\llbracket
M\rrbracket_{\Rightarrow}\geq\llbracket M\rrbracket_{\Downarrow}$. The
symmetric inequality can be proved by showing that the big-step rule for
applications can be _inverted_ in the small-step:

###### Lemma 36

If $MN\Rightarrow_{n+1}\mathscr{D}$, then $M\Rightarrow_{n}\mathscr{E}$,
$N\Rightarrow_{n}\mathscr{F}$ and for all $P$ and $V$,
$P\\{V/x\\}\Rightarrow_{n}\mathscr{G}_{P,V}$ such that for all $A$,

$\displaystyle\mathscr{D}(A)\leq{}$
$\displaystyle{\mathscr{E}}\rvert_{\\{\mathtt{fail}\\}}(A)+\mathscr{E}(\mathbb{R})\cdot{[{\mathtt{fail}}\in{A}]}+\mathscr{E}(\mathcal{V}_{\lambda})\cdot{\mathscr{F}}\rvert_{\\{\mathtt{fail}\\}}(A)$
$\displaystyle+\iint\mathscr{G}_{P,V}(A)\,{\mathscr{E}}\rvert_{\mathcal{V}_{\lambda}}(\lambda
x.dP)\,{\mathscr{F}}\rvert_{\mathcal{V}}(dV).$

  * Proof.

By induction on $n$.

    * •

If $n=0$, then $\mathscr{D}$ is the zero distribution, and so are
$\mathscr{E},\mathscr{F}$ and all $\mathscr{G}_{P,V}$.

    * •

Suppose the thesis holds for every natural number smaller than $n$ and prove
it for $n$. Let us distinguish a few cases, and examine the most relevant
ones:

      * •

If $M$ is an abstraction $\lambda x.L$ and $N$ is a value $W$, then
$M\rightarrow\delta(L\\{W/x\\})$ and $L\\{W/x\\}\Rightarrow_{n}\mathscr{D}$.
We can then observe that

$\displaystyle\mathscr{E}$ $\displaystyle=\delta(\lambda x.L)$
$\displaystyle\mathscr{F}$ $\displaystyle=\delta(W)$
$\displaystyle\mathscr{G}_{P,V}$ $\displaystyle=\mathscr{D}\mbox{ whenever
}P=L\mbox{ and }V=W$

Just observe that

$\mathscr{D}(A)=\iint\mathscr{G}_{P,V}(A)\,\mathscr{E}(\lambda
x.dP)\,\mathscr{F}(dV)$

and that
${\mathscr{E}}\rvert_{\\{\mathtt{fail}\\}}={\mathscr{E}}\rvert_{\mathbb{R}}={\mathscr{F}}\rvert_{\\{\mathtt{fail}\\}}=\mathbf{0}$.

      * •

If none of $M$ and $N$ are values, then $M\rightarrow\mathscr{L}$ and thus
$MN\rightarrow E\\{\mathscr{L}\\}$ where $E=[\cdot]N$. Moreover,
$LN\Rightarrow_{n}\mathscr{H}_{L}$, where

$\mathscr{D}(A)=\int\mathscr{H}_{L}(A)\,E\\{\mathscr{L}\\}((dL)N)=\int\mathscr{H}_{L}(A)\,\mathscr{L}(dL)$

We apply the induction hypothesis (and monotonicity) to each of the
$LN\Rightarrow_{n}\mathscr{H}_{L}$, and we obtain that
$L\Rightarrow_{n-1}\mathscr{I}_{L}$, $N\Rightarrow_{n}\mathscr{F}$ and
$P\\{V/x\\}\Rightarrow_{n}\mathscr{G}_{P,V}$, where

$\displaystyle\mathscr{H}_{L}(A)\leq{}$
$\displaystyle{\mathscr{I}_{L}}\rvert_{\\{\mathtt{fail}\\}}(A)+\mathscr{I}_{L}(\mathbb{R})\cdot{[{\mathtt{fail}}\in{A}]}+\mathscr{I}_{L}(\mathcal{V}_{\lambda})\cdot{\mathscr{F}}\rvert_{\\{\mathtt{fail}\\}}(A)$
$\displaystyle{}+\iint\mathscr{G}_{P,V}(A)\,{\mathscr{I}_{L}}\rvert_{\mathcal{V}_{\lambda}}(\lambda
x.dP)\,{\mathscr{F}}\rvert_{\mathcal{V}}(dV)$

Now let $\mathscr{E}$ be the distribution

$A\mapsto\int\mathscr{I}_{L}(A)\,\mathscr{L}(dL).$

Clearly, $M\Rightarrow_{n}\mathscr{E}$. Moreover,

$\displaystyle\mathscr{D}(A)$
$\displaystyle=\int\mathscr{H}_{L}(A)\,\mathscr{L}(dL)$
$\displaystyle\leq\int{\mathscr{I}_{L}}\rvert_{\\{\mathtt{fail}\\}}(A)\,\mathscr{L}(dL)+\int\mathscr{I}_{L}(\mathbb{R})\cdot{[{\mathtt{fail}}\in{A}]}\,\mathscr{L}(dL)$
$\displaystyle\qquad+\int\mathscr{I}_{L}(\mathcal{V}_{\lambda})\cdot{\mathscr{F}}\rvert_{\\{\mathtt{fail}\\}}(A)\,\mathscr{L}(dL)$
$\displaystyle\qquad+\iiint\mathscr{G}_{P,V}(A)\,{\mathscr{I}_{L}}\rvert_{\mathcal{V}_{\lambda}}(\lambda
x.dP)\,{\mathscr{F}}\rvert_{\mathcal{V}}(dV)\,\mathscr{L}(dL)$
$\displaystyle={\mathscr{E}}\rvert_{\\{\mathtt{fail}\\}}(A)+\mathscr{E}(\mathbb{R})\cdot{[{\mathtt{fail}}\in{A}]}+\mathscr{E}(\mathcal{V}_{\lambda})\cdot{\mathscr{F}}\rvert_{\\{\mathtt{fail}\\}}(A)$
$\displaystyle\qquad+\iint\mathscr{G}_{P,V}(A)\,{\mathscr{E}}\rvert_{\mathcal{V}_{\lambda}}(\lambda
x.dP)\,{\mathscr{F}}\rvert_{\mathcal{V}}(dV)$

$\Box$

###### Lemma 37

If $M\Rightarrow_{n}\mathscr{D}$, then there is $\mathscr{E}$ such that
$M\Downarrow_{n}\mathscr{E}$ and $\mathscr{E}\geq\mathscr{D}$.

  * Proof.

Again, this is an induction on $n$ that makes essential use, this time, of
Lemma 36. $\Box$

  * Restatement of Theorem 2. For all $M$, $\llbracket M\rrbracket_{\Rightarrow}=\llbracket M\rrbracket_{\Downarrow}$.

  * Proof.

This is a consequence of Lemma 35 and Lemma 37. $\Box$

In subsequent sections we let $\llbracket M\rrbracket$ stand for $\llbracket
M\rrbracket_{\Rightarrow}$ or $\llbracket M\rrbracket_{\Downarrow}$.

###  4.5 Geometric Distribution, Revisited

Let’s consider again the geometric distribution of Section 2.4. There is a
monotonically increasing map $f:\mathbb{N}\rightarrow\mathbb{N}$ such that for
every $n$, it holds that

$(\mathit{geometric}\;0.5)\Rightarrow_{f(n)}\sum_{i=0}^{n}\frac{1}{2^{i+1}}\delta(i)$

As a consequence,
$\llbracket\mathit{geometric}\;0.5\rrbracket=\sum_{i=0}^{\infty}\frac{1}{2^{i+1}}\delta(i)$.

###  4.6 Distribution-based and Sampling-based Semantics are Equivalent

This section is a proof of the following theorem.

###### Theorem 3

For every term $M$, $\llbracket M\rrbracket_{\mathbb{S}}=\llbracket
M\rrbracket$.

The way to prove Theorem 3 is by looking at traces of _bounded_ length. For
every $n\in\mathbb{N}$, let $\mathbb{S}_{n}$ be the set of sample traces of
length at most $n$, which itself has the structure of a measure space with
measurable sets ${\cal S}\rvert_{\mathbb{S}_{n}}$. We define the result
distribution $\llbracket M\rrbracket_{\mathbb{S}}^{n}$ as follows:

$\llbracket
M\rrbracket_{\mathbb{S}}^{n}(A)=\int_{\mathbb{S}_{n}}\mathbf{P}_{\\!M}(s)\cdot{[{\mathbf{O}_{M}(s)}\in{A}]}\,ds$

The integral over _all_ traces can be seen as the limit of all integrals over
bounded-length traces:

###### Lemma 38

If $f:\mathbb{S}\to\mathbb{R}_{+}$ is measurable then
$\int\\!f=\sup_{n}\int_{\mathbb{S}_{n}}\\!f$.

  * Proof.

Let $g_{n}(s)=f(s)\cdot[s\in\mathbb{S}_{n}]$, so
$\int_{\mathbb{S}_{n}}\\!f=\int\\!g_{n}$ by definition. Since the $g_{n}$ are
converging to $f$ pointwise from below, we have
$\int\\!f=\sup_{n}\int\\!g_{n}$ by the monotone convergence theorem. $\Box$

A corollary is that $\llbracket
M\rrbracket_{\mathbb{S}}=\sup_{n\in\mathbb{N}}\llbracket
M\rrbracket_{\mathbb{S}}^{n}$.

###### Lemma 39

If $M\rightarrow\mathscr{D}$, then $\llbracket
M\rrbracket=A\mapsto\int\llbracket N\rrbracket(A)\;\mathscr{D}(dN)$

  * Proof.

For every $n$ and for every term $N$, let $\mathscr{E}^{n}_{N}$ be the unique
value distribution such that $N\Rightarrow_{n}\mathscr{E}^{n}_{N}$. By
definition, we have that

$\mathscr{E}^{n+1}_{M}(A)=\int\mathscr{E}^{n}_{N}(A)\;\mathscr{D}(dN).$

By the monotone convergence theorem, then,

$\displaystyle\llbracket M\rrbracket(A)$
$\displaystyle=\sup_{n}\mathscr{E}^{n+1}_{M}(A)=\sup_{n}\int\mathscr{E}^{n}_{N}(A)\;\mathscr{D}(dN)$
$\displaystyle=\int(\sup_{n}\mathscr{E}^{n}_{N}(A))\;\mathscr{D}(dN)=\int\llbracket
N\rrbracket(A)\;\mathscr{D}(dN).$

$\Box$

The following is a useful technical lemma.

###### Lemma 40

$\llbracket
E[\mathsf{D}(\vec{c})]\rrbracket_{\mathbb{S}}^{n+1}(A)=\int\llbracket
N\rrbracket_{\mathbb{S}}^{n}(A)\;E\\{\mu_{\mathsf{D}}(\vec{c})\\}(dN)$.

###### Lemma 41

If $M\rightarrow\mathscr{D}$, then $\llbracket
M\rrbracket_{\mathbb{S}}=A\mapsto\int\llbracket
N\rrbracket_{\mathbb{S}}(A)\;\mathscr{D}(dN)$

A program $M$ is said to _deterministically diverge_ iff
$(M,1,s)\Rightarrow(N,w,[])$ implies that $w=1$, $s=[]$, and $N$ is _not_ a
generalized value. Terms that deterministically diverge have very predictable
semantics, both distribution- and sampling-based.

###### Lemma 42

If $M$ deterministically diverges then $\llbracket M\rrbracket=\llbracket
M\rrbracket_{\mathbb{S}}=\mathbf{0}$.

  * Proof.

One can easily prove, by induction on $n$, that if $M$ deterministically
diverges, then $M\Rightarrow_{n}\mathbf{0}$:

    * •

If $n=0$, then $M\Rightarrow_{n}\mathbf{0}$ by definition.

    * •

About the inductive case, since $M$ cannot be a generalized value, it must be
that $M\rightarrow\delta(N)$ (where $N$ deterministically diverges) and that
$M\Rightarrow_{n+1}\mathscr{D}$, where $N\Rightarrow_{n}\mathscr{D}$. By
induction hypothesis, $\mathscr{D}=\mathbf{0}$.

The fact that $\llbracket M\rrbracket_{\mathbb{S}}=\mathbf{0}$ is even simpler
to prove, since if $M$ deterministically diverges, then there cannot be any
$s,w,V$ such that $M\Downarrow^{s}_{w}V$, and thus $\mathbf{P}_{\\!M}(s)$ is
necessarily $0$. $\Box$

A program $M$ is said to _deterministically converge to a program $N$_ iff
$(M,1,[])\Rightarrow(N,1,[])$. Any term that deterministically converges to
another term has the same semantics as the latter.

###### Lemma 43

Let $M$ deterministically converge to $N$. Then:

  * •

$\mathscr{D}\leq\mathscr{E}$ whenever $M\Rightarrow_{n}\mathscr{D}$; and
$N\Rightarrow_{n}\mathscr{E}$;

  * •

$\llbracket M\rrbracket_{\mathbb{S}}^{n}=\llbracket
N\rrbracket_{\mathbb{S}}^{n}$;

  * •

$\llbracket M\rrbracket=\llbracket N\rrbracket$ and $\llbracket
M\rrbracket_{\mathbb{S}}=\llbracket N\rrbracket_{\mathbb{S}}$

  * Proof.

The first point is an induction on the structure of the proof that $M$
deterministically converge to $N$. Let us consider the second and third
points. Since equality is transitive, we can assume, without losing any
generality, that $(M,1,[])\rightarrow(N,1,[])$, namely that
$M\xrightarrow{\text{det}}N$. With the latter hypothesis, it is easy to
realize that $M\Downarrow^{w}_{s}V$ iff $N\Downarrow^{w}_{s}V$ and that
$M\Rightarrow_{n+1}\mathscr{D}$ iff $N\Rightarrow_{n}\mathscr{D}$. The thesis
easily follows. $\Box$

###### Lemma 44

For every generalized value $G$, it holds that $\llbracket
G\rrbracket=\llbracket G\rrbracket_{\mathbb{S}}=\delta(G)$.

If a term does not diverge deterministically, then it converges either to a
generalized value or to a term that performs a sampling.

###### Lemma 45

For every program $M$, exactly one of the following conditions holds:

  * •

$M$ deterministically diverges;

  * •

There is generalized value $G$ such that $M$ deterministically converges to
$G$

  * •

There are $E,\mathsf{D},c_{1},\ldots,c_{|\mathsf{D}|}$ such that $M$
deterministically converges to $E[\mathsf{D}(c_{1},\ldots,c_{|\mathsf{D}|})]$.

  * Proof.

Easy. $\Box$

We are finally ready to give the two main lemmas that lead to a proof of
Theorem 3. The first one tells us that any distribution-based approximation is
smaller than the sampling based semantics:

###### Lemma 46

If $M\Rightarrow_{n}\mathscr{D}$, then $\mathscr{D}\leq\llbracket
M\rrbracket_{\mathbb{S}}$.

  * Proof.

By induction on $n$:

    * •

If $n=0$, then $\mathscr{D}$ is necessarily $\mathbf{0}$, and we are done.

    * •

About the inductive case, let’s distinguish three cases depending on the three
cases of Lemma 45, applied to $M$:

      * •

If $M$ deterministically diverges, then by Lemma 42,
$\mathscr{D}\leq\llbracket M\rrbracket=\llbracket M\rrbracket_{\mathbb{S}}$.

      * •

If $M$ deterministically converges to a generalized value $G$, then by Lemma
43 and Lemma 44, it holds that

$\mathscr{D}\leq\llbracket M\rrbracket=\llbracket
G\rrbracket=\delta(G)=\llbracket G\rrbracket_{\mathbb{S}}=\llbracket
M\rrbracket_{\mathbb{S}}.$

      * •

If $M$ deterministically converges to $E[\mathsf{D}(\vec{c})]$, let
$\mathscr{E}$ be such that
$E[\mathsf{D}(\vec{c})]\Rightarrow_{n+1}\mathscr{E}$. By Lemma 43 and Lemma 40
we have, by induction hypothesis, that

$\displaystyle\mathscr{D}(A)\leq\mathscr{E}(A)$
$\displaystyle=\int\mathscr{F}_{N}(A)\;E\\{\mu_{\mathsf{D}}(\vec{c})\\}(dN)$
$\displaystyle\leq\int\llbracket
N\rrbracket_{\mathbb{S}}(A)\;E\\{\mu_{\mathsf{D}}(\vec{c})\\}(dN)$
$\displaystyle=\llbracket M\rrbracket_{\mathbb{S}}$

where $N\Rightarrow_{n}\mathscr{F}_{N}$. $\Box$

The second main lemma tells us that if we limit our attention to traces of
length at most $n$, then we stay below distribution-based semantics:

###### Lemma 47

For every $n\in\mathbb{N}$, $\llbracket
M\rrbracket_{\mathbb{S}}^{n}\leq\llbracket M\rrbracket$.

  * Proof.

By induction on $n$:

    * •

In the base case, then let us distinguish three cases depending on the three
cases of Lemma 45, applied to $M$:

      * •

If $M$ deterministically diverges, then by Lemma 42, $\llbracket
M\rrbracket_{\mathbb{S}}^{0}\leq\llbracket M\rrbracket_{\mathbb{S}}=\llbracket
M\rrbracket$.

      * •

If $M$ deterministically converges to a generalized value $G$, then by Lemma
43 and Lemma 44, it holds that

$\llbracket M\rrbracket_{\mathbb{S}}^{0}=\llbracket
G\rrbracket_{\mathbb{S}}^{0}\leq\llbracket
G\rrbracket_{\mathbb{S}}=\delta(G)=\llbracket G\rrbracket=\llbracket
M\rrbracket.$

      * •

If $M$ deterministically converges to $E[\mathsf{D}(\vec{c})]$, then
$\llbracket M\rrbracket_{\mathbb{S}}^{0}=\llbracket
E[\mathsf{D}(\vec{c})]\rrbracket_{\mathbb{S}}^{0}=\mathbf{0}\leq\llbracket
M\rrbracket$.

    * •

About the inductive case, let us again distinguish three cases depending on
the three cases of Lemma 45, applied to $M$:

      * •

If $M$ deterministically diverges, then by Lemma 42, $\llbracket
M\rrbracket_{\mathbb{S}}^{n+1}\leq\llbracket
M\rrbracket_{\mathbb{S}}=\llbracket M\rrbracket$.

      * •

If $M$ deterministically converges to a generalized value $G$, then by Lemma
43 and Lemma 44, it holds that

$\llbracket M\rrbracket_{\mathbb{S}}^{n+1}=\llbracket
G\rrbracket_{\mathbb{S}}^{n+1}\leq\llbracket
G\rrbracket_{\mathbb{S}}=\delta(G)=\llbracket G\rrbracket=\llbracket
M\rrbracket.$

      * •

If $M$ deterministically converges to $E[\mathsf{D}(\vec{c})]$, by Lemma 43
and Lemma 40 we have, by induction hypothesis, that

$\displaystyle\llbracket M\rrbracket_{\mathbb{S}}^{n+1}(A)$
$\displaystyle=\llbracket
E[\mathsf{D}(\vec{c})]\rrbracket_{\mathbb{S}}^{n+1}(A)$
$\displaystyle=\int\llbracket
N\rrbracket_{\mathbb{S}}^{n}(A)\;E\\{\mu_{\mathsf{D}}(\vec{c})\\}(dN)$
$\displaystyle\leq\int\llbracket
N\rrbracket(A)\;E\\{\mu_{\mathsf{D}}(\vec{c})\\}(dN)$
$\displaystyle=\llbracket M\rrbracket.$

$\Box$

  * Restatement of Theorem 3. $\llbracket M\rrbracket_{\mathbb{S}}=\llbracket M\rrbracket$.

  * Proof.

$\displaystyle\llbracket M\rrbracket_{\Rightarrow}$
$\displaystyle=\sup_{n\in\mathbb{N}}\\{\mathscr{D}\mid M\to_{n}\mathscr{D}\\}$
(by definition) $\displaystyle\leq\llbracket M\rrbracket_{\mathbb{S}}$ (by
Lemma 46) $\displaystyle=\sup_{n\in\mathbb{N}}\llbracket
M\rrbracket_{\mathbb{S}}^{n}$ (by Lemma 38) $\displaystyle\leq\llbracket
M\rrbracket$ (by Lemma 47) $\displaystyle=\llbracket
M\rrbracket_{\Rightarrow}$ (by Theorem 2)

$\Box$

###### Corollary 1

The measures $\langle\\!\langle M\rangle\\!\rangle$ and $\langle\\!\langle
M\rangle\\!\rangle^{\\!\mathcal{V}}$ are sub-probability distributions.

###  4.7 An Application of the Distribution-Based Semantics

It is routine to show that for all values $V$, it holds that
${\llbracket\mathtt{score}(V)\rrbracket}\rvert_{\mathcal{V}}={\llbracket
MV\rrbracket}\rvert_{\mathcal{V}}$, where $M$ is the term

$\displaystyle\lambda x.$ $\displaystyle\mathtt{if}\;(0<x)\land(x\leq 1)$
$\displaystyle\mathtt{then}\;(\mathtt{if}\ {\mathit{flip}(x)}\ \mathtt{then}\
{\texttt{true}}\ \mathtt{else}\ {\mathtt{fail}})$
$\displaystyle\mathtt{else}\;\mathtt{fail}$

This shows that even though $\mathtt{score}(V)$ and $MV$ _do not_ have the
same sampling-based semantics, they can be used interchangeably whenever only
their extensional, distribution-based behaviour on values is important. We use
the equation to our advantage by encoding soft constraints with score instead
of flip (as discussed in Section 2.5), as the fewer the nuisance parameters
the better for inference.

Whenever the stronger equation
$\llbracket\mathtt{score}(V)\rrbracket=\llbracket MV\rrbracket$ is needed, we
could replace $M$ by the following one:

$\displaystyle\lambda x.$ $\displaystyle\mathtt{if}\;(0<x)\land(x\leq 1)$
$\displaystyle\mathtt{then}\;(\mathtt{if}\ {\mathit{flip}(x)}\ \mathtt{then}\
{\texttt{true}}\ \mathtt{else}\ {\Omega})$
$\displaystyle\mathtt{else}\;\mathtt{fail}$

###  4.8 Rejection Sampling

The same (normalized) distribution on successful runs would be obtained by re-
evaluating the entire program from the beginning whenever the Boolean
predicate fails, as in:

fix f. λ⋆. let …inif b then n else f 0f 0

This corresponds to a basic inference algorithm known as _rejection sampling_.

###  4.9 Motivation for 1-Bounded Scores

Recall that we only consider $\mathtt{score}(c)$ for $c\in(0,1]$. Admitting
$\mathtt{score}(2)$ (say), we exhibit an anomaly by constructing a recursive
program that intuitively terminates with probability 1, but where the expected
value of its score is infinite. Let

$\mathit{inflate}:={}\mathit{fix}\ f\ \lambda x.\\\ \mathtt{if}\
{\mathit{flip}(0.5)}\ \mathtt{then}\ {\mathtt{score}(2);(f\ x)}\
\mathtt{else}\ {x}.$ $\mathit{inflate}:={}\mathit{fix}\ f\ \lambda
x.\mathtt{if}\ {\mathit{flip}(0.5)}\ \mathtt{then}\ {\mathtt{score}(2);(f\
x)}\ \mathtt{else}\ {x}.$

Since
$\llbracket\mathtt{score}(2)\rrbracket=\llbracket\mathtt{fail}\rrbracket$ we
have $\llbracket\mathit{inflate}\
V\rrbracket=0.5\cdot\delta(V)+0.5\cdot\delta(\mathtt{fail})$ for any $V$.
However, evaluating $\mathit{inflate}\ V$ in a version of our trace semantics
where the argument to score may be 2 yields

$\langle\\!\langle\mathit{inflate}\
V\rangle\\!\rangle(\mathbb{S}_{n})=\sum_{k=1}^{n}1/2=n/2$

and so there $\llbracket\mathit{inflate}\ V\rrbracket_{\mathbb{S}}(A)=\infty$
if $V\in A$, otherwise 0.

More strikingly, in the modified semantics we would also have
$\llbracket\mathit{inflate}\
\textsf{Gaussian}(0,1)\rrbracket_{\mathbb{S}}([q,r])=\infty$ for all real
numbers $q<r$. These examples show that even statically bounded scores in
combination with recursion may yield return value measures that are not even
$\sigma$-finite, causing many standard results in measure theory not to apply.
For this reason, we restrict attention to positive scores bounded by one. An
alternative approach would be to admit unbounded scores, and restrict
attention to those programs for which $\llbracket
M\rrbracket_{\mathbb{S}}(\mathcal{V})<\infty$.

##  5 Inference

In this section, we present a variant of the Metropolis-Hastings (MH)
algorithm [26, 17] for sampling the return values of a particular closed term
$M\in C\Lambda$. This algorithm yields consecutive samples from a Markov chain
over $\mathbb{S}$, such that the density of the samples $s$ converges to
$\mathbf{P}^{\mathcal{V}}_{\\!M}(s)$ up to normalization. We can then apply
the function $\mathbf{O}_{M}$ to obtain the return value of $M$ for a given
trace.

We prove correctness of this algorithm by showing that as the number of
samples goes to infinity, the distribution of the samples approaches the
distributional semantics of the program.

###  5.1 A Metropolis-Hastings Sampling Algorithm

We begin by outlining a generic Metropolis-Hastings algorithm for
probabilistic programs, parametric in a proposal density function $q(s,t)$.
The algorithm consists of three steps:

  * 1.

Pick an initial state $s$ with $\mathbf{P}^{\mathcal{V}}_{\\!M}(s)\neq 0$
(e.g., by running $M$).

  * 2.

Draw the next state $t$ at random with probability density $q(s,t)$.

  * 3.

Compute $\alpha$ as below.

$\alpha=\min\left(1,\frac{\mathbf{P}^{\mathcal{V}}_{\\!M}(t)}{\mathbf{P}^{\mathcal{V}}_{\\!M}(s)}\cdot\frac{q(t,s)}{q(s,t)}\right)$
(1)

    * •

With probability $\alpha$, output $t$ and repeat from 2 with $s:=t$.

    * •

Otherwise, output $s$ and repeat from 2 with $s$ unchanged.

The formula used for the number $\alpha$ above is often called the Hastings
_acceptance probability_. Different probabilistic programming language
implementations use different choices for the density $q$ above, based on
pragmatics. The trivial choice would be to let
$q(s,t)=\mathbf{P}^{\mathcal{V}}_{\\!M}(t)$ for all $s$, which always yields
$\alpha=1$ and so is equivalent to rejection sampling. We here define another
simple density function $q$ (based on Hur et al. [19]), giving emphasis to the
conditions that it needs to satisfy in order to prove the convergence of the
Markov chain given by the Metropolis-Hastings algorithm (Theorem 4).

###  5.2 Proposal Density

In the following, let $M$ be a fixed program. Given a trace
$s=[c_{1},\dots,c_{n}]$, we write $s_{i..j}$ for the trace
$[c_{i},\dots,c_{j}]$ when $1\leq i\leq j\leq n$. Intuitively, the following
procedure describes how to obtain the proposal kernel density ($q$ above):

  * 1.

Given a trace $s$ of length $n$, let $t=[t_{1},\dots,t_{n}]$ where each
$t_{i}$ is drawn independently from a normal distribution with mean $s_{i}$
and variance $\sigma^{2}$, and let $p_{i}$ be the probability density of
$t_{i}$.

  * 2.

Let $k\leq n$ be the largest number such that
$(M,1,t_{1..k})\Rightarrow(M^{\prime},w,[])$. There are three cases:

    * •

If $k=n$, run $M^{\prime}\Downarrow_{t^{\prime}}^{w^{\prime}}V$, and let
$q(s,t@t^{\prime})=p_{1}\dots p_{n}w^{\prime}$.

    * •

If $k<n$ and $M^{\prime}\Downarrow_{[]}^{1}V$, let $q(s,t_{1..k})=p_{1}\dots
p_{k}$.

    * •

Otherwise, let $q(s,t_{1..k})=0$ and propose the trace $[]$.

To define this density formally, we first give a function that partially
evaluates $M$ given a trace. Let $\mathtt{peval}$ be a function taking a
closed term $M$ and trace $s$ and returning the closed term $M^{\prime}$
obtained after applying just as many reduction steps to $M$ as required to use
up the entire trace $s$ (or $\mathtt{fail}$ if this cannot be done).

$\mathtt{peval}(M,s)=\begin{cases}M&\text{if~{}}s=[]\\\ M^{\prime}&\text{if}\
(M,1,s)\Rightarrow(M_{k},w_{k},s_{k})\to(M^{\prime},w^{\prime},[])\\\
&\text{~{}for some~{}}M_{k},w_{k},s_{k},w^{\prime}\text{~{}such
that~{}}s_{k}\neq[]\\\ \mathtt{fail}&\text{otherwise}\end{cases}$

###### Lemma 48

For every $M\in C\Lambda,c\in\mathbb{R},s\in\mathbb{S}$,
$\mathtt{peval}(\mathtt{peval}(M,[c]),s)=\mathtt{peval}(M,c\mathrel{::}s)$.

  * Proof.

By splitting the equality into two inequalities, substituting the alternative
definition of $\mathtt{peval}$ (described in the appendix) and using Scott
induction. $\Box$

###### Lemma 49

For every $M\in C\Lambda,c\in\mathbb{R},s\in\mathbb{S}$,
$\mathtt{peval}(\mathtt{peval}(M,s),t)=\mathtt{peval}(M,s@t)$.

  * Proof.

By induction on $|s|$, with appeal to Lemma 48. $\Box$

###  5.3 A Metropolis-Hastings Proposal Kernel

We define the transition kernel $Q(s,A)$ of the Markov chain constructed by
the algorithm by integrating a density $q(s,t)$ (as a function of $t$) over
$A$ with respect to the stock measure $\mu$ on program traces. For technical
reasons, we need to ensure that $Q$ is a probability kernel, i.e., that
$Q(s,\mathbb{S})=1$ for all $s$. We normalize $q(s,\cdot)$ by giving non-zero
probability $q(s,[])$ to transitions ending in $[]$ (which is not a completed
trace of $M$ by assumption). All this is in Figure 12.

$\displaystyle q(s,t)=\;$
$\displaystyle(\Pi_{i=1}^{k}\operatorname{pdf}_{\mathsf{Gaussian}}(s_{i},\sigma^{2},t_{i}))\cdot\mathbf{P}^{\mathcal{V}}_{\\!N}(t_{k+1..\lvert{t}\rvert})$
$\displaystyle\mbox{if~{}}\lvert{t}\rvert\neq
0,\mbox{~{}where~{}}k=\min\\{\lvert{s}\rvert,\lvert{t}\rvert\\}$
$\displaystyle\mbox{and~{}}N=\texttt{peval}(M,t_{1..k})$ $\displaystyle
q(s,[])=\;$ $\displaystyle