A Lambda-Calculus Foundation for
Universal Probabilistic Programming∗
Johannes Borgström†

Ugo Dal Lago‡

Andrew D. Gordon§

arXiv:1512.08990v5 [] 23 Jan 2017

Marcin Szymczak¶
January 24, 2017

Abstract
We develop the operational semantics of an untyped probabilistic λ-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 λ-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.

∗ 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.
† Uppsala University
‡ University of Bologna & INRIA
§ Microsoft Research and University of Edinburgh
¶ University of Edinburgh

1

Contents
1 Introduction
1.1 Universal Probabilistic Programming in Church
1.2 Problem 1: Semantics of Church Queries . . . .
1.3 Problem 2: Correctness of Trace MCMC . . . . .
1.4 Contributions of the Paper . . . . . . . . . . . .
1.5 Structure of the Paper . . . . . . . . . . . . . . .

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

3
3
4
4
5
5

2 A Foundational Calculus for Church
2.1 Syntax of the Calculus . . . . . . . .
2.2 Big-step Sampling-based Semantics .
2.3 Encoding Church . . . . . . . . . .
2.4 Example: Geometric Distribution . .
2.5 Soft Constraints and score . . . . .
2.6 Example: Linear Regression . . . . .

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

6
6
7
8
9
9
10

3 Sampling-Based Operational Semantics
3.1 Small-step Sampling-based Semantics . . . . . . . . . . . . . . . .
3.2 Some Measure-Theoretic Preliminaries. . . . . . . . . . . . . . . . .
3.3 Measure Space of Program Traces . . . . . . . . . . . . . . . . . .
3.4 Distributions hhM ii and JM KS Given by Sampling-Based Semantics

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

10
10
18
19
21

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

4 Distribution-Based Operational Semantics
4.1 Sub-Probability Kernels . . . . . . . . . . . . . . . . . . . . . . .
4.2 Approximation Small-Step Semantics . . . . . . . . . . . . . . . .
4.3 Approximation Big-Step Semantics . . . . . . . . . . . . . . . . .
4.4 Beyond Approximations . . . . . . . . . . . . . . . . . . . . . . .
4.5 Geometric Distribution, Revisited . . . . . . . . . . . . . . . . . .
4.6 Distribution-based and Sampling-based Semantics are Equivalent
4.7 An Application of the Distribution-Based Semantics . . . . . . .
4.8 Rejection Sampling . . . . . . . . . . . . . . . . . . . . . . . . . .
4.9 Motivation for 1-Bounded Scores . . . . . . . . . . . . . . . . . .

.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.

21
22
22
25
26
28
28
31
31
32

5 Inference
5.1 A Metropolis-Hastings Sampling Algorithm
5.2 Proposal Density . . . . . . . . . . . . . . .
5.3 A Metropolis-Hastings Proposal Kernel . .
5.4 Transition Kernel of the Markov Chain . . .
5.5 Correctness of Inference . . . . . . . . . . .
5.6 Examples . . . . . . . . . . . . . . . . . . .

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

32
32
33
33
34
35
36

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

6 Related Work

38

7 Conclusions and Remarks

40

A Proofs of Measurability
A.1 Deterministic reduction as a measurable function
A.2 Small- step reduction as a measurable function .
A.3 Measurability of P and O . . . . . . . . . . . . .
A.4 Measurability of peval . . . . . . . . . . . . . . .
A.5 Measurability of q and Q . . . . . . . . . . . . .

2

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

.
.
.
.
.

40
44
46
47
50
55

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 x1 e1 ) ...( define xn en ) eq ec )

The query denotes the distribution given by the probabilistic expression eq , given variables xi
defined by potentially probabilistic expressions ei , constrained so that the boolean predicate ec 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) geometric1
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 See

http://forestdb.org/models/geometric.html.

3

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 λ-calculi do not
rigorously treat the combination of these features.
To address the problem we introduce a call-by-value λ-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 λ-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
λ-abstraction) or the exception fail, used to model a failing hard constraint).
• Figure 4 defines small-step relation (M, w, s) → (M ′ , w′ , s′ ).
• Figure 1 defines the big-step relation M ⇓sw G.
For example, if M is the λ-term for our geometric distribution example and we have M ⇓sw G
then there is n ≥ 0 such that:
• the trace has the form s = [q1 , . . . , qn+1 ] where each qi is a probability, and qi < 0.5 if and
only if i = n + 1. (A sample qi ≥ 0.5 is tails; a sample qi < 0.5 is heads.)
• the result takes the form G = n if n > 1, and otherwise G = fail (the failure of a hard
constraint leads to 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 λ-terms and let D
range over distributions, that is, sub-probability Borel measures on terms of the λ-calculus. We
define JM KS 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 6 defines a family of small-step relations M ⇒n D.
• Figure 7 defines a family of big-step relations M ⇓n D.
These step-indexed families are approximations to their suprema, distributions written as JM K⇒
and JM K⇓ . By Theorem 2 we have JM K⇒ = JM K⇓ . 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 JM KS = JM K⇒ .

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
4

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, s0 , s1 , s2 , . . . . 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 JM K⇒ conditional on success, that is, that the computation terminates and yields a value (not
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 σ-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 λ-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 λ-calculus (Theorem 4).
The only previous work on formal semantics of λ-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 λ-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 λ-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 ⇓sw G, and small-step semantics, (M, w, s) →
(M ′ , w′ , s′ ), which are equivalent by Theorem 1. We define a distribution JM K 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 ⇒n D) and big-step (M ⇓n D) styles, which by Theorem 2 are equivalent, and define the

5

meaning JM K 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 JM KS = JM K
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 λ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 ∈ R. We use 0 and 1 to represent false and true,
respectively. Let I be a countable set of distribution identifiers (or simply distributions). Metavariables for distributions are D, E. Each distribution identifier D has an integer arity |D| ≥ 0, and
defines a density function pdf D : R|D|+1 → [0, ∞) of a sub-probability kernel. For example, a draw
(rnd()) from the uniform distribution on the unit interval has density pdf rnd (c) = 1 if c ∈ [0, 1]
and otherwise 0, while a draw (Gaussian(m, v)) from the Gaussian distribution with mean m and
(c−m)2 √
variance v has density pdf Gaussian (m, v, c) = 1/(e 2v
2vπ) 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 σg : R|g| → 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 X .
V ::= c
M, N ::= V

|

|

|

x

|

λx.M

M N

|

D(V1 , . . . , V|D| )

if V then M else N

|

|

g(V1 , . . . , V|g| )

score(V )

|

fail

The term fail acts as an exception and models a failed hard constraint. The term score(c)
models a soft constraint, and is parametrized on a positive probability c ∈ (0, 1]. As usual, free
occurrences of x inside M are bound by λ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
~ /~x}, where ~x is a sequence of variables
denoted M {V /x}. This can be easily generalized to M {V
and V~ is a sequence of values (of the same length). Let Λ denote the set of all terms, and CΛ
the set of closed terms. The set of all closed values is V, and we write Vλ for V \ R. Generalized
values G, H are elements of the set GV = V ∪ {fail}, i.e., generalized values are either values
or fail. Finally, erroneous redexes, ranged over by metavariables like T, R, are closed terms in
one of the following five forms:
• c M.

6

G ∈ GV
G

[]
⇓1

G

(Eval Val)

pdf D (~c, c) = 0
[c]

D(~c) ⇓0 fail

w = pdf D (~c, c)
D(~c)

[c]
⇓w

N ⇓sw22 V

P [V /x] ⇓sw33 G

s1 @s2 @s3
M N ⇓w
G
1 ·w2 ·w3

M ⇓sw fail
(Eval Appl Raise1)
M N ⇓sw fail
M ⇓sw11 λx.P

c

(Eval Appl)

M ⇓sw c
(Eval Appl Raise2)
M N ⇓sw fail

N ⇓sw22 fail

s1 @s2
M N ⇓w
fail
1 ·w2

(Eval Random)

[]
g(~c) ⇓1 σg (~c) (Eval Prim)

(Eval Random Fail)

M ⇓sw11 λx.P

w>0

(Eval Appl Raise3)

M ⇓sw G
(Eval If True)
if true then M else N ⇓sw G

c ∈ (0, 1]
score(c)

[]
⇓c

N ⇓sw G
(Eval If False)
if false then M else N ⇓sw G
T is an erroneous redex
(Eval Fail)
[]
T ⇓1 fail

(Eval Score)

true

Figure 1: Sampling-Based Big Step Semantics

•
•
•
•

D(V1 , . . . , V|D| ) where at least one of the Vi is a λ-abstraction.
g(V1 , . . . , V|g| ) where at least one of the Vi is a λ-abstraction.
if V then M else N , where V is neither true nor false.
score(V ), where V ∈
/ (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 ⇓sw 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 ⇓sw 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 [c1 , . . . , cn ] of reals of arbitrary
length. We let M ⇓sw G be the least relation closed under the rules in Figure 1. The (Eval
Random) rule replaces a random draw from a distribution D parametrized by a vector ~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 D(~c) at c. (Eval Random Fail) throws an exception
if c is outside the support of the corresponding distribution. Meanwhile, (Eval Score), applied
to score(c), sets the weight to c and returns a dummy value. The applications of soft constraints
using score are described in Section 2.5.
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 subcompu-

7

hcie = c
hxie = x
hg e1 , . . . , en ie =
let x1 = e1 in . . . let xn = en in g(x1 , . . . , xn )
where x1 , . . . , xn ∈
/ fv(e1 ) ∪ · · · ∪ fv (en )
hD e1 , . . . en ie =
let x1 = e1 in . . . let xn = en in D(x1 , . . . , xn )
where x1 , . . . , xn ∈
/ fv(e1 ) ∪ · · · ∪ fv (en )
hlambda () eie = λx.heie where x ∈
/ fv (e)
hlambda x eie = λx.heie
hlambda (x1 . . . xn ) eie = λx1 .hlambda (x2 . . . xn ) eie
he1 e2 ie = he1 ie he2 ie
he1 e2 . . . en ie = h(e1 e2 ) . . . en ie
hif e1 e2 e3 ie = let x = e1 in (if x then he2 ie else he3 ie )
where x ∈
/ fv (e2 ) ∪ fv (e3 )
hquery (define x1 e1 ) . . . (define xn en ) eout econd i =
let x1 = (fix x1 .he1 ie ) in
...
let xn = (fix xn .hen ie ) in
let b = econd in
if b then eout else fail

Figure 2: Translation of Church

tations 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:
e ::= c

|

|

x

|

(g e1 . . . en )

(lambda (x1 . . . xn ) e)

|

|

(D e1 . . . en )

|

(if e1 e2 e3 )

(e1 e2 . . . en )

d ::= (define x e)
q ::= (query d1 . . . dn e econd )
To make the translation more intuitive, it is convenient to add to the target language a letexpression of the form let x = M in N , that can be interpreted as syntactic sugar for (λx.N ) M ,
and sequencing M ; N that stands for λ⋆.N M where ⋆ as usual stands for a variable that does
not appear free in any of the terms under consideration.
The rules for translating Church expressions to the calculus are shown in Figure 2, where fv (e)
denotes the set of free variables in expression e and fix x.M is a call-by-value fixpoint combinator
λy.Nfix Nfix (λx.M )y where Nfix is λz.λw.w(λy.((zz)w)y). Observe that (fix x.M )V evaluates to
M {(fix x.M )/x}V deterministically. We assume that for each distribution identifier D of arity k,
there is a deterministic function pdf 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.
8

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) in
let geometric =
(fix g.
λp. (let y = rnd() < p in
if y then 0 else 1 + (g p))) in
let n = fix n′ .geometric 0.5 in
let b = n > 1 in
if 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 geometric 0.5.
It can be shown (by repeatedly applying (Eval Appl)) that for any lambda-abstraction λx.M ,
M {(fix x.M )/x} V ⇓sw G if and only if (fix x.M ) V ⇓sw 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 in
if y then 0 else 1 + (. . . ).
[0.7]

For the first random draw, we have rnd() ⇓1 0.7 by (Eval Random) (because the density of rnd
[0.7]
is 1 on the interval [0, 1]) and so (Eval Prim) gives rnd() < 0.5 ⇓1
false. After unfolding the
[0.8]
false and
recursion two more times, evaluating the subsequent “flips” yields rnd() < 0.5 ⇓1
[0.3]
rnd() < 0.5 ⇓1
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
[0.7,0.8,0.3]
arrive at geometric 0.5 ⇓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 |x − c|, for instance,
condition x c M := if flip(exp(−(x − c)2 )) then M else fail.
Then condition x c M has the effect of continuing as M with probability exp(−(x − c)2 ), and
otherwise terminating execution. In the context of a sampling-based semantics, it has the effect of
9

adding a uniform sample from [0, 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 gradientbased methods of inference (e.g., Homan and Gelman [18]). Using score, the above conditioning
operator can be redefined as
score-condition x c M := score(exp(−(x − c)2 )); M

2.6

Example: Linear Regression

For an example of soft constraints, consider the ubiquitous linear regression model y = m · x + b +
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 query2 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 x1 . . . xn ) e) for (define f
(lambda (x1 . . . xn ) e), and use and for multiadic conjunction.)
( query
( define
( define
( define
( define

( sqr x ) (* x x ) ) )
( squash x y ) ( exp (- ( sqr (- x y ) ) ) ) )
( flip p ) (< ( rnd ) p ) )
( 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 ys are (soft) equal to k · 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 score(−) in
our λ-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 ::= [·]
2 Cf.

|

EM

|

(λx.M )E

http://forestdb.org/models/linear-regression.html.

10

det

E[g(~c)] −−→ E[σg (~c)]
det

E[(λx.M ) V ] −−→ E[M {V /x}]
det

E[if 1 then M2 else M3 ] −−→ E[M2 ]
det

E[if 0 then M2 else M3 ] −−→ E[M3 ]
det

E[T ] −−→ E[fail]
det

E[fail] −−→ fail if E is not [·]
Figure 3: Deterministic Reduction.

We let C be the set of all closed evaluation contexts, i.e., where every occurrence of a variable x
is as a subterm of λx.M . The term obtained by replacing the only occurrence of [·] in E by M is
indicated as E[M ]. Redexes are generated by the following grammar:
R ::= (λx.M )V

|

|

fail

|

|

D(~c)

|

g(~c)

|

score(c)

if true then M else N

if false then M else N

|

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 = fail, then E is proper,
that is, E 6= [·].


Proof. This is an easy induction on the structure of M .
det

Deterministic reduction is the relation −−→ on closed terms defined in Figure 3.
det

det

Lemma 2 If M −−→ M ′ and M −−→ M ′′ then M ′ = M ′′ .
det

Proof. Since M −−→ M ′ implies that M is not a generalized value, Lemma 1 states that M =
E[R] for some unique E, R. If R = fail, then E is proper and E[R] can only reduce to fail.
det

Otherwise, it follows immediately by inspection of the reduction rules that E[R] −−→ E[N ] for
some N that is uniquely determined by the redex R.

Let us define composition of contexts E ◦ E ′ inductively as:
[ ] ◦ E′

(E M ) ◦ E ′
((λx.M ) E) ◦ E ′

,

E′

,
,

(E ◦ E ′ ) M
(λx.M ) (E ◦ E ′ )

Lemma 3 (E ◦ E ′ )[M ] = E[E ′ [M ]].


Proof. By induction on the structure of E.
det

det

Lemma 4 If E[R] −−→ E[N ], then R −−→ N .
Proof. By case analysis on the deterministic reduction rules.
11

det

M −−→ N
(Red Pure)
(M, w, s) → (N, w, s)

c ∈ (0, 1]
(Red Score)
(E[score(c)], w, s) → (E[true], c · w, s)

w′ = pdf D (~c, c)
w′ > 0
(Red Random)
(E[D(~c)], w, c :: s) → (E[c], w · w′ , s)

pdf D (~c, c) = 0
(Red Random Fail)
(E[D(~c)], w, c :: s) → (E[fail], 0, s)
Figure 4: Small-step sampling-based operational semantics

det

det

Lemma 5 For any E and M such that M 6= E ′ [fail], if M −−→ M ′ then E[M ] −−→ E[M ′ ].
Proof. Standard, using Lemmas 1 and 2.
det
Since M −−→ M ′ , M is not a generalized value. By Lemma 1, M = E ′ [R] for some E ′ , R.
det
By assumption, R 6= fail, so by inspection of the reduction rules E ′ [R] −−→ E ′ [N ] for some
N . By Lemma 2, E ′ [N ] = M ′ . By Lemma 3, E[M ] = (E ◦ E ′ )[R] and E[M ′ ] = (E ◦ E ′ )[N ].
det

det

Since Lemma 4 gives R −−→ N , by case analysis on the derivation of R −−→ N we can show
det
det
that (E ◦ E ′ )[R] −−→ (E ◦ E ′ )[N ], which implies E[M ] −−→ E[M ′ ].

Lemma 6 If (M, w, s) → (M ′ , w′ , s′ ) and (M, w, s) → (M ′′ , w′′ , s′′ ), then M ′ = M ′′ , w′ = w′′
and s′′ = s′ .
Proof. By case analysis. Since there is no rule that reduces generalized values, (M, w, s) →
(M ′ , w′ , s′ ) implies that M ∈
/ GV, so by Lemma 1, M = E[R] for some unique E, R.
• If (M, w, s) → (M ′ , w′ , s′ ) was derived with (Red Pure), then M = E[R], where R 6= D(c)
and R 6= score(c), which implies that (M, w, s) → (M ′′ , w′′ , s′′ ) must also have been derived
det

det

with (Red Pure). Hence, we have w′′ = w′ = w, s′′ = s′ = s, M −−→ M ′ and M −−→ M ′′ .
By Lemma 2, M ′′ = M ′ , as required.
• If (M, w, s) → (M ′ , w′ , s′ ) was derived with (Red Random), then M = E[D(~c)], s = c :: s∗
and pdf D (~c, c) > 0. Hence, (M, w, s) → (M ′′ , w′′ , s′′ ) must also have been derived with (Red
Random), and so M ′′ = M ′ = E[c], s′′ = s′ = s∗ and w′′ = w′ = w pdf D (~c, c), as required.
The (Red Random Fail) case is analogous.
• If (M, w, s) → (M ′ , w′ , s′ ) was derived with (Red Score), then M = E[score(c)] and c ∈
(0, 1], so (M, w, s) → (M ′′ , w′′ , s′′ ) must also have been derived with (Red Score). Hence
M ′′ = M ′ = E[true], w′′ = w′ = c · w and s′′ = s′ = s.


Rules of small-step reduction are given in Figure 4. We let multi-step reduction be the inductively
defined relation (M, w, s) ⇒ (M ′ , w′ , s′ ) if and only if (M, w, s) = (M ′ , w′ , s′ ) or (M, w, s) →
(M ′′ , w′′ , s′′ ) ⇒ (M ′ , w′ , s′ ) for some M ′′ , w′′ , s′′ . 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) ⇒ (G′ , w′ , s′ ) and (M, w, s) ⇒ (G′′ , w′′ , s′′ ), then G′ = G′′ , w′ = w′′
and s′ = s′′ .
Proof. By induction on the derivation of (M, w, s) ⇒ (G′ , w′ , s′ ), with appeal to Lemma 6.

12

• Base case: (M, w, s) = (G′ , w′ , s′ ). Generalized values do not reduce, so G′′ = G′ = G,
w′′ = w′ = w and s′′ = s′ = s.
• Induction step: (M, w, s) → (M̂ , ŵ, ŝ) ⇒ (G′ , w′ , s′ ). Since M 6= G′′ , we also have (M, w, s) →
(M ∗ , w∗ , s∗ ) ⇒ (G′′ , w′′ , s′′ ).
By Lemma 6, (M ∗ , w∗ , s∗ ) = (M̂ , ŵ, ŝ), and so by induction hypothesis, (G′′ , w′′ , s′′ ) =
(G′ , w′ , s′ ), as required.

Lemma 8 For any E and M such that M 6= E ′ [fail], if (M, w, s) → (M ′ , w′ , s′ ) then (E[M ], w, s) →
(E[M ′ ], w′ , s′ )
Proof. By inversion of →, using Lemma 5.
det
• If (M, w, s) → (M ′ , w′ , s′ ) was derived with (Red Pure), then M −−→ M ′ , so by Lemma 5,
det

E[M ] −−→ E[M ′ ], and by (Red Pure), (E[M ], w, s) → (E[M ′ ], w′ , s′ ).
• If (M, w, s) → (M ′ , w′ , s′ ) was derived with (Red Random), then M = E ′ [D(~c)], M ′ = E ′ [c],
s = c :: s′ and w′ = w pdf D (~c, c), where pdf D (~c, c) > 0. By (Red Random) and Lemma 3, we
can derive (E[M ], w, s) → (E[M ′ ], w′ , s′ ). Cases (Red Random Fail) and (Red Score) are
anaologous.


Lemma 9 If (E[R], w, s) → (E[N ], w′ , s′ ) then (R, w, s) → (N, w′ , s′ )
Proof. By case analysis.
det
• If (E[R], w, s) → (E[N ], w′ , s′ ) was derived with (Red Pure), then E[R] −−→ E[N ], so by
det

Lemma 5, R −−→ N , which implies (M, w, s) → (M ′ , w′ , s′ ).
• If (E[R], w, s) → (E[N ], w′ , s′ ) was derived with (Red Random), then R = D(~c), N = c,
s = c :: s′ and w′ = w pdf D (~c, c), where pdf D (~c, c) > 0.
Hence, with (Red Random), we can derive (D(~c), w, s) → (c, w′ , s′ )
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) ⇒ (M ′ , w′ , s′ ) and M ′ 6= fail, then we have (E[M ], w, s) ⇒
(E[M ′ ], w′ , s′ ).
Proof. By induction on the number of steps in the derivation of (M, w, s) ⇒ (M ′ , w′ , s′ ), with
appeal to Lemma 8.
Since M ′ 6= fail, no expression in the derivation chain (other than the last one) can be of the
form E ′ [fail].

Lemma 11 For any E, if (M, w, s) ⇒ (fail, w′ , s′ ) then
(E[M ], w, s) ⇒ (fail, w′ , s′ ).
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 6= [ ]. If (M, w, s) ⇒ (fail, w′ , s′ ) was derived in 0
steps, then M = fail, w′ = w′ and s′ = s, so by (Red Pure), (E[fail], w, s) → (fail, w, s), as
required.
If (M, w, s) ⇒ (fail, w′ , s′ ) was derived in 1 or more steps, then:
• If M = E ′ [fail] and E ′ 6= [ ], then ((E ◦ E ′ )[fail], w, s) → (fail, w′ , s′ ) by (Red Pure).
• Otherwise, there exist M̂ , ŵ, ŝ such that (M, w, s) → (M̂ , ŵ, ŝ) ⇒ (fail, w′ , s′ ), where M ∈
/
GV. By induction hypothesis, (E[M̂ ], ŵ, ŝ) ⇒ (fail, w′ , s′ ) for any E, and by Lemma 8,
(E[M ], w, s) → (E[M̂ ], ŵ, ŝ).


13

Lemma 12 If (M, w, s) ⇒ (M ′ , w′ , s′ ) and w ≥ 0, then w′ ≥ 0.
Proof. By induction on the number of steps in the derivation.
• If (M, w, s) ⇒ (M ′ , w′ , s′ ) was derived in 0 steps, then w′ = w, so w′ ≥ 0.
• If (M, w, s) ⇒ (M ′ , w′ , s′ ) was derived in 1 or more steps, then (M, w, s) → (M ∗ , w∗ , s∗ ) ⇒
(M ′ , w′ , s′ ).
If (M, w, s) → (M ∗ , w∗ , s∗ ) was derived with (Red Pure), then w∗ = w ≥ 0.
If (M, w, s) → (M ∗ , w∗ , s∗ ) was derived with (Red Random), then w∗ = w · w′′ for some
w′′ > 0, so w∗ ≥ 0.
If (M, w, s) → (M ∗ , w∗ , s∗ ) was derived with (Red Score), then w∗ = w · c for some c > 0,
so w′ ≥ 0.
If (M, w, s) → (M ∗ , w∗ , s∗ ) was derived with (Red Random Fail), then w∗ = 0.
In either case, w∗ ≥ 0, so by induction hypothesis, w′ ≥ 0.

Lemma 13 If (M, w, s) → (M ′ , w′ , s′ ) was not derived with (Red Random Fail) and w > 0,
then w′ > 0.
Proof. By inspection (similar to the inductive step in the proof of Lemma 12).
Lemma 14 If (M, w, s) → (M ′ , w′ , s′ ), then for any w∗ ≥ 0, (M, ww∗ , s) → (M ′ , w′ w∗ , s′ )


Proof. By case analysis.
Lemma 15 If (M, w, s) → (M ′ , w′ , s′ ), then for any s∗ , (M, w, s@s∗ ) → (M ′ , w′ , s′ @s∗ )



Proof. By case analysis.

Lemma 16 If (M, w, s) → (M ′ , w′ , s′ ), then there is s∗ such that s = s∗ @s′ and (M, w, s∗ ) →
(M ′ , w′ , [])


Proof. By case analysis.
Lemma 17 If (M, w, s) →k (M ′ , w′ , s′ ), then for any w∗ ≥ 0, (M, ww∗ , s) →k (M ′ , w′ w∗ , s′ )
Proof. By induction on k, with appeal to Lemma 14.



Lemma 18 If (M, w, s) →k (M ′ , w′ , s∗ ), then for any s′ , (M, w, s@s′ ) →k (M ′ , w′ , s∗ @s′ )
Proof. By induction on k, with appeal to Lemma 15.
Lemma 19 If both (M, 1, s) ⇒ (M ′ , w′ , []) and (M ′ , 1, s′ ) ⇒ (M ′′ , w′′ , []), then (M, 1, s@s′ ) ⇒
(M ′′ , w′ · w′′ , []).
Proof. By Lemma 18, (M, 1, s@s′ ) ⇒ (M ′ , w′ , s′ ) and by lemma 12, w′ ≥ 0. Hence, by Lemma
17, (M ′ , w′ , s′ ) ⇒ (M ′′ , w′ w′′ , []), which gives (M, 1, s@s′ ) ⇒ (M ′′ , w′ w′′ , []).

[]

Lemma 20 For any E, E[fail] ⇓1 fail.
Proof. By induction on the structure of E.
• Base case: E = [ ], the result follows by (Eval Val).
• Induction step:
[]
• Case E = (λx.L) E ′ : By induction hypothesis, E ′ [fail] ⇓1 fail, and by (Eval Appl
[]
Raise2), (λx.L) E ′ [fail] ⇓1 fail, as required.
[]
• Case E = E ′ L: By induction hypothesis, E ′ [fail] ⇓1 fail, so by (Eval Appl Raise1),
[]
we get E ′ [fail] L ⇓1 fail.

14

[c]

Lemma 21 For any E, if pdf D (~c, c) = 0, then E[D(~c)] ⇓0 fail.
Proof. By induction on the structure of E.
• Base case: E = [ ], the result follows by (Eval Random Fail).
• Induction step:
[c]
• Case E = (λx.L) E ′ : By induction hypothesis, E ′ [D(~c)] ⇓0 fail, and by (Eval Appl
[]
Raise2), (λx.L) E ′ [D(~c)] ⇓0 fail, as required.
[c]
• Case E = E ′ L: By induction hypothesis, E ′ [D(~c)] ⇓0 fail, so by (Eval Appl Raise1),
[]
we get E ′ [D(~c)] L ⇓0 fail.

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

′

s@s
Lemma 22 If (M, 1, s) → (M ′ , w, []) and M ′ ⇓sw′ G, then M ⇓w·w
′ G.

Proof. By induction on the structure of M .
If M = E[fail] for some E 6= [ ], the result follows immediately by Lemma 20. Now, let us
assume that M 6= E[fail].
• Base case: M = R:
• If M = g(~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 = if true then M2 else M3 : We have (if true then M2 else M3 , 1, []) →
′
(M2 , 1, []). By assumption, M2 ⇓sw′ G. Thus, the desired result holds by (Eval If True).
• Case M = if false then M2 else M3 : analogous to the previous case.
• Case M = (λx.N1 ) V : We have ((λx.N1 ) V, 1, []) → (N1 {V /x}, 1, []). Since (λx.N1 ) and V
′
′
are already values and N1 {V /x} ⇓sw′ G by assumption, (Eval Appl) yields (λx.N1 ) V ⇓sw′
G.
• Case M = D(~c): (M, 1, s) → (M ′ , w, []) must have been derived with (Red Random) or
(Red Random Fail). In the former case, s = [c], M ′ = c, and w = pdf D (~c, c), where
[]
c > 0. The second assumption then takes the form c ⇓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 = score(c), c ∈ (0, 1]: (M, 1, s) → (M ′ , w, []) must have been derived with (Red
Score).so M ′ = true, w = c and s = []. Thus, the result then follows from (Eval Score).
• Induction step: M = E[R], E 6= [ ], R 6= fail:
• Case E = (λx.L) E ′ : M = (λx.L) E ′ [R].
We have ((λx.L) E ′ [R], 1, s) → ((λx.L) E ′ [N ], w, []) for some N , so by lemmas 8 and 9,
′
(E ′ [R], 1, s) → (E ′ [N ], w, []). By assumption, (λx.L) E ′ [N ] ⇓sw′ G.
′
• If (λx.L) E ′ [N ] ⇓sw′ G was derived with (Eval Appl), then E ′ [N ] ⇓sw11 V and (λx.L) V ⇓sw22
s@s1
G, where w′ = w1 w2 and s′ = s1 @s2 . By induction hypothesis, E ′ [R] ⇓ww
V , so (Eval
1
′
s@s′
Appl) gives (λx.L) E [R] ⇓ww′ G, as required.
′
• If (λx.L) E ′ [N ] ⇓sw′ G was derived with (Eval Appl Raise3), then G = fail and
′
s@s′
E ′ [N ] ⇓sw′ fail. By induction hypothesis, E ′ [R] ⇓ww
fail, so by (Eval Appl
′
′
s@s
Raise3), (λx.L) E ′ [R] ⇓ww
′ fail
• Case E = E ′ L: M = E ′ [M ∗ ] L:
We have (E ′ [R] L, 1, s) → (E ′ [N ] L, w, []) for some N , so by lemmas 8 and 9, (E ′ [R], 1, s) →
′
(E ′ [N ], w, []). By assumption, E ′ [N ] L ⇓sw′ G.
′
′
w2
1
• If E ′ [N ] L ⇓sw′ G was derived with (Eval Appl), then E ′ [N ] ⇓w
s1 (λx.N ), L ⇓s2 V
′
′
′
w3
and N [V /x] ⇓s3 G, where w = w1 w2 w3 and s = s1 @s2 @s3 . By induction hypothesis,
s@s1
s@s′
E ′ [R] ⇓ww
(λx.N ′ ), so (Eval Appl) gives E ′ [R] L ⇓ww
′ G, as required.
1
′
• If E ′ [N ] L ⇓sw′ G was derived with (Eval Appl Raise1), then G = fail and
′
s@s′
E ′ [N ] ⇓sw′ fail. By induction hypothesis, E ′ [R] ⇓ww
fail, so by (Eval Appl
′
′
′
s@s
Raise1), E [R] L ⇓ww′ fail
15

′

• If E ′ [N ] L ⇓sw′ G was derived with (Eval Appl Raise3), then E ′ [N ] ⇓sw11 (λx.N ′ ) and
s@s1
L ⇓sw22 fail, where w′ = w1 w2 and s′ = s1 @s2 . By induction hypothesis, E ′ [R] ⇓ww
1
′
s@s
(λx.N ′ ), so (Eval Appl Raise3) gives E ′ [R] L ⇓ww
′ fail, as required.
′
′
• If E ′ [N ] L ⇓sw′ G was derived with (Eval Appl Raise1), then G = fail and N1′ ⇓sw′ c.
s@s′
′
s@s′
By induction hypothesis, E ′ [R] ⇓ww
′ c, so by (Eval Appl Raise1), E [R] L ⇓ww ′
fail.

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 ⇓sw G if and only if (M, 1, s) ⇒ (G, w, []).
Proof. The left to right implication is an induction on the derivation of M ⇓sw G. The most
interesting case is definitely the following:
(Eval Appl)
M ⇓sw11 λx.M ′
N ⇓sw22 V
s1 @s2 @s3
M N ⇓w
G
1 ·w2 ·w3

M ′ [V /x] ⇓sw33 G

By induction hypothesis, (M, 1, s1 ) ⇒ (λx.M ′ , w1 , []), (N, 1, s2 ) ⇒ (V, w2 , []) and (M ′ [V /x], 1, s3 ) ⇒
(G, w3 , []). By Lemma 10 (for E = [ ] N ), (M N, 1, s1 ) ⇒ ((λx.M ′ ) N, w1 , []). By Lemma 10 again
(for E = (λx.M ′ ) [ ]), ((λx.M ′ ) N, 1, s2 ) ⇒ ((λx.M ′ ) V, w2 , []). By Lemma 19, (M N, 1, s1 @s2 ) ⇒
((λx.M ′ ) V, w1 w2 , []) By (Red Pure), ((λx.M ′ ) V, w1 · w2 , []) → (M ′ [V /x], w1 · w2 , []), which
implies (M N, 1, s1 @s2 ) ⇒ ((λx.M ′ ) V, w1 w2 , []) Thus, the desired result follows by Lemma
19.
(Eval Val)
G ∈ GV
• Case:
[]
G ⇓1 G
Here, M = V , w = 1 and s = []. so (M, w0 , s0 ) reduces to (V, w0 , s0 ) in 0 steps by the
small-step semantics.
(Eval Random)
w = pdf D (~c, c)
• Case: w > 0
[c]
D(~c) ⇓w c
By (Red Random) (taking E = [ ]), (D(~c), 1, [c]) → (c, w, []).
(Eval Random Fail)
pdf D (~c, c) = 0
• Case:
[c]
D(~c) ⇓0 fail
By (Red Random Fail) (taking E = [ ]), (D(~c), 1, [c]) → (fail, 0, []).
(Eval Prim)
• Case:

[]

g(~c) ⇓1 σg (~c)
By (Red Pure) (taking E = [ ]), (g(~c), 1, []) → (σg (~c), 1, []).
(Eval Score)
c ∈ (0, 1]
• Case:
[]
score(c) ⇓c true
By (Red Score) (taking E = [ ]), (D(~c), 1, []) → (c, w, []).
(Eval Appl)
M ⇓sw11 λx.M ′
N ⇓sw22 V
• Case: M ′ [V /x]
⇓sw33 G
s1 @s2 @s3
M N ⇓w
G
1 ·w2 ·w3
16

•

•

•

•

•

By induction hypothesis, (M, 1, s1 ) ⇒ (λx.M ′ , w1 , []), (N, 1, s2 ) ⇒ (V, w2 , []) and (M ′ [V /x], 1, s3 ) ⇒
(G, w3 , []).
By Lemma 10 (for E = [ ] N ), (M N, 1, s1 ) ⇒ ((λx.M ′ ) N, w1 , []).
By Lemma 10 again (for E = (λx.M ′ ) [ ]), ((λx.M ′ ) N, 1, s2 ) ⇒ ((λx.M ′ ) V, w2 , []).
By Lemma 19, (M N, 1, s1 @s2 ) ⇒ ((λx.M ′ ) V, w1 w2 , [])
By (Red Pure), ((λx.M ′ ) V, w1 ·w2 , []) → (M ′ [V /x], w1 ·w2 , []), which implies (M N, 1, s1 @s2 ) ⇒
((λx.M ′ ) V, w1 w2 , [])
Thus, the desired result follows by Lemma 19.
(Eval Appl Raise1)
M ⇓sw fail
Case:
M N ⇓sw fail
By induction hypothesis, (M, 1, s) ⇒ (fail, w, []).
By Lemma 11 (with E = [ ] N )), (M N, 1, s) ⇒ (fail, w, []).
(Eval Appl Raise2)
M ⇓sw c
Case:
M N ⇓sw fail
By induction hypothesis, (M, 1, s) ⇒ (c, w, []). By Lemma 10 (with E = [ ] N )), (M N, 1, s) ⇒
(c N, w, []).
By (Red Pure), (c N, w, []) → (fail, w, []).
Thus, (M N, 1, s) ⇒ (fail, w, []).
(Eval Appl Raise3)
s1
λx.M ′
M ⇓w
1
s2
Case: N ⇓w2 fail
s1 @s2
M N ⇓w
fail
1 ·w2
By induction hypothesis, (M, 1, s1 ) ⇒ (λx.M ′ , w1 , []), and (N, 1, s2 ) ⇒ (fail, w2 , []).
By Lemma 10, (M N, 1, s1 ) ⇒ ((λx.M ′ ) N, w1 , []).
By Lemma 11, ((λx.M ′ ) N, 1, s2 ) ⇒ (fail, w2 , []).
Thus, by Lemma 19, (M N, 1, s1 @s2 ) ⇒ (fail, w1 · w2 , []).
(Eval If True)
M2 ⇓sw G
Case:
if true then M2 else M3 ⇓sw G
By (Red Pure) (taking E = [ ]), (if true then M2 else M3 , 1, s) → (M2 , 1, s). By induction
hypothesis, (M2 , 1, s) ⇒ (G, w, []).
Hence (if 1 then M2 else M3 , 1, s) ⇒ (G, w, [])
Case (Eval If False): analogous to (Eval If True)
(Eval Fail)

• Case:

[]

T ⇓1 fail
By (Red Pure), (T, 1, []) → (fail, 1, []).
The right to left implication can be proved by an induction on the length of the derivation of
(M, 1, s) ⇒ (G, w, []).
• Base case: If (M, 1, s) = (G, w, []), then M ⇓w
s G by (Eval Val).
• Induction step: assume (M, 1, s) → (M ′ , w′ , s′ ) →n (G, w, []). If (M, 1, s) → (M ′ , w′ , s′ ) was
derived with (Red Random Fail), then M = E[D(~c)], n = 1, s = [c], G = fail and
w = w′ = pdf D (~c, c) = 0. By Lemma 21, we have M ⇓[ c]0 fail, as required.
Otherwise, by Lemma 13, w′ > 0, so by Lemma 17, (M ′ , 1, s′ ) →n (G, w/w′ , []). By induction
′
hypothesis, M ′ ⇓sw/w′ G. By Lemma 16, (M, 1, s∗ ) → (M ′ , w′ , []), where s = s∗ @s′ .
∗

′

s @s
Therefore, by Lemma 22, M ⇓w
G, and so M ⇓sw G.

As a corollary of Theorem 1 and Lemma 7 we obtain:
Lemma 23 If M ⇓sw G and M ⇓sw′ G′ then w = w′ and G = G′ .

17



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 σ-algebra (over a set X) is a set Σ of subsets of X that contains ∅, and is closed under
complement and countable union (and hence is closed under countable intersection). Let the σalgebra generated by S, written σ(S), be the set σ(S) S ⊆ P(X), that is the least σ-algebra over
∪S that is a superset of S. In other words, σ(S) is the least set such that:
1. we have S ⊆ σ(S) and ∅ ∈ σ(S); and
2. ((∪S) \ A) ∈ σ(S) if A ∈ σ(S); and
3. ∪i∈N Ai ∈ σ(S) if each Ai ∈ σ(S).
T
An equivalent definition is that σ(S) , {Σ | S ⊆ Σ and Σ is a σ-algebra}.
We write R+ for [0, ∞] and R[0,1] for the interval [0, 1]. A metric space is a set X with a
symmetric distance function δ : X × X → R+ that satisfies the triangle inequality δ(x, z) ≤
δ(x, y) + δ(y, z) and the axiom δ(x, x) = 0. We write B(x, r) , {y | δ(x, y) < r} for the open
ball around x of radius r. We equip R+ and R[0,1] with the standard metric δ(x, y) = |x − y|,
and products of metric spaces with the Manhattan metric (e.g., δ((x1 , x2 ), (y1 , y2 )) = δ(x1 , y1 ) +
δ(x2 , y2 )). The Borel σ-algebra on a metric space (X, δ) is B(X, δ) , σ({B(x, r) | x ∈ X ∧ r > 0}).
We often omit the arguments to B when they are clear from the context.
A measurable space is a pair (X, Σ) where X is a set of possible outcomes, and Σ ⊆ P(X)
is a σ-algebra of measurable sets. As an example, consider the extended positive real numbers
R+ equipped with the Borel σ-algebra R, i.e. the set σ({(a, b) | a, b ≥ 0}) which is the smallest
σ-algebra containing all open (and closed) intervals. We can create finite products of measurable
spaces by iterating the construction (X, Σ) × (X ′ , Σ′ ) = (X × X ′ , σ(A × B | A ∈ Σ ∧ B ∈ Σ′ )).
If (X, Σ) and (X ′ , Σ′ ) are measurable spaces, then the function f : X → X ′ is measurable if and
only if for all A ∈ Σ′ , f −1 (A) ∈ Σ, where the inverse image f −1 : P(X ′ ) → P(X) is given by
f −1 (A) , {x ∈ X | f (x) ∈ A}.
A measure µ on (X, Σ) is a function from Σ to R+ , that is (1) zero on the empty set, that
is, µ(∅) = 0, and (2) countably additive, that is, µ(∪i Ai ) = Σi µ(Ai ) if A1 , A2 , . . . are pairwise disjoint. The measure µ is called a (sub-probability) distribution if µ(X) ≤ 1 and finite if
µ(X) 6= ∞. If µ, ν are finite measures and c ≥ 0, we write c·µ for the finite measure A 7→ c·(µ(A))
and µ + ν for the finite measure A 7→ µ(A) + ν(A). We write 0 for the zero measure A 7→ 0. For
any element x of X, the Dirac measure δ(x) is defined as follows:

1 if x ∈ A;
δ(x)(A) =
0 otherwise.
A measure space is a triple M = (X, Σ, µ) where µ is a measure on the measurable space
(X, Σ). Given a measurable function f : X → R+ , the integral of f over M can be defined
following Lebesgue’s theory and denoted as either of
Z
Z
f dµ = f (x) µ(dx) ∈ R+ .
The Iverson brackets [P ] are 1 if predicate P is true, and 0 otherwise. We then write
Z
Z
f dµ , f (x) · [x ∈ A] µ(dx).
A

18

R
We equip
some
R
R measurable spaces (X, Σ) with a stock measure µ. We then write f (s) ds (or
shorter, f ) for f dµ when f is measurable f : X → R+ . In particular, we let the stock measure
on (Rn , B) be the Lebesgue measure λn .
R
A function f is a density of a measure ν (with respect to the measure µ) if ν(A) = A f dµ for
all measurable A.
Given a measurable set A from (X, Σ), we write Σ|A for the restriction of Σ to elements in A,
i.e., Σ|A = {B ∩ A | B ∈ Σ}. Then (A, Σ|A ) is a measurable space. Any distribution µ on (X, Σ)
trivially yields a distribution µ|A on (A, Σ|A ) by µ|A (B) = µ(B).

3.3

Measure Space of Program Traces

In this section, we construct a measure space on the set S of program traces: (1) we define a
measurable space (S, S) and (2) we equip it with a stock measure µ to obtain our measure space
(S, S, µ).
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),
U
the set of all program traces is S = n∈N Rn . Now, let us define the σ-algebra S on S as follows:
let Bn be the Borel σ-algebra on Rn (we take B0 to be {{[]}, {}}). Consider the class of sets S of
the form:
]
A=
Hn
n∈N

where Hn ∈ Bn for all n. Then S is a σ-algebra, and so (S, S) is a measurable space.
Lemma 24 S is a σ-algebra on S.
U
n
for all n, so S ∈ S.
Proof. We have S = n∈N Rn and Rn ∈ RU
If A is defined as above, then S − A = n∈N (Rn − Hn ), where Rn − Hn ∈ Rn for all n, so
S − A ∈ S.
U
Rn for all
For closure
= n∈N Hin for all i ∈ N,
S where Hin ∈
U Ai S
S
U union, take
S under countable
n
i, n. Then i∈N Ai = i∈N n∈N Hin = n∈N ( i∈N Hin ) ∈ S, because i∈N Hin ∈ R .
Thus, S is a σ-algebra on E.

Stock Measure on Program Traces Since each primitive distribution 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
µ on (S, S) defined as follows:
!
X
]
µ
λn (Hn )
Hn =
n∈N

n∈N

where λ0 = δ([]) and λn is the Lebesgue measure on Rn for n > 0.
Lemma 25 µ is a measure on (S, S).
Proof. We check the three properties:

U
n
1. Since
P∞ for all n ∈ N and Hn ∈ R , we have λn (Hn ) ∈ [0, ∞], obviously µ( n∈N Hn ) =
n=1 λn (Hn ) ∈ [0, ∞]
P∞
U
2. If H = n∈N Hn = ∅, then Hn = ∅ for all n, so µ(H) = n=1 λn (∅) = 0.

19

U

3. Countable additivity: if H1 =
in S, then:

n∈N

µ(

∞
]

H1n , H2 =

Hm ) =

m=1

U

µ(

n∈N H2n , . . .

∞ ]
∞
]

m=1 n=0
∞ ]
∞
]

Hmn )

=

µ(

=

n=0 m=1
∞
∞
X
]

=
=
=

is a sequence of disjoint sets

Hmn )

λn (
Hmn )
n=0
m=1
∞ X
∞
X
λn (Hmn )

n=0 m=1
∞
∞ X
X

λn (Hmn )

m=1 n=0
∞
X

µ(Hm )

m=1

P
P∞
P∞ P∞
where the equality ∞
n=0
m=1 λn (Hmn ) =
m=1
n=0 λn (Hmn ) follows from Tonelli’s
theorem for series (see [36]).

S
A measure µ on (X, Σ) is σ-finite if X = i Ai for some countable (finite or infinite) sequence
of sets Ai ∈ Σ such that µ(Ai ) < ∞. If µ is a σ-finite measure on (X, Σ), the measure space
(X, Σ, µ) is also called σ-finite. σ-finite measure spaces behave better with respect to integration
than those who are not.
In the following, let [a, b]n = {(x1 , . . . , xn ) | xi ∈ [a, b] ∀i ∈ 1..n}.
Lemma 26 The measure µ on (S, S) is σ-finite.
U
S
U
S
Proof. For every n ∈ N, we have that Rn = k∈N [−k, k]n . Hence, S = n∈N Rn = n∈N k∈N [−k, k]n
is a countable union of sets in S of the form [−k, k]n . Finally, for all k, n ∈ N we have µ([−k, k]n ) =
λn ([−k, k]n ) = (2k)n < ∞.

It follows that (S, S, µ) is a σ-finite measure space.
Discrete Random Variables We have taken the sample space to be the real numbers, but any
complete separable metric space will
in order to add discrete distributions to
U do. For example,
n
(R
⊎
N)
.
The
measurable
sets Hn become (R ⊎ P(N))n .
the language we can change S to n∈N
P∞
n
The stock measure µ would become n=0 (λ, µ# ) (Hn ), where µ# is the counting measure on N
(that is, µ# (A) = |A| if A is finite, otherwise µ# (A) = ∞).
Discrete distributions have probability mass functions, that is, densities with respect to the
counting measure on N, which are trivially zero-extended to densities with respect to µ. Given a
measurable injection function ⌈·⌉ : R⊎N → 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 = pdf D (~c, z)
w>0
(Eval Random)
[z]
D(~c) ⇓w ⌈z⌉

20

3.4

Distributions hhMii and JMKS Given by Sampling-Based Semantics

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

G
if M ⇓sw G for some w ∈ R+
OM (s) =
fail otherwise.

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

w if M ⇓sw G for some G ∈ GV
PM (s) =
0 otherwise
R
This density function induces a distribution hhM ii on traces defined as hhM ii(A) := A PM .
By inverting the result function OM , we also obtain a distribution JM KS 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.
Z
JM KS (A) := hhM ii(O−1
(A))
=
PM (s) · [OM (s) ∈ A] ds.
M
As an example, for the geometric distribution example of Section 2.4 we have Ogeometric 0.5 (s) =
n if s ∈ [0.5, 1]n[0, 0.5), and otherwise Ogeometric 0.5 (s) = fail. Similarly, we have Pgeometric 0.5 (s) =
1 if s ∈ [0.5, 1]n[0, 0.5) for some n, and otherwise 0. We then obtain
X
hhgeometric 0.5ii(A) =
λn+1 (A ∩ {[0.5, 1]n[0, 0.5)}) and
n∈N

Jgeometric 0.5KS ({n}) =

Z

[s ∈ {[0.5, 1]n [0, 0.5)}] ds =

1
.
2n+1

As seen above, we use the exception fail to model the failure of a hard constraint. To restrict
attention to normal termination, we modify PM as follows.

w if M ⇓sw V for some V ∈ V
V
PM (s) =
0 otherwise.
As above, this density function generates distributions over traces and values as, respectively
Z
−1
V
hhM ii (A) :=
PV
M = hhM ii(A ∩ OM (V))
A

V

(JM KS )|V (A) := hhM ii

(O−1
M (A))

=

Z

V
PM
(s) · [OM (s) ∈ A] ds

To show that the above definitions make sense measure-theoretically, we first define the measurable space of terms (Λ, M), where M is the set of Borel-measurable sets of terms with respect
to the recursively defined metric d in Figure 5.
Lemma 27 For any closed term M , the functions PM , OM and PV
M are all measurable; hhM ii
and hhM iiV are measures on (S, S); JM KS is a measure on (GV, M|GV ); and (JM KS )|V is a measure
on (V, M|V ).


Proof. See Appendix A.

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
21

d(x, x) = 0
d(c, d) = |c − d|
d(M N, LP ) = d(M, L) + d(N, P )
d(g(V1 , . . . , Vn ),g(W1 , . . . , Wn ))
= d(V1 , W1 ) + · · · + d(Vn , Wn )

d(λx.M, λx.N ) = d(M, N )
d(D(V1 , . . . , Vn ),D(W1 , . . . , Wn ))

= d(V1 , W1 ) + · · · + d(Vn , Wn )
d(score(V ), score(W )) = d(V, W )
d(if V then M else N,if W then L else P )
= d(V, W ) + d(M, L) + d(N, P )
d(fail, fail) = 0
d(M, N ) = ∞ otherwise
Figure 5: Metric d on terms.

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 SK. Any closed term M can be written
as N {~c/~x}, where N is a skeleton. The set of closed terms corresponding this way to a skeleton
M ∈ SK is denoted as 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, Σ) and (Y, Σ′ ) are measurable spaces, then a function Q : X × Σ′ → R[0,1] is called a
(sub-probability) kernel (from (X, Σ) to (Y, Σ′ )) if
1. for every x ∈ X, Q(x, ·) is a sub-probability distribution on (Y, Σ′ ); and
2. for every A ∈ Σ′ , Q(·, A) is a non-negative measurable function X → R[0,1] .
The measurable function q : X × Y
R → R+ is said to be a density of kernel Q with respect to a
measure µRon (Y, Σ′ ) if Q(v, A) = A q(v, y) µ(dy) for all v ∈ X and A ∈ Σ′ . When Q is a kernel,
note that f (y) Q(x, dy) denotes the integral of f with respect to the measure Q(x, ·).
Kernels can be composed in the following ways: If Q1 is a kernel from
R (X1 , Σ1 ) to (X2 , Σ2 )
and Q2 is a kernel from (X2 , Σ2 ) to (X3 , Σ3 ), then Q2 ◦ Q1 : (x, A) 7→ Q2 (y, A) Q1 (x, dy) is a
kernel from (X1 , Σ1 ) to (X3 , Σ3 ). Moreover, if Q1 is a kernel from (X1 , Σ1 ) to (X2 , Σ2 ) and Q2 is
a kernel from (X1′ , Σ′1 ) to (X2′ , Σ′2 ), then Q1 × Q2 : ((x, y), (A × B)) 7→ Q1 (x, A) · Q2 (y, B) uniquely
extends to a kernel from (X1 , Σ1 ) × (X1′ , Σ′1 ) to (X2 , Σ2 ) × (X2′ , Σ′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 µ is a measure on terms and E is an evaluation context, we let
E{µ} be the push-forward measure A 7→ µ({M | E[M ] ∈ A}).
One-step evaluation is a relation M → D between closed terms M and distributions D on

22

terms, defined as follows:
E[D(~c)] → E{µD(~c) }

det

E[M ] → δ(E[N ]) if M −−→ N

E[score(c)] → c · δ(E[true]) if 0 < c ≤ 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 D such
that M → D.


Proof. An easy consequence of Lemma 1.

We need to prove the just introduced notion of one-step reduction to support composition. This
is captured by the following result.
Lemma 29 → is a sub-probability kernel.
Let RΛP = {E[R] ∈ CΛ} be the set of all closed reducible terms.
Proof. Lemma 28 already tells us that → can be seen as a function →
ˆ defined as follows:

D(A) if M → D;
→(M,
ˆ
A) =
0
otherwise.
The fact that →(M,
ˆ
·) is a distribution is easily verified. On other hand, the fact that →(·,
ˆ A)
is measurable amounts to proving that OS (A, B) = (→(·,
ˆ 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 OS (A, B) ∩ TM(N ) is measurable. The thesis then follows by observing that
[
OS (A, B) =
OS (A, B) ∩ TM(N )
N ∈SK

and that SK is countable. Now, let us observe that for every skeleton N , the nature of any term
L in 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 TM(xy) are nothing
but deterministic redexes (actually, all of them rewrites deterministically to δ(fail). This allows
us to proceed by distinguishing three cases:
• If all terms in TM(N ) are values, then it can be easily verified that

TM(N ) if 0 ∈ B;
OS (A, B) ∩ TM(N ) =
∅
if 0 6∈ B.
Both when 0 ∈ B and when 0 6∈ B, then, OS (A, B) ∩ TM(N ) is indeed measurable.
• If all terms in TM(N ) contain deterministic redexes, then

→−1 (A) ∩ TM(N ) if 1 ∈ B
OS (A, B) ∩ TM(N ) =
∅
if 1 6∈ B.
Since deterministic reduction → is known to be measurable, then both when 1 ∈ B and when
1 6∈ B, the set OS (A, B) ∩ TM(N ) is measurable.
• The hardest case is when N is of the form G[D(~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 app : C × CΛ → CΛ, that given an evaluation context E and a term M ,
returns the term E[M ]. This is proved measurable in the Appendix.
23

n>0
(DRed Val)
G ⇒n δ(G)
M →D

M ⇒n+1

M ⇒0 0 (DRed Empty)

{N ⇒n EN }N ∈supp(D)
(DRed Step)
R
A 7→ EN (A) D(dN )

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

• The function deapp : RΛP → C ×CΛ that “splits” a term in RΛP into an evaluation context
E and a closed term M . This is proved measurable in the Appendix.
• For every distribution identifier D, the function distapp D : Rn → CΛ (where n is the arity
of D) that, given a tuple of real numbers x, returns the term D(x). This function is a
continuous function between two metric spaces, so measurable.
• We know that for every distribution identifier D, there is a kernel µD : Rn × ΣR → R[0,1] .
Moreover, one can also consider the Dirac kernel on evaluation contexts, namely I : C ×
ΣC → R[0,1] where I(E, A) = [A ∈ E]. Then, the product µD × I is also a kernel, so
measurable.
This concludes the proof.

Given a family {DM }M∈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, DM (B) for the function that
assigns to any term M ∈ A the real number DM (B). The step-indexed approximation small-step
semantics is the family of n-indexed relations M ⇒n D between terms and result distributions
inductively defined in Figure 6. Since generalised values have no transitions (there is no D such
that G → D), the rules above are disjoint and so there is at most one D such that M →n 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 ∈ N, the function ⇒n is a kernel.
Proof. By induction on n:
• ⇒0 can be seen as the function →
ˆ 0 that attributes 0 to any pair (M, A). This is clearly a
kernel.
• ⇒n+1 can be seen as the function ⇒n+1
ˆ defined as follows:

if M ∈ GV and M ∈ A;
 1
0R
if M ∈ GV and M 6∈ A;
→
ˆ n+1 (M, A) =

( →
ˆ n (N, A) D(dN )) if M → D.

The fact that →
ˆ n+1 (M, ·) 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:
(→
ˆ n+1 (·, A))−1 (B) = (→
ˆ n+1 (·, A))−1 (B) ∩ GV ∪

(→
ˆ n+1 (·, A))−1 (B) ∩ (CΛ − GV).

Now, the fact that (→
ˆ n+1 (·, A))−1 (B) ∩ GV is a measurable set of terms is clear: it is A ∩ GV
if 1 ∈ B and ∅ otherwise. But how about (→
ˆ n+1 (·, A))−1 (B) ∩ (CΛ − GV)? In that case, we
just need to notice that
(→
ˆ n+1 (·, A))−1 (B) ∩ (CΛ − GV) = (→
ˆ n ◦ →)−1 (B)
where →
ˆ n and → are kernels (the former by induction hypothesis, the latter by Lemma 29).
Since kernels compose, this concludes the proof.
24

n>0
(DEval Val)
G ⇓n δ(G)

M ⇓0 0 (DEval Empty)

n>0
(DEval Fail)
T ⇓n δ(fail)

n>0
(DEval Fun)
g(~c) ⇓n δ(σg (~c))

n>0
(DEval Samp)
D(~c) ⇓n µD(~c)

0<c≤1
n>0
(DEval Score)
score(c) ⇓n c · δ(true)

M ⇓n D
(DEval If True)
if true then M else N ⇓n+1 D

M ⇓n D

N ⇓n D
(DEval If False)
if false then M else N ⇓n+1 D

N ⇓n E

{L{V /x} ⇓n EL,V }(λx.L)∈supp(D),V ∈supp(E )

M N ⇓n+1 A 7→ D|{fail}
RR(A) + D(R) · [fail ∈ A] + D(Vλ ) · E |{fail} (A)
+ EL,V (A) D|Vλ (λx.dL) E |V (dV )

(DEval Appl)

Figure 7: Step Indexed Approximation Big-Step Semantics.


Lemma 31 For every closed term M and for every n ∈ N there is a unique distribution D such
that M ⇒n D.


Proof. This is an easy consequence of Lemma 30.

4.3

Approximation Big-Step Semantics

The step-indexed approximation big-step semantics M ⇓n D is the n-indexed family of relations
between terms and result distributions inductively defined by the rules in Figure 7.
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 ⇓n D
let x = M in N ⇓n+1

{N {V /x} ⇓n EV }V ∈supp(D)


D|R{fail} (A) + D(R) · [fail ∈ A]
A 7→
+ EV (A) D|V (dV )

M {V /x} ⇓n E
(λx.M )V ⇓n+1 E

n>0
c V ⇓n δ(fail)

The existence of the integral in rule (DEval Appl) is guaranteed by a lemma analogous to Lemma
30.
Lemma 32 For every n ∈ N, the function ⇓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.

25

4.4

Beyond Approximations

The set of result distributions with the pointwise order forms an ω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
JM K⇒ = sup{D | M →n D}
JM K⇓ = sup{D | M ⇓n 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 , JM K⇒ = JM K⇓ .
The following is a fact which will be quite useful in the following:
Lemma 33 (Monotonicity) If M ⇒n D, m ≥ n and M ⇒m E , then E ≥ 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 ⇒n D, N ⇒m E , and for all L and V , L{V /x} ⇒p EL,V , then M N ⇒n+m+p F
such that for all A
F (A) ≥ D|{fail} (A) + D(R) · [fail ∈ A] + D(Vλ ) · E |{fail} (A)
ZZ
+
EL,V (A) D|Vλ (λx.dL) E |V (dV ).
Proof. First of all, one can prove that if N R⇒n D and L{V /x} ⇒m EV for all V then
(λx.L)N ⇒n+m F where F (A) ≥ D|{fail} (A) + EV (A) D|V (dV ) for all A. This is an induction
on n.
• RIf n = 0, then D is necessarily the zero distribution A 7→ 0. Then F (A) ≥ 0 = D|{fail} (A) +
EV (A) D|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 D = δ(W ), D|{fail} is the zero distribution and thus
Z
(λx.L)N ⇒m+1 (A 7→ D|{fail} (A) + EV (A) D|V (dV )).
The thesis follows by monotonicity.
• If N is an exception fail, then D = δ(fail), and since (λx.L)fail → fail, we can
conclude that, since D|V is the zero distribution,
Z
(λx.L)N ⇒2 δ(fail) = (A 7→ D|{fail} (A) + EV (A) D|V (dV )).
The thesis again follows by monotonicity.
R
• If N is not a generalized value, then, necessarily D(A) = GP (A) H (dP ), where N → H
and P ⇒n GP for every P . By induction hypothesis, there are distributions IP such that
(λx.L)P ⇒n+m IP , and, for all A,
Z
IP (A) ≥ GP |{fail} + EV (A) GP |V (dV )
Let now E be the evaluation context (λx.L)[·]. Then, it holds that (λx.L)N → E{H } and
thus:
Z
(λx.L)N ⇒n+m+1 (A 7→ IP (A) (E{H }((λx.L)dP ))).
26

We can now observe that:
Z
Z
IP (A) (E{H }((λx.L)dP )) = IP (A) H (dP )
Z
ZZ
≥ GP |{fail} (A) H (dP ) +
EV (A) GP |V (dV ) H (dP )
ZZ
= D|{fail} (A) +
EV (A) GP |V (dV ) H (dP )
Z
= D|{fail} (A) + EV (A) D|V (dV ).
Then one can prove the statement of the lemma, again by induction on n, following the same
strategy as above.

Lemma 35 If M ⇓n D there is E s.t. M ⇒3n E and E ≥ D.
Proof. By induction on n, we can prove that if M ⇓n D, then M ⇒E where E ≥ D. The only
interesting case is when M is an application, and there we simply use Lemma 34.

At this point, we already know that JM K⇒ ≥ JM K⇓ . 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 M N ⇒n+1 D, then M ⇒n E , N ⇒n F and for all P and V , P {V /x} ⇒n GP,V
such that for all A,
D(A) ≤ E |{fail} (A) + E (R) · [fail ∈ A] + E (Vλ ) · F |{fail} (A)
ZZ
+
GP,V (A) E |Vλ (λx.dP ) F |V (dV ).
Proof. By induction on n.
• If n = 0, then D is the zero distribution, and so are E , F and all GP,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 λx.L and N is a value W , then M → δ(L{W/x}) and L{W/x} ⇒n D.
We can then observe that
E = δ(λx.L)
F = δ(W )
GP,V = D whenever P = L and V = W
Just observe that
D(A) =

ZZ

GP,V (A) E (λx.dP ) F (dV )

and that E |{fail} = E |R = F |{fail} = 0.
• If none of M and N are values, then M → L and thus M N → E{L } where E = [·]N .
Moreover, LN ⇒n HL , where
Z
Z
D(A) = HL (A) E{L }((dL)N ) = HL (A) L (dL)
We apply the induction hypothesis (and monotonicity) to each of the LN ⇒n HL , and we
obtain that L ⇒n−1 IL , N ⇒n F and P {V /x} ⇒n GP,V , where
HL (A) ≤ IL |{fail} (A) + IL (R) · [fail ∈ A] + IL (Vλ ) · F |{fail} (A)
ZZ
+
GP,V (A) IL |Vλ (λx.dP ) F |V (dV )
27

Now let E be the distribution
A 7→

Z

IL (A) L (dL).

Clearly, M ⇒n E . Moreover,
Z
D(A) = HL (A) L (dL)
Z
Z
≤ IL |{fail} (A) L (dL) + IL (R) · [fail ∈ A] L (dL)
Z
+ IL (Vλ ) · F |{fail} (A) L (dL)
ZZZ
+
GP,V (A) IL |Vλ (λx.dP ) F |V (dV ) L (dL)
= E |{fail} (A) + E (R) · [fail ∈ A] + E (Vλ ) · F |{fail} (A)
ZZ
+
GP,V (A) E |Vλ (λx.dP ) F |V (dV )


Lemma 37 If M ⇒n D, then there is E such that M ⇓n E and E ≥ D.
Proof. Again, this is an induction on n that makes essential use, this time, of Lemma 36.



Restatement of Theorem 2. For all M , JM K⇒ = JM K⇓ .
Proof. This is a consequence of Lemma 35 and Lemma 37.



In subsequent sections we let JM K stand for JM K⇒ or JM K⇓ .

4.5

Geometric Distribution, Revisited

Let’s consider again the geometric distribution of Section 2.4. There is a monotonically increasing
map f : N → N such that for every n, it holds that
(geometric 0.5) ⇒f (n)
As a consequence, Jgeometric 0.5K =

4.6

n
X
1
δ(i)
i+1
2
i=0

P∞

1
i=0 2i+1 δ(i).

Distribution-based and Sampling-based Semantics are Equivalent

This section is a proof of the following theorem.
Theorem 3 For every term M , JM KS = JM K.
The way to prove Theorem 3 is by looking at traces of bounded length. For every n ∈ N, let Sn
be the set of sample traces of length at most n, which itself has the structure of a measure space
with measurable sets S|Sn . We define the result distribution JM KnS as follows:
Z
n
PM (s) · [OM (s) ∈ A] ds
JM KS (A) =
Sn

The integral over all traces can be seen as the limit of all integrals over bounded-length traces:
R
R
Lemma 38 If f : S → R+ is measurable then f = supn Sn f .
28

R
R
Proof. Let gn (s) = f (s) · [s ∈ Sn ], so Sn f = gn by definition. Since the gn are converging to
R
R

f pointwise from below, we have f = supn gn by the monotone convergence theorem.

A corollary is that JM KS = supn∈N JM KnS .

R
Lemma 39 If M → D, then JM K = A 7→ JN K(A) D(dN )

Proof. For every n and for every term N , let ENn be the unique value distribution such that
N ⇒n ENn . By definition, we have that
Z
n+1
EM
(A) = ENn (A) D(dN ).
By the monotone convergence theorem, then,
Z
n+1
JM K(A) = sup EM
(A) = sup ENn (A) D(dN )
n
n
Z
Z
n
= (sup EN (A)) D(dN ) = JN K(A) D(dN ).
n


The following is a useful technical lemma.
R
Lemma 40 JE[D(~c)]Kn+1
(A) = JN KnS (A) E{µD (~c)}(dN ).
S
R
Lemma 41 If M → D, then JM KS = A 7→ JN KS (A) D(dN )

A program M is said to deterministically diverge iff (M, 1, s) ⇒ (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 JM K = JM KS = 0.
Proof. One can easily prove, by induction on n, that if M deterministically diverges, then
M ⇒n 0:
• If n = 0, then M ⇒n 0 by definition.
• About the inductive case, since M cannot be a generalized value, it must be that M → δ(N )
(where N deterministically diverges) and that M ⇒n+1 D, where N ⇒n D. By induction
hypothesis, D = 0.
The fact that JM KS = 0 is even simpler to prove, since if M deterministically diverges, then there
cannot be any s, w, V such that M ⇓sw V , and thus PM (s) is necessarily 0.

A program M is said to deterministically converge to a program N iff (M, 1, []) ⇒ (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:
• D ≤ E whenever M ⇒n D; and N ⇒n E ;
• JM KnS = JN KnS ;
• JM K = JN K and JM KS = JN KS
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
det
assume, without losing any generality, that (M, 1, []) → (N, 1, []), namely that M −−→ N . With
w
w
the latter hypothesis, it is easy to realize that M ⇓s V iff N ⇓s V and that M ⇒n+1 D iff
N ⇒n D. The thesis easily follows.

Lemma 44 For every generalized value G, it holds that JGK = JGKS = δ(G).
29

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, D, c1 , . . . , c|D| such that M deterministically converges to E[D(c1 , . . . , c|D| )].


Proof. Easy.

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 ⇒n D, then D ≤ JM KS .
Proof. By induction on n:
• If n = 0, then D is necessarily 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, D ≤ JM K = JM KS .
• If M deterministically converges to a generalized value G, then by Lemma 43 and Lemma
44, it holds that
D ≤ JM K = JGK = δ(G) = JGKS = JM KS .
• If M deterministically converges to E[D(~c)], let E be such that E[D(~c)] ⇒n+1 E . By Lemma
43 and Lemma 40 we have, by induction hypothesis, that
Z
D(A) ≤ E (A) = FN (A) E{µD (~c)}(dN )
Z
≤ JN KS (A) E{µD (~c)}(dN )
= JM KS



where N ⇒n FN .

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 ∈ N, JM KnS ≤ JM K.
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, JM K0S ≤ JM KS = JM K.
• If M deterministically converges to a generalized value G, then by Lemma 43 and Lemma
44, it holds that
JM K0S = JGK0S ≤ JGKS = δ(G) = JGK = JM K.

• If M deterministically converges to E[D(~c)], then JM K0S = JE[D(~c)]K0S = 0 ≤ JM K.
• 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, JM Kn+1
≤ JM KS = JM K.
S
• If M deterministically converges to a generalized value G, then by Lemma 43 and Lemma
44, it holds that
JM Kn+1
= JGKn+1
≤ JGKS = δ(G) = JGK = JM K.
S
S

30

• If M deterministically converges to E[D(~c)], by Lemma 43 and Lemma 40 we have, by
induction hypothesis, that
JM Kn+1
(A) = JE[D(~c)]Kn+1
(A)
S
S
Z
= JN KnS (A) E{µD (~c)}(dN )
Z
≤ JN K(A) E{µD (~c)}(dN )
= JM K.


Restatement of Theorem 3. JM KS = JM K.
Proof.
JM K⇒ = sup{D | M →n D}

(by definition)

n∈N

≤ JM KS
= supJM KnS

(by Lemma 46)
(by Lemma 38)

n∈N

≤ JM K

(by Lemma 47)

= JM K⇒

(by Theorem 2)



Corollary 1 The measures hhM ii and hhM iiV are sub-probability distributions.

4.7

An Application of the Distribution-Based Semantics

It
is
routine
to
show
that
for
Jscore(V )K|V = JM V K|V , where M is the term

all

values

V,

it

holds

that

λx.if (0 < x) ∧ (x ≤ 1)
then (if flip(x) then true else fail)
else fail
This shows that even though score(V ) and M V 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 Jscore(V )K = JM V K is needed, we could replace M by the
following one:
λx.if (0 < x) ∧ (x ≤ 1)
then (if flip(x) then true else Ω)
else 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 . . . in
if b then n else f 0
f 0
This corresponds to a basic inference algorithm known as rejection sampling.
31

4.9

Motivation for 1-Bounded Scores

Recall that we only consider score(c) for c ∈ (0, 1]. Admitting 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
inflate := fix f λx.if flip(0.5) then score(2); (f x) else x.
Since Jscore(2)K = JfailK we have Jinflate V K = 0.5 · δ(V ) + 0.5 · δ(fail) for any V . However,
evaluating inflate V in a version of our trace semantics where the argument to score may be 2
yields
n
X
hhinflate V ii(Sn ) =
1/2 = n/2
k=1

and so there Jinflate V KS (A) = ∞ if V ∈ A, otherwise 0.
More strikingly, in the modified semantics we would also have Jinflate Gaussian(0, 1)KS ([q, r]) =
∞ 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 σ-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 JM KS (V) < ∞.

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 ∈ CΛ. This algorithm yields consecutive
V
samples from a Markov chain over S, such that the density of the samples s converges to PM
(s)
up to normalization. We can then apply the function OM 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:
V
1. Pick an initial state s with PM
(s) 6= 0 (e.g., by running M ).
2. Draw the next state t at random with probability density q(s, t).
3. Compute α as below.


PV (t) q(t, s)
(1)
·
α = min 1, M
V (s) q(s, t)
PM
• With probability α, 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 α above is often called the Hastings acceptance probability. Different probabilistic programming language implementations use different choices for the density q
V
above, based on pragmatics. The trivial choice would be to let q(s, t) = PM
(t) for all s, which
always yields α = 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).

32

V
q(s, t) = (Πki=1 pdf Gaussian (si , σ 2 , ti )) · PN
(tk+1..|t| )

if |t| 6= 0, where k = min{|s|, |t|}
and N = peval(M, t1..k )
Z
q(s, t) dt, where A = {t | |t| 6= 0}
q(s, []) = 1 −
A
Z
q(s, t) dt
Q(s, A) =
A

Figure 8: Proposal Density q(s, t) and Kernel Q(s, A) for Program M

5.2

Proposal Density

In the following, let M be a fixed program. Given a trace s = [c1 , . . . , cn ], we write si..j for the
trace [ci , . . . , cj ] when 1 ≤ i ≤ j ≤ 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 = [t1 , . . . , tn ] where each ti is drawn independently from a
normal distribution with mean si and variance σ 2 , and let pi be the probability density of ti .
2. Let k ≤ n be the largest number such that (M, 1, t1..k ) ⇒ (M ′ , w, []). There are three
cases:
′
′
′
• If k = n, run M ′ ⇓w
t′ V , and let q(s, t@t ) = p1 . . . pn w .
′ 1
• If k < n and M ⇓[] V , let q(s, t1..k ) = p1 . . . pk .
• Otherwise, let q(s, t1..k ) = 0 and propose the trace [].
To define this density formally, we first give a function that partially evaluates M given a trace.
Let peval be a function taking a closed term M and trace s and returning the closed term M ′
obtained after applying just as many reduction steps to M as required to use up the entire trace
s (or fail if this cannot be done).

M
if s = []



M ′
if (M, 1, s) ⇒ (Mk , wk , sk ) → (M ′ , w′ , [])
peval(M, s) =

for some Mk , wk , sk , w′ such that sk 6= []



fail otherwise
Lemma 48 For every M ∈ CΛ, c ∈ R, s ∈ S, peval(peval(M, [c]), s) = peval(M, c :: s).
Proof. By splitting the equality into two inequalities, substituting the alternative definition of
peval (described in the appendix) and using Scott induction.

Lemma 49 For every M ∈ CΛ, c ∈ R, s ∈ S, peval(peval(M, s), t) = peval(M, s@t).
Proof. By induction on |s|, with appeal to Lemma 48.

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 µ on
program traces. For technical reasons, we need to ensure that Q is a probability kernel, i.e., that
Q(s, S) = 1 for all s. We normalize q(s, ·) by giving non-zero probability q(s, []) to transitions
ending in [] (which
R is not a completed trace of M by assumption). All this is in Figure 8.
The integral A q(s, t)dt is well-defined if and only if q(s, ·) is non-negative and measurable for
every s. In order to show that this property is satisfied, we first need to prove that the peval
function, used in the definition of q, is measurable:
33

Lemma 50 peval is a measurable function CΛ × S → CΛ.
Using this result, we can show that q, as a function defined on pairs of traces, is measurable.
Lemma 51 For any closed program M , the transition density q(·, ·) : (S× S) → R+ is measurable.
By a well-known result in measure theory [2, Theorem 18.1], it follows that q(s, ·) is measurable
for every s ∈ S. To define the transition kernel for the algorithm in terms of the proposal kernel
Q, we need to show that Q is a probability kernel.
Lemma 52 The function Q is a probability kernel on (S, S).
The proofs of lemmas 50, 51 and 52 can be found in the long version of this paper [4].

5.4

Transition Kernel of the Markov Chain

We now use the proposal kernel Q to construct the transition kernel of the Markov chain induced
by the algorithm. To avoid trivial cases, we assume that M has positive success probability and
does not behave deterministically, i.e., that JM K(V) > 0 and hhM ii({[]}) = 0.
Hastings’ Acceptance Probability α is defined as in Equation (1) on page 32, where we let
V
V
α(s, t) = 0 if PM
(t) = 0 and otherwise α(s, t) = 1 if PM
(s) · q(s, t) = 0. Given the proposal
transition kernel Q and the acceptance ratio α, the Metropolis-Hastings algorithm yields a Markov
chain over traces with the following transition probability kernel.
Z
Z
P (s, A) =
α(s, t) Q(s, dt) + [s ∈ A] · (1 − α(s, t)) Q(s, dt).
(2)
A

Define P n (s, A) to be the probability of the n:th element of the chain with transition kernel P
starting at s being in A:
P 0 (s, A)

=

P n+1 (s, A)

=

[s ∈ A]
Z
P (t, A)P n (s, dt)

−1
n
Lemma 53 If s0 ∈ O−1
M (V) then P (s0 , OM (V)) = 1.

Proof. By induction on n. The base case Rholds, since s0 ∈ O−1
M (V) by assumption. For the
−1
−1
n
(V))P
(s
induction case, we have P n+1 (s0 , OM
(V)) = P (s, O−1
0 , ds). If s ∈ OM (V) we have
M
Z
Z
−1
α(s, t) Q(s, dt) + (1 − α(s, t)) Q(s, dt)
P (s, OM (V)) =
O−1
M (V)

=
=

Z

O−1
M (V)

Z

O−1
M (V)

q(s, t) dt + (1 − α(s, []))q(s, [])
q(s, t) dt + (1 − α(s, []))(1 −

= 1 − α(s, [])(1 −

Z

O−1
M (V)

Z

O−1
M (V)

q(s, t) dt)

q(s, t) dt)

V
where α(s, []) = 0 since PM
([]) = 0 by assumption. Then
Z
Z
−1
n
n
P (s, O−1
P (s, OM (V))P (s0 , ds) =
M (V))P (s0 , ds)
O−1
M (V)

=

Z

O−1
M (V)

1P n (s0 , ds)

=1
where the first and the third equality follow from the induction hypothesis.
34



n
n
n
Lemma 54 There is 0 ≤ c < 1 such that P n ([], O−1
M (V)) = 1 − c and P ([], {[]}) = c .
V
Proof. Let c = 1 − hhM iiV (S \ {[]}). By assumption [] 6∈ O−1
M (V) and c < 1, and since hhM ii is
a sub-probability distribution we have 0 ≤ c. We proceed by induction on n. The base case is
trivial. For the induction case, we have P (s, S \ {[]}) = 1 for all s ∈ O−1
M (V). Finally
Z
V
V
P ([], O−1
(V))
=
PM
= hhM iiV (O−1
M
M (V)) = hhM ii (S \ {[]}).
O−1
(V)

M

Based on Lemma 53 and 54, we below consider the Markov chain with kernel P restricted to
O−1
M (V) ∪ {[]}.

5.5

Correctness of Inference

By saying that the inference algorithm is correct, we mean that as the number of steps goes
to infinity, the distribution of generated samples approaches the distribution specified by the
sampling-based semantics of the program.
Formally, we define T n (s, A) = P n (s, O−1
M (A)) as the value sample distribution at step n of
the Metropolis-Hastings Markov chain. For two measures defined on the same measurable space
(X, Σ), we also define the variation norm ||µ1 − µ2 || as:
||µ1 − µ2 || = sup |µ1 (A) − µ2 (A)|
A∈Σ

We want to prove the following theorem:
V
Theorem 4 (Correctness) For every trace s with PM
(s) 6= 0,

lim ||T n (s, ·) − JM K|V || = 0.

n→∞

To do so, we first need to investigate the convergence of P n to our target distribution π, defined
as follows:
π(A) = hhM iiV (A)/hhM iiV (S).
We use a sequence of known results for Metropolis-Hastings Markov chains [38] to prove that
P n converges to π. We say that a Markov chain transition kernel P is D-irreducible if D is a
non-zero sub-probability distribution on (S, S), and for all x ∈ S, A ∈ S there exists an integer
n > 0 such that D(A) > 0 implies P n (x, A) > 0. We say that P is D-aperiodic if there do not
exist d ≥ 2 and disjoint B1 , . . . , Bd such that D(B1 ) > 0, and x ∈ Bd implies P (x, B1 ) = 1, and
x ∈ Bi implies that P (x, Bi+1 ) = 1 for i ∈ {1, . . . , d − 1}.
Lemma 55 (Tierney [38], Theorem 1 and Corollary 2) Let K be the transition kernel of
a Markov chain given by the Metropolis-Hastings algorithm with target distribution D. If K is
D-irreducible and aperiodic, then for all s, limn→∞ ||K n (s, ·) − D|| = 0.
V
Lemma 56 (Strong Irreducibility) If PM
(s) > 0 and hhM iiV (A) > 0 then P (s, A) > 0.
V
Proof. There is n such that PM
(A ∩ Sn ) > 0. Write A|n = A ∩ Sn . For all t ∈ A|n , q(s, t) > 0
by case analysis on whether n ≤ |s|. If n ≤ |s|, then for all t ∈ A|n ,

q(s, t) = Πni=1 pdf Gaussian (si , σ 2 , ti ) > 0
q(t, s) =

(Πni=1

2

pdf Gaussian(ti , σ , si )) ·

and

V
Ppeval(M,s
(s(n+1) , . . . , sn )
1..n )

> 0.

Similarly, if n > |s|, then for all t ∈ A|n ,
|s|

V
(t(|s|+1) , . . . , t|s| ) > 0
q(s, t) = (Πi=1 pdf Gaussian(si , σ 2 , ti )) · Ppeval(M,t
1..|s| )

q(t, s) =

|s|
Πi=1

pdf Gaussian (ti , σ 2 , si ) > 0.
35

and

V
Since µ(A|n ) > 0 and PM
(t) > 0 for all t ∈ A|n ,

P (s, A) ≥ P (s, A|n )
Z
α(s, t) Q(s, dt)
≥
A|n
Z
α(s, t)q(s, t) dt
=
A|n

=

Z

min{q(s, t),

A|n

V
PM
(t)q(t, s)
} dt
V (s)
PM

> 0.



Corollary 2 (Irreducibility) P as given by Equation (2) is π-irreducible.
Lemma 57 (Aperiodicity) P as given by Equation (2) is π-aperiodic.
Proof. Assume that B1 , B2 are disjoint sets such that π(B1 ) > 0 and P (s, B2 ) = 1 for all s ∈ B1 .
If s ∈ B1 , Lemma 56 gives that P (s, B1 ) > 0, so P (s, B2 ) < P (s, S) = 1, which is a contradiction.
A fortiori, P is π-aperiodic.

Lemma 58 If µ1 and µ2 are measures on (X1 , Σ1 ) and f : X1 → X2 is measurable Σ1 /Σ2 , then
||µ1 f −1 − µ2 f −1 || ≤ ||µ1 − µ2 ||
Proof. We have supB∈Σ2 |µ1 f −1 (B) − µ2 f −1 (B)| = supA∈Σ′1 ||µ1 (A) − µ2 (A)||, where Σ′1 =
{f −1 (B)|B ∈ Σ2 }. By measurability of f we get Σ′1 ⊆ Σ1 , so by monotonicity of sup we get

supA∈Σ′1 |µ1 (A) − µ2 (A)| ≤ supA∈Σ1 |µ1 (A) − µ2 (A)|.
V
Restatement of Theorem 4. For every trace s with PM
(s) 6= 0,

lim ||T n (s, ·) − JM K|V || = 0.

n→∞

Proof. By Corollary 2, P is π-irreducible, and by Lemma 57, P is π-aperiodic. Lemma 55 then
yields that
lim ||P n (x, ·) − π|| = 0.
n→∞

By definition, T (s, A) = P (s, O−1
M (A)) and JM K|V (A) = JM K(A ∩ V)/JM K(V). By Theorem 3,
−1
−1
−1
V
JM K(A ∩ V) = JM KS (A ∩ V) = hhM ii(O−1
M (A ∩ V) = hhM ii(OM (A) ∩ OM (V)) = hhM ii (OM (A))
−1
−1
V
and similarly JM K(V) = hhM ii(OM (V)) = hhM ii (S), which gives JM K|V (A) = π((OM (A)). Thus,
n

n

by Lemma 58 and the squeeze theorem for limits we get

lim ||T n (s, ·) − JM K|V || ≤ lim ||P n (s, ·) − π|| = 0.

n→∞

5.6

n→∞



Examples

To illustrate how inference works, we revisit the geometric distribution and linear regression
examples from Section 2. Before discussing the transition kernels for these models, note that
the products of Gaussian densities always cancel out in the acceptance probability α, because
pdf Gaussian (si , σ 2 , ti ) = pdf Gaussian (ti , σ 2 , si ) by the definition of the Gaussian PDF.

36

Geometric Distribution Let us begin with the implementation of the geometric distribution,
described in 2.4, which we will call M1 . Since the only random primitive used in M1 is rnd, whose
density is 1 on all its support, and there are no calls to score, the weight of any trace that yields a
value must be 1. Because the geometric function applied to 0.5 returns a value immediately when
the call to rnd returns a number smaller than 0.5, and recursively calls itself otherwise, otherwise
returns a value immediately
The function geometric applied to 0.5 calls itself recursively if the call to rnd returned a value
greater or equal to a half, and returns a value immediately otherwise. Hence, every valid trace
consists of a sequence of numbers in [0.5, 1], followed by a number in [0, 0.5), and so the set of
valid traces is S1 = {s | si ∈ [0, 0.5) for i < |s| ∧ s|s| ∈ [0.5, 1] ∧ |s| > 0}. The proposal density is
q(s, t) = [t ∈ S1 ]Πki=1 pdf Gaussian(si , σ 2 , ti )
where k = min{|s|, |t|}. The term [t ∈ S1 ] reflects the fact that for every non-valid trace,
PV
peval(M,t1..k ) (tk+1..|t| ) = 0.
As noted above, the Gaussians cancel out in the acceptance ratio, and the density of every
valid trace is 1, so α(s, t) = [t ∈ S1 ]. This means that every valid trace is accepted. The transition
kernel of the Markov chain induced by the MH algorithm is
Z
min{|s|,|t|}
pdf Gaussian(si , σ 2 , ti )µ(dt)
Πi=1
P (s, A) =
A∩S1
Z
min{|s|,|t|}
pdf Gaussian (si , σ 2 , ti )µ(dt)
Πi=1
+ [s ∈ A]
S\S1

Linear Regression with flip Now, consider the linear regression model from section 2.6, which
can be translated from Church to the core calculus by applying the rules in Figure 2 (details are
omitted, but the translation is straightforward as there is no recursion).
In every trace in this translated model, which we call M2 , we have two draws from Gaussian(0, 2)
, whose values are assigned to variables m and b. They are followed by four calls to rnd made
while evaluating the four calls to softeq. The conditioning statement at the end sets the return
value to false if at least one call to softeq evaluates to false. Since softeq x y returns true
if and only if the corresponding call to rnd returned a value less than squash x y, it follows from
the definitions of squash and f that the element of the trace consumed by softeq (f x) y must
1
be in the interval [1, e(m·x+b−y)
2 )]. Note that since the pdf of rnd is flat, the weight of any trace
depends only on the first two random values, drawn from the Gausians, as long as the remaining
four random values are in the right intervals.
The full density for this model is

Π2i=1 pdf Gaussian(0, 2, si ) ·
PV
M2 (s) =




1
Π4i=1 si+2 ∈ 1, (s ·x +s −y )2
e i i 2 i
if s ∈ R6 and PV
/ R6 .
M2 (s) = 0 if s ∈
Note that the partial derivative of PV
M2 (s) with respect to each of s3 , s4 , s5 , s6 is zero wherever
defined, precluding the use of efficient gradient-based methods for searching over these components
of the trace.
6
Now, let us derive the density q(s, t), assuming that PV
M2 (s) > 0 (which implies s ∈ R , as
6
shown above) and t ∈ R . Since we have |s| = |t| = 6, the formula for q reduces to:
q(s, t) = (Π6i=1 pdf Gaussian (si , σ 2 , ti )PV
M2′ ([])
where M2′ = peval(M2 , t). Because there cannot be more than six random draws in any run
′ []
V
of the program, M2′ is determinstic. This means that PV
M ′ ([]) = 0 if M2 ⇓1 fail and PM ′ ([]) = 1
2

[]

if M2′ ⇓1 fail for some V .

37

2

It is easy to check that if t ∈
/ R6 , then q(s, t) = 0—since there is no trace of length other than
6 leading to a value, the value of PV
M2′ (tk+1..|t| ) in the definition of q must be 0 in this case.
Thus, the proposal density is

q(s, t) = Π6i=1 pdf Gaussian (si , σ 2 , ti ) ·


1
Π4i=1 [ti+2 ∈ [0, (t ·x +t −y )2 )]
e i 1 2 i
for t ∈ R6 and q(s, t) = 0 for t ∈
/ R6 .
Hence, the acceptance ratio reduces to
α(s, t)

= min{1,

Π2i=1 pdf Gaussian (0, 2, ti )
·
Π2i=1 pdf Gaussian(0, 2, si )
1
Π4i=1 [ti+2 ∈ [0, (t ·x +t −y )2 )]}
1
i
2
i
e

if t ∈ R6 and α(s, t) = 0 otherwise.
Note that α(s, t) is only positive if each of t3 , t4 , t5 , t6 are within a certain (small) interval.
This is problematic for an implementation, since it will need to find suitable values for all these
components of the trace for every new trace to be proposed, leading to inefficiencies due to a
slowly mixing Markov chain.
Linear Regression with score In this alternative version M3 of the previous model, we also
have two draws from Gaussian(0, 2) at the beginning, but the calls to flip are replaced with calls
to score, which multiply the trace density by a positive number without consuming any elements
of the trace. Because the support of the Gaussian PDF is R and there are precisely two random
draws (both from Gaussians) in every trace leading to a value, the set of valid traces is R2 . We
2
4
−(s1 ·xi +s2 −yi )2
have PV
if s ∈ R2 and PV
M3 (s) = Πi=1 pdf Gaussian (0, 2, si ) Πi=1 e
M3 (s) = 0 otherwise.
V
2
Assuming PM3 (s) > 0 and t ∈ R , we get the proposal density
q(s, t) = Π2i=1 pdf Gaussian(si , σ 2 , ti )Π4i=1

1
e(t1 ·xi +t2 −yi )2

where x = [0, 1, 2, 3] and y = [0, 1, 4, 6]. If t ∈
/ R2 , then q(s, t) = 0, because otherwise there would
be a trace of length different than 2 leading to a value.
Thus, the acceptance ratio is
α(s, t) =

Π2i=1 pdf Gaussian (0, 2, ti )
Π2i=1 pdf Gaussian(0, 2, si )

if t ∈ R2 and α(s, t) = 0 otherwise.
In contrast to the previous example, here the acceptance ratio is positive for all proposals,
non-zero gradients exist almost everywhere, and there are four fewer nuisance parameters to deal
with (one per data point!). This makes inference for this version of the model much more tractable
in practice.

6

Related Work

To the best of our knowledge, the only previous theoretical justification for trace MCMC is the
recent work by Hur et al. [19], who show correctness of trace MCMC for the imperative probabilistic
language R2 [27]. Their result does not apply to higher-order languages such as Church or our
λ-calculus, nor to programs that do not almost surely terminate [9]. Their algorithm is different
from ours in that it exploits the explicit storage locations found in imperative programs, keeping
one sample trace per location. The authors do state that the space of traces in their language is
38

equipped with a “stock” measure, and that the distributions of program traces and transitions are
given by densities with respect to that measure. They do not, however, show that these densities
are measurable. Their proof of correctness only shows that the acceptance ratio α computed by
their algorithm matches Hasting’s formula: the authors do not prove convergence of the resulting
Markov chain. Indeed, properties such as irreducibility and aperiodicity depend on the choices of
parameters in the algorithm.
Other probabilistic language implementations also use trace MCMC inference, including Church [15],
Venture [25], WebPPL [13], and Anglican [39]. These works focusing on efficiency and convergence properties, and do not state formal correctness claims for their implementations.
Wingate et al. [42] give a general program transformation for a probabilistic language to support
trace MCMC, with a focus on labelling sample points in order to maximise sample reuse. Extending
our trace semantics with such labelling is important future work, given that Kiselyov [22] points
out some difficulties with the transformation and proposes alternatives.
Many recent probabilistic languages admit arbitrary non-negative scores. This is done either
by having an explicit score-like function, as in WebPPL (called factor), or by observing that
a particular value V was drawn from a given distribution D(~c) (without adding it to the trace),
as in Web Church (written (D ~c V )) or Anglican (observe (D ~c) V ). In recent work for a
non-recursive λ-calculus with score, Staton et al. [35] note that unbounded scores introduce the
possibility of “infinite model evidence errors”. As seen in Section 4.9, even statically bounded
scores exhibit this problem in the presence of recursion.
Kozen [23] gives a semantics of imperative probabilistic programs as partial measurable functions from infinite random traces to final states, which serves as the model for our trace semantics.
Kozen also proves this semantics equivalent to a domain-theoretic one. Park et al. [30] give an
operational version of Kozen’s trace-based semantics for a λ-calculus with recursion, but “do not
investigate measure-theoretic properties”. Cousot and Monerau [5] generalise Kozen’s trace-based
semantics to consider probabilistic programs as measurable functions from a probability space
into a semantics domain, and study abstract interpretation in this setting. Toronto et al. [41]
use a pre-image version of Kozen’s semantics to obtain an efficient implementation using rejection
sampling. Scibior et al. [34] define a monadic embedding of probabilistic programming in Haskell
along the lines of Kozen’s semantics; their paper describes various inference algorithms but has
no formal correctness results.
Ramsey and Pfeffer [32] provide a monadic denotational semantics for a first-order functional
language with discrete probabilistic choice, and a Haskell implementation of the expectation monad
using variable elimination. Bhat et al. [1] define a denotational semantics based on density functions for a restricted first-order language with continuous distributions. They also present a type
system ensuring that a given program has a density.
Jones [20, Chapter 8] defines operational and domain-theoretic semantics for a λ-calculus with
discrete probabilistic choice and a fixpoint construct. Our distribution-based operational semantics
generalises Jones’s to deal with continuous distributions. Like Kozen’s and Jones’s semantics,
our operational semantics makes use of the partially additive structure on the category of subprobability kernels [28] in order to treat programs that make an unbounded number of random
draws. Staton et al. [35] give a domain-theoretic semantics for a λ-calculus with continuous
distributions and unbounded score, but without recursion. While giving a fully abstract domain
theory for probabilistic λ-calculi with recursion is known to be hard [21], there have been recent
advances using probabilistic coherence spaces [6, 8] and game semantics [7], which in some cases
are fully abstract. We see no strong obstacles in applying any of these to a typed version of our
calculus, but it is beyond the scope of this work. Another topic for future work are methodologies
for equivalence checking in the style of logical relations or bisimilarity, which have been recently
shown to work well in discrete probabilistic calculi [3].

39

7

Conclusions and Remarks

As a foundation for probabilistic inference in languages such as Church, we defined a probabilistic
λ-calculus with draws from continuous probability distributions and both hard and soft constraints,
defined its semantics as distributions on terms, and proved correctness of a trace MCMC inference
algorithm via a sampling semantics for the calculus.
Although our emphasis has been on developing theoretical underpinnings, we also implemented
our algorithm in F# to help develop our intuitions and indeed to help debug definitions. The
algorithm is correct and effective, but not optimized. In future, we aim to extend our proofs to
cover more efficient algorithms, inspired by Wingate et al. [42] and Kiselyov [22], for example.

A

Proofs of Measurability

This appendix contains the proofs of measurability of PM , OM , PV
M , peval and q, as well as a
proof that Q is a probability kernel.
The proofs usually proceed by decomposing the functions into simpler operations. However,
unlike Toronto [40], we do not define these functions entirely in terms of general measurable
operators, because the scope for reuse is limited here. We would have, for instance, to define
multiple functions projecting different subexpressions of different expressions, and prove them
measurable. Hence, the overhead resulting from these extra definitions would be greater than the
benefits.
First we recap some useful results from measure theory:
• A function f : X1 → X2 between metric spaces (X1 , d1 ) and (X2 , d2 ) is continuous if for
every x ∈ X1 and ǫ > 0, there exists δ such that for every y ∈ X1 , if d1 (x, y) < δ, then
d2 (f (x), f (y)) < ǫ.
• A subset A of a metric space (X, d) is dense if
∀x ∈ X, ǫ > 0 ∃y ∈ A

d(x, y) < ǫ

• A metric space is separable if it has a countable dense subset.
• Given a sequence of points xn in a metric space (X, d), we say that x is the limit of xn if for
all ǫ > 0, there exists an N such that d(xn , x) < ǫ.
• A subset A of a metric space is closed if it contains all the limit points, that is if xn ∈ A for
all n and xn → x, then x ∈ A.
Lemma 59 (Billingsley [2, ex. 13.1]) Let (Ω, Σ) and (Ω′ , Σ′ ) be two measurable spaces, T :
Ω → Ω′ a function and A1 , A2 , . . . a countable collection of sets in Σ whose union is Ω. Let
Σn = {A | A ⊆ AN , A ∈ Σ} be a σ-algebra in An and Tn : An → Ω′ a restriction of T to An .
Then T is measurable Σ/Σ′ if and only if Tn is measurable Σn /Σ′ for every n.
A convenient way of showing that a function is Borel-measurable is to show that it is continuous
as a function between metric spaces.
Let us represent the product σ-algebra M × R × S as a Borel σ-algebra induced by a metric.
First, we define the standard metric on R, and the disjoint union of Manhattan metrics for S:
dR (w, w′ ) ,
dS (s, s′ ) ,

|w − w′ |
(P
|s|
′
′
i=1 |si − s | if |s| = |s |
∞
otherwise

We can easily verify that (S, d) generates S. We define the metric on Λ × R × S to be the
Manhattan metric:
40

d((M, w, s), (M ′ , w′ , s′ )) , dΛ (M, M ′ ) + dR (w, w′ ) + dS (s, s′ )
The following is a standard result in measure theory:
Lemma 60 (Gallay [10, Proposition 4.2 b)]) If X1 , X2 are separable metric spaces then
B(X1 × X2 ) = B(X1 ) × B(X2 )
It is obvious that (R, d) and (S, d) are separable. Now, let ΛQ be the subset of ΛP in which all
constants are rational. Then, it is easy to show that ΛQ is countable.
Lemma 61 ΛQ is a dense subset of (ΛP , d)
Proof. We need to prove that
∀M ∈ ΛP , ǫ > 0 ∃MQ ∈ ΛQ

d(M, Mq ) < ǫ

This can be easily shown by induction (the base case follows from the fact that Q is a dense
subset of R.

Lemma 62 The metric space (ΛP , d) is separable.


Proof. Corollary of Lemma 61.
Corollary 3 The σ-algebra on Λ × R × S generated by the metric d is M × R × S.

Throughout this section, we call a function “measurable” if it is Borel measurable and “continuous” if it is continuous as a function between metric spaces.
We can use lemma 59 to split the space M of expressions into subspaces of expressions of
different type, and restrict functions (such as the reduction relation) to a given type of expression,
to process different cases separately.
We write Subst(M, x, v) for M {V /x}, to emphasize the fact that substitution is a function.
Detailed definition of substitution
Subst(c, x, V ) , c
Subst(x, x, V ) , V
Subst(x, y, V ) , y if x 6= y
Subst(λx.M, x, V ) , λx.M
Subst(λx.M, y, V ) , λx.(Subst(M, y, V )) if x 6= y
Subst(M N, x, V ) , Subst(M, x, V ) Subst(N, x, V )
Subst(D(V1 , . . . , V|D| ), x, V ) , D(Subst(V1 , x, V ), . . . , Subst(V|D| , x, V ))
Subst(g(V1 , . . . , V|g| ), x, V ) , g(Subst(V1 , x, V ), . . . , Subst(V|g| , x, V ))
Subst(if W then M else L, x, V ) ,
if Subst(W, x, V ) then Subst(M, x, V ) else Subst(L, x, V )
Subst(score(V ′ ), x, V ) , score(Subst(V ′ , x, V ))
Subst(fail, x, V ) , fail
For convenience, let us also define a metric on contexts:
d([·], [·])

,

d(EM, F N ) ,
d((λx.M )E, (λx.N )F ) ,
d(E, F )

,
41

0
d(E, F ) + d(M, N )
d(M, N ) + d(E, F )
∞ otherwise

Lemma 63 d(E[M ], F [N ]) ≤ d(E, F ) + d(M, N ).
Proof. By induction on the structure of E.
If d(E, F ) = ∞, then the result is obvious, since d(M ′ , N ′ ) ≤ ∞ for all M ′ , N ′ .
Now let us assume d(E, F ) 6= ∞ and prove the result by simultaneous induction on the structure
on E and F :
• Case E = F = [·]: in this case, E[M ] = M , F [N ] = N , and d(E, F ) = 0, so obviously
d(E[M ], F [N ]) = d(E, F ) + d(M, N )
• Case E = E ′ L1 , F = F ′ L2 :
We have d(E[M ], F [N ]) = d(E ′ [M ] L1 , F ′ [N ] L2 ) = d(E ′ [M ], F ′ [N ]) + d(L1 , L2 ). By induction hypothesis, d(E ′ [M ], F ′ [N ]) ≤ d(E ′ , F ′ ) + d(M, N ), so d(E[M ], F [N ]) ≤ d(E ′ , F ′ ) +
d(M, N ) + d(L1 , L2 ) = d(E, F ) + d(M, N ).
• Case E = (λx.L1 ) E ′ , F = (λx.L2 ) F ′ :
We have d(E[M ], F [N ]) = d((λx.L1 )(E ′ [M ]), (λx.L2 )(F ′ [N ])) = d(λx.L1 , λx.L2 )+d(E ′ [M ], F ′ [N ]).
By induction hypothesis, d(E ′ [M ], F ′ [N ]) ≤ d(E ′ , F ′ ) + d(M, N ), so d(E[M ], F [N ]) ≤
d(E ′ , F ′ ) + d(λx.L1 , λx.L2 ) + d(M, N ) = d(E, F ) + d(M, N ).

Lemma 64 If d(E, F ) = ∞, then for all R1 , R2 , d(E[R1 ], F [R2 ]).
Proof. By induction on the structure of E:
• If E = [ ], then d(E, F ) = ∞ implies F 6= [ ]:
– If F = (λx.M ) F ′ , then d(E[R1 ], F [R2 ]) = d(R1 , (λx.M ) F ′ [R2 ]) = ∞, because R1 is
either not an application or of the form V1 V2 , and F ′ [R2 ] is not a value.
– If F = F ′ N , then d(E[R1 ], F [R2 ]) = d(R1 , F ′ [R2 ] N ) = ∞, because R1 is either not
an application or of the form V1 V2 , and F ′ [R2 ] is not a value.
• If E = (λx.M ) E ′ , then:
– If F = F ′ N , then d(E[R1 ], F [R2 ]) = d(λx.M, F ′ [R2 ]) + d(E ′ [R1 ], N ) = ∞, because
d(λx.M, F ′ [R2 ]) = ∞, asF ′ [R2 ] cannot be a lambda-abstraction.

– If F = (λx.N ) F ′ , then d(E, F ) = ∞ implies that either d(M, N ) = ∞ or d(E ′ , F ′ ) =
∞. We have d(E[R1 ], F [R2 ]) = d(M, N ) + d(E ′ [R1 ], F ′ [R2 ]). If d(M, N ) = ∞, then
obviously d(E[R1 ], F [R2 ]) = ∞. Otherwise, by induction hypothesis, d(E ′ , F ′ ) = ∞
gives d(E ′ [R1 ], F ′ [R2 ]) = ∞, and so d(E[R1 ], F [R2 ]) = ∞.

• If E = E ′ M and F = F ′ N , then d(E, F ) = ∞ implies that either d(M, N ) = ∞ or
d(E ′ , F ′ ) = ∞. We have d(E[R1 ], F [R2 ]) = d(M, N )+d(E ′ [R1 ], F ′ [R2 ]), so d(E ′ [R1 ], F ′ [R2 ]) =
∞ follows like in the previous case.
The property also holds in all remaining cases by symmetry of d.



Lemma 65 d(E[R1 ], F [R2 ]) = d(E, F ) + d(R1 , R2 ).
Proof. If d(E, F ) = ∞, then d(E[R1 ], F [R2 ]) = ∞ by Lemma 64, otherwise the proof is the
same as the proof of lemma 63, with inequality replaced by equality when applying the induction
hypothesis.

Lemma 66 d(Subst(M, x, V ), Subst(N, x, W )) ≤ d(M, N ) + k · d(V, W ) where k is the max of
the multiplicities of x in M and N
Proof. By simultaneous induction on the structure of M and N .

42



Let C denote the set of contexts and G the set of primitive functions. Let:
• Λappl , {E[(λx.M )V ] | E ∈ C, (λx.M ) ∈ CΛ, V ∈ V}
• Λapplc , {E[c V ] | E ∈ C, c ∈ R, V ∈ V}
• Λiftrue , {E[if true then M else N ] | E ∈ C, M, N ∈ CΛ}
• Λiffalse , {E[if false then M else N ] | E ∈ C, M, N ∈ CΛ}
• Λfail , {E[fail] | E ∈ C \ {[ ]}}
• Λprim (g) , {E[g(~c)] | E ∈ C, ~c ∈ R|g| }
S
• Λprim , g∈G Λprim (g)

• AΛif , {E[if G then M else N ] | E ∈ C, M, N ∈ CΛ, G ∈ GV}
• Λdist (D) , {E[D(~c)] | E ∈ C, ~c ∈ R|D| }
S
• Λdist , D∈D Prnd (D)
S
• AΛprim , g∈G E[g(G1 , . . . , G|g| )] | E ∈ C, G1 , . . . , G|g| ∈ GV}
• AΛdist ,

S

D∈D

E[D(G1 , . . . , G|D| )] | E ∈ C, G1 , . . . , G|D| ∈ GV}

• AΛscr , {E[score(c)] | E ∈ C, c ∈ R}
• Λscr , {E[score(c)] | E ∈ C, c ∈ (0, 1]}
Lemma 67 All the sets above are measurable.
Proof. All these sets except for Λscr are closed, so they are obviously measurable. The set Λscr is
not closed (for example, we can define a sequence of points in Λscr whose limit is score(0) ∈
/ Λscr ),
but it is still measurable:
Define a function iscr : AΛscr → R by iscr (E[score(c)]) = c. This function is continuous and
so measurable. Since the interval (0, 1] is a Borel subset of R, i−1
scr ((0, 1]) = Λscr is measurable. 
Now, we need to define the set of erroneous redexes of all types.
• RΛif , AΛif \ (Λiftrue ∪ Λiffalse ))
• RΛprim , AΛprim \ Λprim
• RΛdist , AΛdist \ Λdist
• RΛscr , AΛscr \ Λscr
• Λerror , RΛif ∪ RΛprim ∪ RΛdist ∪ RΛscr
Lemma 68 The set Λerror is measurable.
Proof. It is constructed from measurable sets by operations preserving measurability.



Define:
Λdet = Λappl ∪ Λcappl ∪ Λiftrue ∪ Λiffalse ∪ Λfail ∪ Λprim ∪ Λerror
Lemma 69 Λdet is measurable.


Proof. Λdet is a union of measurable sets.
43

Lemma 70 GV is measurable.
Proof. It is easy to see that GV is precisely the union of sets of all closed expressions of the form
c, λx.M , x and fail, so it is closed, and hence measurable.

Lemma 71 V is measurable.
Proof. V is the union of sets of all closed expressions of the form c, λx.M and x , so it is closed,
and hence measurable.


A.1

Deterministic reduction as a measurable function

Let us define a function performing one step of the reduction relation. This function has to be
defined piecewise. Let us start with sub-functions reducing deterministic redexes of the given type.
gappl
gappl (E[(λx.M ) V ])

:

Λappl → CΛ

= E[Subst(M, x, v)]

Lemma 72 gappl is measurable.
Proof. By Lemma 65, we have d(E[(λx.M )V ], F [(λx.N )W ]) = d(E, F ) + d(M, N ) + d(V, W )
and by Lemma 66, d(E[Subst(M, x, V )], F [Subst(N, x, W )]) ≤ d(E, F ) + d(M, N ) + k · d(V, W ),
where k is the maximum of the multiplicities of x in M and N .
ǫ
. Then, if d(E[(λx.M )V ], F [(λx.N )W ]) < δ, then
For any ǫ > 0, take δ = k+1
d(E[Subst(M, x, V )], F [Subst(N, x, W )])

≤ d(E, F ) + d(M, N ) + k · d(V, W )
≤ (k + 1) · (d(E, F ) + d(M, N ) + d(V, W ))
= (k + 1) · d(E[(λx.M )V ], F [(λx.N )W ])
< ǫ



Thus, gappl is continuous, and so measurable.
gapplc :
gapplc (E[c M ]) =

Λapplc → CΛ
E[fail]

Lemma 73 gapplc is measurable.


Proof. It is easy to check that gapplc is continous.
gprim

:

gprim (E[g(~c)])

=

Λprim → CΛ
E[σg (~c)]

Lemma 74 gprim is measurable.
Proof. By assumption, every primitive function g is measurable. gprim is a composition of a
function splitting a context and a redex, g and a function combining a context with a redex, all
of which are measurable.


44

giftrue

:

giftrue (E[if true then M1 else M2 ]) =
giffalse :
giffalse (E[if false then M1 else M2 ]) =

Λiftrue → CΛ

E[M1 ]
Λiffalse → CΛ
E[M2 ]

Lemma 75 giftrue and giffalse are measurable.
Proof. We have d(E[if true then M1 else N1 ], F [if true then M2 else N2 ]) = d(E, F ) +
d(M1 , M2 ) + d(N1 , N2 ) ≥ d(E[M1 ], F [M2 ]), so giftrue is continuous, and so measurable, and similarly for giffalse .

gfail

:

gfail (E[fail])

Λfail → CΛ

= fail

Lemma 76 gfail is measurable.


Proof. Obvious, since it is a constant function.
gerror

:

Λerror → CΛ

gerror (E[T ]) = E[fail]

Lemma 77 gerror is measurable.
Proof. We have d(E[T1 ], F [T2 ]) ≥ d(E, F ) = d(E[fail], F [fail]), so gerror is continuous and
hence measurable.


′
gdet
′
gdet

:

Λdet → CΛ

= gappl ∪ gapplc ∪ gprim ∪ giftrue ∪ giffalse ∪ gfail ∪ gerror

′
Lemma 78 gdet
is measurable.



Proof. Follows directly from Lemma 59.
det

′
Lemma 79 M −−→ N if and only if gdet
(M ) = N .



Proof. By inspection.

45

A.2
Let

Small- step reduction as a measurable function
Tval
Tdet
Tscr
Trnd

= GV × R × S
= Λdet × R × S
= Λscr × R × S
= {(E[D(~c)], w, c :: s) | E ∈ C, D ∈ D, ~c ∈ R|D| , w ∈ R, s ∈ S, c ∈ R,
pdf D (~c, c) > 0}

Lemma 80 Tval , Tdet , Tscr and Trnd are measurable.
Proof. The measurability of Tval , Tdet and Tscr is obvious (they are products of measurable sets),
so let us focus on Trnd .
For each distribution D, define a function iD : Λrnd (D) × R × (S \ {[]}) → R|D| × R by
iD (E[D(~c)], w, c :: s) = (c, ~c). This function is continuous, and so measurable. Then, since for
each D,Spdf D is measurable by assumption, the function jd = pdf D ◦iD is measurable. Then,
−1
((0, ∞)), and since the set of distributions is countable, Trnd is measurable. 
Trnd = D∈D jD

Let T = CΛ × R × S and let Tblocked = T \ (Tval ∪ Tdet ∪ Tscr ∪ Trnd ) be the set of non-reducible
(“stuck”) triples, whose first components are not values. Obviously, Tblocked is measurable.
Define:
gval

:

gval (G, w, s)

=

Tval → T

(fail, 0, [])

Obviously, gval is measurable.
gdet
gdet (M, w, s)

: Tdet → T
′
= (gdet
(M ), w, s)

Lemma 81 gdet is measurable.


Proof. All components of gdet are measurable.

grnd

:

Trnd → T

grnd ,
g1 (E[D(~c)], w, c :: s) ,

(g1 , g2 , g3 )
E[c]

g2 (E[D(~c)], w, c :: s) ,
g3 (E[D(~c)], w, c :: s) ,

w · pdf D (~c, c),
s

Lemma 82 grnd is measurable.
Proof. For g1 , we have d(E[c], E ′ [c′ ]) ≤ d(E, E ′ ) + d(c, c′ ) ≤ d(E, E ′ ) + d(~c, c~′ ) + d(w, w′ ) +
d(s, s′ ) = d((E[D(~c)], w, c :: s), (E ′ [D(c~′ )], w′ , c′ :: s′ )) and d((E[D(~c)], w, c :: s), (E ′ [E(c~′ )], w′ , c′ ::
s′ )) = ∞ if D 6= E, so g1 is continuous and hence Borel-measurable.
For g2 , we have g2 (E[D(~c)], w, c :: s) = gw (E[D(~c)], w, c :: s) × (pdf D ◦gc )(E[D(~c)], w, c :: s),
where gw (E[D(~c)], w, c :: s) = w and gc (E[D(~c)], w, c :: s) = (~c, c). The continuity (and so
measurability) of gw and gc can be easily checked (as for g1 above). Thus, pdf D ◦gc is a composition
of measurable functions (since distributions are assumed to be measurable), and so g2 is a pointwise
product of measurable real-valued functions, so it is measurable.
The continuity (and so measurability) of g3 can be shown in a similar way to g1 .
Hence, all the component functions of grnd are measurable, so grnd is itself measurable.

46

gscr
gscr (E[score(c)], w, s)

: Tscr → T
, (E[true], c · w, s)

Lemma 83 gscr is measurable.
Proof. The first component function of gscr can easily be shown continuous, and so measurable,
and ditto for the third component. The second component is a pointwise product of two measurable
functions, like in the grnd case. Hence, gscr is measurable.

For completeness, we also define:
gblocked
gblocked (M, w, s)

:

Tblocked → T

, (fail, 0, [])

This function is trivially measurable.
Define
g

:

T →T

g

, gval ∪ gdet ∪ gscr ∪ gblocked

Lemma 84 g is measurable.


Proof. Follows from Lemma 59.
Lemma 85 For every (M, w, s) ∈ T ,

1. If (M, w, s) → (M ′ , w′ , s′ ), then g(M, w, s) = (M ′ , w′ , s′ ).
2. If g(M, w, s) = (M ′ , w′ , s′ ) 6= (fail, 0, []) , then (M, w, s) → (M ′ , w′ , s′ ).


Proof. By inspection.

A.3

Measurability of P and O

It is easy to check that the sets GV and R+ (nonnegative reals) form ωCPOs with the orderings
fail ≤ M for all M and 0 ≤ x, respectively. This means that functions into GV and R+ also form
ωCPOs with pointwise ordering.
Define:
(
M
if M ∈ GV, s = []
ΘΛ (f )(M, w, s) ,
f (g(M, w, s)) otherwise
(
w
if M ∈ GV, s = []
Θw (f )(M, w, s) ,
f (g(M, w, s)) otherwise
It can be shown that these functions are continuous, so we can define:
⊥Λ = (M, w, s) 7→ fail
⊥w = (M, w, s) 7→ 0
O′ (M, s) , sup ΘnΛ (⊥Λ )(M, 1, s)
n

P′ (M, s) , sup Θnw (⊥w )(M, 1, s)
n

47

Lemma 86 If (M, w0 , s) ⇒ (G, w, []), then supn Θnw (⊥w )(M, w0 , s) = w and supn ΘnΛ (⊥Λ )(M, w0 , s) =
G.
Proof. By induction on the derivation of (M, w0 , s) ⇒ (G, w, []):
• If (M, w0 , s) →0 (G, w, []), and so M ∈ GV and s = [], then the equalities follow directly
from the definitions of Θw and ΘΛ .
• If (M, w0 , s) → (M ′ , w′ , s′ ) ⇒ (G, w, []), assume that supn Θnw (⊥w )(M ′ , w′ , s′ ) = w and
supn ΘnΛ (⊥Λ )(M ′ , w′ , s′ ) = G, We have M ∈
/ GV. By Lemma 85, g(M, w0 , s) = (M ′ , w′ , s′ ).
n
n
Hence supn Θw (⊥w )(M, w0 , s) = supn Θw (⊥w )(g(M, w0 , s)) = supn Θnw (⊥w )(M ′ , w′ , s′ ) =
w by induction hypothesis. Similarly, supn ΘnΛ (⊥Λ )(M, w0 , s) = G.

Corollary 4 If (M, 1, s) ⇒ (G, w, []), then P′ (M, s) = w and O′ (M, s) = G.
Lemma 87 If supn Θnw (⊥w )(M, w0 , s) = w 6= 0, then (M, w0 , s) ⇒ (G, w, []) for some G ∈ GV.
Proof. Because the supremum is taken with respect to a flat ωCPO, supn Θnw (⊥w )(M, w0 , s) =
w > 0 implies Θkw (⊥w )(M, w0 , s) = w for some k > 0. We can then prove the result by indiction
on k:
• Base case, k = 1: We must have Θw (⊥w )(M, w0 , s) = w0 , M = G ∈ GV and s = [] as
otherwise we would obtain ⊥w (M, w0 , s) = 0. Hence (M, w0 , s) reduces to (G, w0 , []) in 0
steps.
• Induction step: Θk+1
w (⊥w )(M, w0 , s) = w. If M ∈ GV and s = [], then w = w0 and (M, w0 , s)
reduces to itself in 0 steps, like in the base case. Otherwise, we have Θkw (⊥w )((M ′ , w′ , s′ )) =
w, where g(M, w0 , s) = (M ′ , w′ , s′ ). We know that (M ′ , w′ , s′ ) 6= (fail, 0, []), because
otherwise we would have w = 0. Thus, by Lemma 85, (M, w0 , s) → (M ′ , w′ , s′ ). By
induction hypothesis, (M ′ , w′ , s′ ) ⇒ (G, w, []), which implies (M, w0 , s) ⇒ (G, w, []).

Lemma 88 If supn ΘnΛ (⊥w )(M, w0 , s) = V ∈ V, then (M, w0 , s) ⇒ (V, w, []) for some w ∈ R.


Proof. Similar to the proof of Lemma 87.

Corollary 5 If there are no G, w such that (M, 1, s) ⇒ (G, w, []), then P′ (M, s) = 0 and O′ (M, s) =
fail.
Corollary 6 For any M , PM = P′ (M, ·) and OM = O′ (M, ·).
Lemma 89 If (X, Σ1 ) and (Y, Σ2 ) are measurable spaces, Y forms a flat ωCPO with a bottom
element ⊥ such that {⊥} ∈ Σ2 and f1 , f2 , . . . is a ω-chain of Σ1 /Σ2 measurable functions (on the
ωCPO with pointwise ordering), then supi fi is Σ1 /Σ2 measurable.
Proof. Since f −1 (A ∪ {⊥}) = f −1 (A) ∪ f −1 ({⊥}), we only need to show that (supi fi )−1 ({⊥}) ∈
Σ1 and (supi fi )−1 (A) ∈ Σ1 for all
/ A.
T A ∈ Σ2 such that ⊥ ∈
/ A, then
We have (supi fi )−1 ({⊥}) = i fi−1 ({⊥}), which is measurable by definition. If ⊥ ∈
−1
sup
f
(x)
∈
A
if
and
only
if
f
(x)
∈
A
for
some
i,
so
by
extensionality
of
sets,
sup
f
i
i
i
i
i (A) =
S −1

i fi (A) ⊆ Σ1 .
Lemma 90 P′ is measurable (CΛ × S)/R|R+ .

Proof. First, let us show by induction on n that Θnw (⊥w ) is measurable for every n:
• Base case, n = 0: Θ0w (⊥w ) = ⊥w is a constant function, and so trivially measurable.

48

n
• Induction step: suppose Θnw (⊥w ) is measurable. Then we have Θn+1
w (⊥w ) = Θw (Θw (⊥w )),
so it is enough to show that Θw (f ) is measurable if f is measurable:

The domain of the first case is GV × R × {[]}, which is clearly measurable. The domain of
the second case is measurable as the complement of the above set in T .

The sub-function corresponding to the first case returns the second component of its argument, so it is continuous and hence measurable. The second case is a composition of two
measurable functions, hence measurable.
Thus, Θw (f ) is measurable for any measurable f , and so Θn+1
w (⊥w ) is measurable.
By Lemma 89, supn Θnw (⊥w ) is measurable. Since P′ is a composition of supn Θnw (⊥w ) and a
continuous function mapping (M, s) to (M, 1, s), it is a composition of measurable functions, and
so it is measurable.

Lemma 91 O′ is measurable (CΛ × S)/M|GV .


Proof. Similar to the proof of Lemma 90.
Lemma 92 For any closed term M , the function PM is measurable S/R|R+ .
Proof. Since P′ is measurable, PM = P′ (M, ·) is measurable for every M ∈ CΛ.



Lemma 93 For each M , the function OM is measurable S/M|GV .
Proof. Since O′ is measurable, OM = O′ (M, ·) is measurable for every M ∈ CΛ.



Lemma 94 For all M , s, PV
M (s) = PM (s)[OM (s) ∈ V]
w
Proof. By Lemma 23, if M ⇓w
s G, then w, G are unique. If M ⇓s V , then PM (s) = w,
V
w
PM (s) and OM (s) ∈ V, so the equality holds. If M ⇓s fail, then PM (s) = w, PV
M (s) = 0 and
OM (s) ∈
/ V), so both sides of the equation are 0. If there is no G such that M ⇓w
s G, then both
sides are also 0.


Lemma 95 PV
M is measurable for every M .
V
Proof. By Lemma 94, PV
M (s) = PM (s)[OM (s) ∈ V] , so PM is a pointwise product of a measurable function and a composition of OM and an indicator function for a measurable set, hence
it is measurable.


Restatement of Lemma 92. For any closed term M , the functions PM , OM and PV
M are
all measurable; hhM ii and hhM iiV are measures on (S, S); JM KS is a measure on (GV, M|GV ); and
(JM KS )|V is a measure on (V, M|V ).
Proof. For all M ∈ CΛ, PM , OM and PV
M are measurable by lemmas 92, 93 and 95, respectively.
V
Since PM , and PV
M are obviously nonnegative, the functions hhM ii and hhM ii are measures of
V
densities PM and PM with respect to the stock measure µ [10, Section 2.3.3]. The function JM KS
is a transformation of the measure hhM ii on (S, S) by the S/M|GV -measurable function OM , so
it is a measure on (GV, M|GV ) [2, Section 13, Transformations of Measures]. Since (JM KS )|V (A) =
JM KS (A ∩ V) for every measurable set A ∈ M|GV , the function (JM KS )|V is a restriction of JM KS
to V, so it is a measure on (V, M|V ).

49

A.4

Measurability of peval

Like in the previous section, we start by giving an alternative definition of peval, using the function
g instead of referring to the reduction relation directly.
The set of closed terms CΛ is a ωCPO with respect to the partial order defined by fail ≤ G
for all G. Hence the set F of all functions (CΛ × R × S) → CΛ is a ωCPO with respect to the
pointwise order. Define Φ : F → F as:
(
M
if s = []
Φ(f )(M, w, s) =
f (g(M, w, s)) otherwise
It is easy to check that Φ is monotone and preserves suprema of ω-chains, so it is continuous.
Hence, we can define:
peval′ (M, s) = sup Φk (⊥Λ )(M, 1, s)
k

where ⊥Λ (M, w, s) = fail, as before.
We first need to show that the original peval function is well-defined.
Lemma 96 If (M, w0 , s) ⇒ (Mk , wk , sk ) → (M ′ , w′ , []) and sk 6= [] and (M, w0 , s) ⇒ (Ml , wl , sl ) →
(M ′′ , w′′ , []) and sl 6= [], then M ′ = M ′′ and w′ = w′′ .
Proof. By induction on the derivation of (M, w0 , s) ⇒ (Mk , wk , sk ):
• If (M, w0 , s) ⇒ (Mk , wk , sk ) was derived in 0 steps, we have Mk = M , wk = w and sk = s,
and so (M, w0 , s) → (M ′ , w′ , []), where s 6= [].

If (M, w0 , s) ⇒ (Ml , wl , sl ) was derived in 0 steps, then (Ml , wl , sl ) = (M, w0 , s), and so
M ′′ = M ′ and w′′ = w′ by Lemma 6.

If (M, w0 , s) ⇒ (Ml , wl , sl ) was derived in 1 or more steps, we have (M, w0 , s) → (M̂ , ŵ, ŝ) ⇒
(Ml , wl , sl ) → (M ′′ , w′′ , []) and sl 6= [], for some M̂ , ŵ, ŝ. By Lemma 6, ŝ = []. We have
(M̂ , ŵ, []) ⇒ (Ml , wl , sl ), where sl 6= []. This leads to a contradiction, as it is easy to show
that reducing a term with an empty trace cannot yield a triple with a non-empty trace (there
is no rule which adds an element to a trace)
• If (M, w0 , s) ⇒ (Mk , wk , sk ) was derived in 1 on more steps, we have (M, w0 , s) → (M ∗ , w∗ , s∗ ) →k
(Mk , wk , sk ) → (M ′ , w′ , []) for some k ≥ 0, M ∗ , w∗ , s∗ . Now, if (M, w0 , s) ⇒ (Ml , wl , sl ) was
derived in 1 or more steps, we have (M, w0 , s) → (M̂ , Ŵ , ŝ) ⇒ (Ml , wl , sl ) → (M ′′ , w′′ , [])
and sl 6= [] for some M̂ , ŵ, ŝ, where (M̂ , Ŵ , ŝ) = (M ∗ , w∗ , s∗ ) by Lemma 6. Hence, the
result follows by the induction hypothesis.
If (M, w0 , s) ⇒ (Ml , wl , sl ) was derived in 0 steps, then (Ml , wl , sl ) = (M, w0 , s), and so
(M, w0 , s) → (M ′′ , w′′ , []). By Lemma 6, this implies s∗ = [], so (M ∗ , w∗ , []) ⇒ (Mk , wk , sk )
for sk 6= [], which is impossible, as explained in the previous case.
Lemma 97 If (M, w0 , s) ⇒ (Mk , wk , sk ) → (M ′ , w′ , []) and sk 6= [], then supn Φn (⊥Λ )(M, w0 , s) =
M ′.
Proof. By induction on the length of derivation of (M, w0 , s) ⇒ (Mk , wk , sk ) → (M ′ , w′ , []).
Suppose (M, w0 , s) →k (Mk , wk , sk ) → (M ′ , w′ , []).
• Base case, k = 0: We have (M, w0 , s) → (M ′ , w′ , []) and s 6= []. Hence, by Lemma
85, g(M, w0 , s) = (M ′ , w′ , []), and so, by monotonicity of Φ, supk Φk (⊥Λ )(M, w0 , s) =
supk Φ(Φ(Φk (⊥Λ )))(M, w0 , s) = supk Φ(Φk (⊥Λ ))(M ′ , w′ , []) = M ′ , as required.
• Induction step: Let (M, w0 , s) →k+1 (Mk , wk , sk ) → (M ′ , w′ , []). Then there exist M ∗ ,
w∗ , s∗ such that (M, w0 , s) → (M ∗ , w∗ , s∗ ) →k (Mk , wk , sk ) → (M ′ , w′ , []). Now, we
have supk Φk (⊥Λ )(M, w0 , s) = supk Φ(Φk (⊥Λ ))(M, w0 , s) = supk Φk (⊥Λ )(M ∗ , w∗ , s∗ ), and
supk Φk (⊥Λ )(M ∗ , w∗ , s∗ ) = M ′ by induction hypothesis, which ends the proof.
50


Corollary 7 If (M, 1, s) ⇒ (Mk , wk , sk ) → (M ′ , w′ , []) and sk 6= [], then peval′ (M, s) = M ′ .
Lemma 98 If supn Φn (⊥Λ )(M, w0 , s) = M ′ 6= fail, then either s = [] or (M, w0 , s) ⇒ (Mk , wk , sk ) →
(M ′ , w′ , []) for some Mk , wk , sk , w′ , where sk 6= [].
Proof. Like in lemma 87, for every M , w0 , s, we must have Φk (⊥Λ )(M, w0 , s) = M ′ for some
k > 0, and we can prove the result by induction on k.
• Base case. k = 1: we must have s = [] as otherwise we would have M ′ = fail.
• Induction step: suppose Φk+1 (⊥Λ )(M, w0 , s) = M ′ . By definition of Φ, if s 6= [], we have
Φk (⊥Λ )(M ∗ , w∗ , s∗ ) = M ′ , where g(M, w0 , s) → (M ∗ , w∗ , s∗ ). Since M ′ 6= fail by assumption, Lemma 85 yields (M, w0 , s) → (M ∗ , w∗ , s∗ ). By induction hypothesis, either
s∗ = [] or (M ∗ , w∗ , s∗ ) ⇒ (M ∗∗ , w∗∗ , s∗∗ ) → (M ′ , w′′ , []) for some M ∗∗ , w∗∗ , s∗∗ , w′′ ,
where s∗∗ 6= []. In the former case, we have (M, w0 , s) ⇒ (Mk , wk , sk ) → (M ′ , w′ , []) with
(M, w0 , s) = (Mk , wk , sk ), (M ∗ , w∗ , s∗ ) = (M ′ , w′ , []) and sk 6= [], as required. In the latter
case, we have (M, w0 , s) ⇒ (M ∗∗ , w∗∗ , s∗∗ ) → (M ′ , w′′ , []), with s∗∗ 6= [].

Lemma 99 peval = peval′
Proof. We need to show that peval(M, s) = peval′ (M, s) for all M ∈ CΛ, s ∈ S.
If s = [], then the equality follows trivially from the two definitions. Now, assume s 6= [].
If peval′ (M, s) = M ′ 6= fail, then it follows from Lemma 98 that peval(M, s) = M ′ ,
Now, let peval′ (M, s) = fail and suppose that peval(M, s) = M ′ 6= fail. Since s 6= [], by
definition of peval there must be Mk , wk , sk , w′ such that (M, 1, s) ⇒ (Mk , wk , sk ) → (M ′ , w′ , [])
and sk 6= []. But by Corollary 7, this implies that peval′ (M, s) = M ′ 6= fail, which yields a
contradiction. Hence peval(M, s) = fail.

Lemma 100 For every k, pevalk = Φk (⊥λ ) is measurable.
Proof. By induction on k:
• Base case: k = 0: peval0 = ⊥λ is a constant function on CΛ × S, so trivially measurable.
• Induction step : we have pevalk+1 = Φ(pevalk ), so it is enough to show that Φ(f ) is
measurable if f is measurable. Φ(f ) is defined in pieces, so we want to use Lemma 59.
The domain of the first case is CΛ×{[]}, so obviously measurable. The domain of the second
case is p−1 (g −1 (CΛ × R × S) ∩ (CΛ × {1} × (S \ {[]}))), and p(M, s) = (M, 1, s) is continuous,
and so measurable. Hence, the domain is measurable. Finally, the domain of the last case
is the complement of the union of the two above measurable sets, which means it is also
measurable.
Thus, we only need to show that the functions corresponding to these three cases are measurable. This is obvious in the first and third case, because the corresonding functions are
constant. The function for the second case is φ(M, s) = f (g(p(M, s))), where p is as defined
above and g ′ is the restriction of g to g −1 (CΛ × R × S), which is measurable since restrictions preserve measrability. Since composition of measurable functions is measurable, φ is
measurable.
Thus, pevalk+1 is measurable, as required.



Lemma 101 peval′ is a measurable function CΛ × S → CΛ.


Proof. Corollary of Lemmas 100 and 89.
51

Restatement of Lemma 50. peval is a measurable function CΛ × S → CΛ.



Proof. Corollary of Lemma 101 and Lemma 99.
Lemma 102 For every M ∈ CΛ, c ∈ R, s ∈ S, peval(peval(M, [c]), s) ≤ peval(M, c :: s)
Proof. Define a property P ⊆ F :

P (f ) ⇔ sup Φk (⊥λ )(Φ(f )(M, [c]), s) ≤ sup Φk (⊥λ )(M, c :: s) ∀M, c, s
k

k

k

λ

k

Since supk Φ (⊥ ) is a fixpoint of Φ, Φ(supk Φ (⊥λ )) = supk Φk (⊥λ ), so
P (sup Φk (⊥λ )) ⇐⇒ sup Φk (⊥λ )(sup Φl (⊥λ )(M, [c]), s) ≤ sup Φk (⊥λ )(M, c :: s)
k

k

l

k

∀M, c, s

So we only need to prove P (supk Φk (⊥λ )).
To show that the property P is ω-inductive, let f1 ≤ f2 ≤ . . . be a ω-chain and supi fi its
limit. Then Φ(f1 ) ≤ Φ(f2 ) ≤ . . . and supi Φ(fi ) = Φ(supi fi ). For all M , s, we have
Φ(sup fi )(M, s) = (sup Φ(fi ))(M, s) = sup(Φ(fi )(M, s))
i

i

i

Note that either Φ(fi )(M, s) = fail for all i or there is some n such that Φ(fn )(M, s) ∈ V
and Φ(fm )(M, s) = Φ(fn )(M, s) for all m > n. In either case, there is a n(M, s) such that
supi (Φ(fi )(M, s)) = Φ(fn(M,s) )(M, s). Hence
P (sup fi ) ⇔ sup Φk (⊥λ )(Φ(sup fi )(M, [c]), s) ≤ sup Φk (⊥λ )(M, c :: s) ∀M, c, s
i

i

k

k

⇔ sup Φk (⊥λ )(Φ(fn(M,[c]) )(M, [c]), s) ≤ sup Φk (⊥λ )(M, c :: s) ∀M, c, s
k

k

⇔ P (fn(M,[c]) )
as required.
Now we can prove the desired property by Scott induction:
• Base case:
P (⊥λ ) ⇔ sup Φk (⊥λ )(Φ(⊥λ )(M, [c]), s) ≤ sup Φk (⊥λ )(M, c :: s) ∀M, c, s
k

k

For any M , c, s, we have
sup Φk (⊥λ )(Φ(⊥λ )(M, [c]), s) = sup Φk (⊥λ )(fail, s) = fail ≤ sup Φk (⊥λ )(M, c :: s)
k

k

k

as required.
• Induction step: We need to show that for all f such that P (f ), P (Φ(f )) holds, that is
sup Φk (⊥λ )(Φ(Φ(f ))(M, [c]), s) ≤ sup Φk (⊥λ )(M, c :: s) ∀M, c, s
k

k

′

– Case (M, 1, [c]) → (M , w, [c]):
LHS

=

sup Φk (⊥λ )(Φ(Φ(f ))(M, [c]), s)
k

=

sup Φk (⊥λ )(Φ(f )(M ′ , [c]), s)
k

(by assumption) ≤
=

sup Φk (⊥λ )(M ′ , c :: s)
k

Φ(sup Φk (⊥λ ))(M, c :: s)
k

=

(sup Φk (⊥λ )(M, c :: s)

=

RHS

k

52

– Case (M, 1, [c]) → (M ′ , w, []):
LHS

=

sup Φk (⊥λ )(Φ(Φ(f ))(M, [c]), s)

=

sup Φk (⊥λ )(Φ(f )(M ′ , []), s)

k
k

=

sup Φk (⊥λ )(M ′ , s)

=

Φ(sup Φk (⊥λ ))(M, c :: s)

=

(sup Φk (⊥λ )(M, c :: s)

=

RHS

=

sup Φk (⊥λ )(Φ(Φ(f ))(M, [c]), s)

=

sup Φk (⊥λ )(fail, s)

k
k
k

– Case (M, 1, [c]) 6→:
LHS

k
k

=

Φ(sup Φk (⊥λ ))(M, c :: s)

=

(sup Φk (⊥λ )(M, c :: s)

=

RHS

k
k

Therefore, P (supk Φk (⊥λ )), holds, and so peval(peval(M, [c]), s) ≤ peval(M, c :: s) for all
closed M , c, s.

Lemma 103 For every M ∈ CΛ, c ∈ R, s ∈ S, peval(peval(M, [c]), s) ≥ peval(M, c :: s)
Proof. Like in the previous lemma, we use Scott induction. Define the property:
Q(f ) ⇔ f (M, c :: s) ≤ sup Φk (⊥λ )(sup Φl (⊥λ )(M, [c]), s)
k
λ

l

∀M, c, s

∧ f ≤ sup Φk (⊥ )
k

We need to show that Q(supk Φk (⊥λ )) holds.
First, we need to verify that Q is ω-inductive. This is obvious for the second conjunct, so let us
concentrate on the first. Once again, we use the property that for all ω-chains f1 ≤ f2 ≤ . . . and
M , s, the chain f1 (M, s) ≤ f2 (M, s) ≤ . . . will eventually be stationary. For all M ,c,s, we have
(supi fi )(M, c :: s) = fn(M,c,s) (M, c :: s) for some n(M, c, s). Then for every M ,c,s, the inequality
(sup fi )(M, c :: s) ≤ sup Φk (⊥λ )(sup Φl (⊥λ )(M, [c]), s)
i

k

l

follows from Q(fn(M,c,s) ).
• Base case:
Q(⊥λ ) ⇔ ⊥λ (M, c :: s) ≤ sup Φk (⊥λ )(sup Φl (⊥λ )(M, [c]), s)
k
λ

l

∧ ⊥λ ≤ sup Φk (⊥ )
k

Both inequalities are obvious, because the LHS is always fail.

53

∀M, c, s

• Induction step: Give Q(f ), for every M , c, s we need to show:
sup Φk (⊥λ )(sup Φl (⊥λ )(M, [c]), s)

Φ(f )(M, c :: s) ≤

k

l

∀M, c, s

sup Φk (⊥λ )

Φ(f ) ≤

k

Again, the second inequality is obvious, so let us concentrate on the first.
– Case (M, 1, [c]) → (M ′ , w, [c]):

f (M ′ , c :: s)
sup Φk (⊥λ )(sup Φl (⊥λ )(M ′ , [c]), s)

LHS =
(by first assumption) ≤

k

l

sup Φk (⊥λ )(Φ(sup Φl (⊥λ ))(M, [c]), s)

=

k

l
k

λ

=

sup Φ (⊥ )(sup Φl (⊥λ )(M, [c]), s)

=

RHS

k

– Case (M, 1, [c]) → (M ′ , w, []):
LHS

l

= f (M ′ , s)

(by second assumption) ≤ sup Φk (⊥λ )(M ′ , s)
k

= sup Φk (⊥λ )(Φ(sup Φl (⊥λ ))(M ′ , []), s)
k

l
k

λ

= sup Φ (⊥ )(sup Φl (⊥λ )(M ′ , []), s)
k

l

= sup Φk (⊥λ )(Φ(sup Φl (⊥λ ))(M, [c]), s)
k

l

= sup Φk (⊥λ )(sup Φl (⊥λ )(M, [c]), s)
k

l

= RHS
– Case (M, 1, [c]) 6→:
LHS

= fail
≤ RHS


As required.
Restatement of Lemma 48. peval(peval(M, [c]), s) = peval(M, c :: s)



Proof. Follows from Lemmas 102 and 103.

Restatement of Lemma 49. For all closed M , s, t, peval(peval(M, s), t) = peval(M, s@t)
Proof. By induction on |s|.

• Base case: s = []. We have peval(M, []) = M (by definition of peval), so the result is trivial.

• Induction step: s = c :: s′ .
We want peval(peval(M, c :: s), t) = peval(M, c :: s@t).
We have:
LHS =
(by Lemma 48) =
(by induction hypothesis) =
(by Lemma 48) =

peval(peval(M, c :: s), t)
peval(peval(peval(M, [c]), s), t)
(peval(peval(M, [c]), s@t)
peval(M, [c] :: s@t)


54

A.5

Measurability of q and Q

Lemma 104 For all s ∈ S and M ∈ CΛ,

R

q (s, t)µ(dt)
S\[] M

≤1

To prove this lemma, we need some auxiliary results:
[]

Lemma 105 If M ⇓w G and M ⇓sw′ G′ , then s = [].
[]



Proof. By induction on the derivation of M ⇓w G.
V
Lemma 106 If PV
M ([]) > 0, then PM (t) = 0 for all t 6= [].



Proof. Follows directly from Lemma 105.

Lemma 107 (Tonelli’s theorem for sums and integrals, 1.4.46 in [36]) If (Ω, Σ, µ) is a measure space and f1 , f2 , . . . a sequence of non-negative measurable functions, then
∞
X

Z

fi (x) µ(dx) =

Ω i=1

∞ Z
X

fi (x) µ(dx)

Ω

i=1



Proof. Follows from the monotone convergence theorem.

Lemma 108 (Linearity of Lebesgue integral, 1.4.37 ii) from [36]) If (Ω, Σ) is a measurable space, f a non-negative measurable function, and µi , µ2 , . . . a sequence of measures on Σ,
then
Z
∞ Z
∞
X
X
f (x) µi (dx)
µi (dx) =
f (x)
Ω

Ω

i=1

i=1

Lemma 109 (Ex. 1.4.36 xi) from [36]) If (Ω, Σ, µ) is a measure space and f a nonnegative
measurable function on Ω and B ∈ Σ and f B a restriction of f to B, then
Z
Z
f (x)[x ∈ B] µ(dx) =
f (x) µB (dx)
Ω

B

Below we write q(s, t) as qM (s, t), to make the dependency on M explicit.
∗
Let qM
be defined as follows:
(
if t = []
PV
∗
M ([])
qM
(s, t) =
qM (s, t) otherwise
Lemma 110 For all M ∈ CΛ and s, y ∈ S
(
PV
M (t)
∗
qM
(s, t) =
∗
pdf Gaussian (s1 , σ 2 , t1 )qpeval(M,[s
([s2 , . . . s|s| ], [t2 , . . . t|t| ])
1 ])

if s = [] or t = []
otherwise

Proof. By induction on |s|:
• Case s = []:
∗
∗
If t = [], the result follows directly from the definition of qM
. Otherwise, qM
([], t) =
V
qM ([], t) = PM
(t), as required.

• Case |s| = n + 1 > 0:

Again, if t = [], the result follows immediately. Otherwise, we have
∗
qM
(s, t) = qM (s, t) = Πki=1 (pdf Gaussian (si , σ 2 , ti ))PV
peval(M,[t1 ,...,tk ]) (t)

55

where k = min(|s|, |t|) > 0. Hence
∗
qM
(s, t)

= pdf Gaussian(s1 , σ 2 , t1 )Πki=2 (pdf Gaussian (si , σ 2 , ti ))PV
peval(M,[t1 ,...,tk ]) ([tk+1 , . . . , t|t| ])

(by Lemma 48) = pdf Gaussian(s1 , σ 2 , t1 )Πki=2 (pdf Gaussian (si , σ 2 , ti ))PV
peval(peval(M,[t1 ]),[t2 ,...,tk ]) ([tk+1 , . . . , t|t| ])
∗
= (pdf Gaussian (s1 , σ 2 , t1 ))qpeval(M,[s
([s2 , . . . , s|s| )], [t2 , . . . , t|t| ])
1 ])



as required.
Lemma 111 If PV
M ([]) > 0, then peval(M, t) = fail for every t 6= [].
[]

Proof. It PV
M ([]) = w > 0, then we must have M ⇓w V for some V ∈ V, which implies
(M, 1, []) ⇒ (G, w, []). Using Lemma 15, we can easily show by induction that (M, 1, t) ⇒ (G, w, t)
for any t 6= []. Because the reduction relation is deterministic, this implies that there are no M ′ ,
w′ such that (M, 1, t) ⇒ (M ′ , w′ , []) (if there were, we would have (M ′ , w′ , []) ⇒ (G, w, t), but no
reduction rule can add an element to a trace). This means that peval, by applying reduction
repeatedly, will never reach (M ′ , []) for any M ′ , so peval(M, t) = fail.

∗
Lemma 112 If PV
M ([]) > 0, then qM (s, t) = 0 for all s ∈ S, t 6= [].



Proof. Follows easily from Lemma 111.
Restatement of Lemma 104 . For all s ∈ S and M ∈ CΛ,
Proof. By induction on |s|.

R

q (s, t)µ(dt)
S\[] M

• Base case: s = []
Z

=
≤

Z

Z

qM ([], t) µ(dt)
S\{[]}

S\{[]}

PV
M (t) µ(dt)

PM (t) µ(dt)
S

= hhM ii(S)
= hhM ii(O−1
M (GV))

by Theorem 3

= JM KS (GV)
= JM K(GV)
≤ 1

because JM K is a sub-probability distribution.
• Induction step: s 6= []

56

≤1

We have:
Z

Z

=
(by Thm 16.9 from Billingsley)

qM (s, t) µ(dt)
S\{[]}
∗
qM
(s, t) µ(dt)

S\{[]}

∞ Z
X

=

∗
qM
(s, t) µ(dt)

Ri

i=1

∞ Z
X

(by Lemma 109) =

∗
qM
(s, t) λi (dt)

Ri

i=1

∞ Z
X

=

i=1

∞ Z
X

(by Fubini’s theorem) =
(by Lemma 107) =

Z

=

pdf Gaussian(s1 , σ 2 , t1 )

Z

Ri−1

R

i=1

Z

∗
([s2 , . . . , s|s| ], [t2 , . . . , t|t| ]) λi (dt)
pdf Gaussian(s1 , σ 2 , t1 )qpeval(M,[t
1 ])

Ri

pdf Gaussian(s1 , σ 2 , t1 )
R

∞ Z
X
i=0

2

pdf Gaussian(s1 , σ , t1 )

Ri

Z

{[]}

R

Z

S\{[]}

∗
(s′ , t′ )
qpeval(M,[t
1 ])

∗
qpeval(M,[t
(s′ , t′ ) λi−1 (dt′ ) λ(dt1 )
1 ])

∗
(s′ , t′ ) λi (dt′ ) λ(dt1 )
qpeval(M,[t
1 ])

′
′
PV
peval(M,[t1 ]) (t ) µ(dt ) +

′

!

µ(dt )

λ(dt1 )

Now, we need to show that for all N ,
Z

{[]}

′
′
PV
N (t ) µ(dt ) +

Z

S\{[]}

∗
qN
(s′ , t′ ) µ(dt′ ) ≤ 1

(3)

R V ′
R
′
′
′
First, note that {[]} PV
N (t ) µ(dt ) ≤ S PN (t ) µ(dt ) ≤ 1, by the same property as the
R
′
V
one used in the base case. We also have {[]} PV
N (t ) µ(dt) = PN ([]), so by Lemma 112, if
V
PN ([]) > 0, then
Z
Z
Z
′
′
∗
′ ′
′
V ′
′
PV
qN (s , t ) µ(dt ) =
PN (t ) µ(dt ) +
N (t ) µ(dt ) ≤ 1
{[]}

{[]}

S\{[]}

On the other hand, if PV
N ([]) = 0, then
Z
Z
Z
∗
′ ′
′
V ′
′
qN (s , t ) µ(dt ) =
PN (t ) µ(dt )+
{[]}

∗
qN
(s′ , t′ )

µ(dt ) =

S\{[]}

S\{[]}

′

Z

S\{[]}

qN (s′ , t′ ) µ(dt′ ) ≤ 1

by induction hypothesis.
Hence:
Z

qM (s, t) µ(dt)

S\{[]}

≤
=

Z

pdf Gaussian (s1 , σ 2 , t1 ) λ(dt1 )

R

1



as required.
57

Restatement of Lemma 51. For any closed program M , the transition density q(·, ·) : (S×S) →
R+ is measurable.
Proof. It is enough to show that q(s, t) is measurable for every |s| = n and |t| = m, then the
result follows from Lemma 59.
Note that a function taking a sequence s and returning any subsequence of it is trivially
continuous and measurable, so for any function of s and t to be measurable, it is enough to show
that it is measurable as a function of some projections of s and t.
• If m > 0 and n < m, then we have q(s, t) = Πni=1 pdf Gaussian (s1 , σ 2 , ti )PV
peval(M,t1..n ) (tn+1..m ) =
n
2
′
′
Πi=1 pdf Gaussian(si , σ , ti )P (peval(M, t1..n ), tn+1..m )[O (peval(M, t1..n ), tn+1..m ) ∈ V].
Each pdf Gaussian (si , σ 2 , ti ) is measurable, as a composition of a function projecting (si , ti )
from (s, t) and the Gaussian pdf, so their pointwise product must be measurable.

Now, P′ is measurable, and the function mapping (s, t) to (peval(M, t1..n ), tn+1..m ) is a pair
of two measurable functions, one of which is a composition of the measurable peval(M, ·)
and a projection of t1..n , and the other just a projection of tn+1..m ). Hence, the function
mapping (s, t) to P′ (peval(M, t1..n ), tn+1..m ) is a composition of measurable functions.
Finally, [O′ (peval(M, t1..n ), tn+1..m ) ∈ V] is a composition of the measurable function mapping (s, t) to (peval(M, t1..n ), tn+1..m ) and the indicator function for the measurable set V,
thus it is measurable.
Hence, q(s, t) is a pointwise product of measurable functions, so it is measurable.
2
V
• If m > 0 and n ≥ m, then q(s, t) = Πm
i=1 pdf Gaussian (s1 , σ , ti )Ppeval(M,t) ([])
2
′
′
= Πm
i=1 pdf Gaussian (si , σ , ti )P (peval(M, t), [])[O (peval(M, t), []) ∈ V].

2
Now, the function mapping (s, t) to Πm
i=1 pdf Gaussian (si , σ , ti ) is measurable like in the previous case. The function mapping (s, t) to (peval(M, t), []) is a pairing of two measurable
functions, one being a composition of the projection of t and peval(M, ·), the other being a
constant function returning []. Hence, P′ (peval(M, t), []) is a composition of two measurable
functions. Meanwhile, [O′ (peval(M, t), []) ∈ V] is a composition of a measurable function
and an indicator function.
R
• If m = 0, then q(s, []) = 1 − S\{[]} q(s, t) µ(dt). Since we have already shown that q(s, t) is
R
measurable on S × (S \ []), S\{[]} q(s, t) µ(dt) is measurable by Fubini’s theorem, so q(s, []) is
a difference of measurable functions, and hence it is measurable.


Restatement of Lemma 52. The function Q is a probability kernel on (S, S).
Proof. We need to verify the two properties of probability kernels:
1. For every s ∈ S, Q(s, ·) is a probability distribution on S. Since
R for every s ∈ S, q(s, ·) is
non-negative measurable S (by [2, Theorem 18.1]), Q(s, B) = B q(s, y)µ(dy) (as a function
of B) is a well-defined measure for all s ∈ S. Finally, Q(s, S) = Q(s, []) + Q(s, S \ {[]}) = 1.
2. For every B ∈ S, Q(·, B) is a non-negative measurable function on S: Since (S, S, µ)
is
R a σ-finite measure space, q(·, ·) is non-negative and measurable S × S and Q(s, B) =
q(s, y)µ(ds), this follows from [2, Theorem 18.3].

B

References
[1] S. Bhat, J. Borgström, A. D. Gordon, and C. V. Russo. Deriving probability density functions
from probabilistic functional programs. In N. Piterman and S. A. Smolka, editors, Proceedings
of TACAS 2013, volume 7795 of LNCS, pages 508–522. Springer, 2013.

58

[2] P. Billingsley. Probability and Measure. Wiley-Interscience, third edition, 1995.
[3] A. Bizjak and L. Birkedal. Step-indexed logical relations for probability. In A. M. Pitts,
editor, Proceedings of FoSSaCS 2015, volume 9034 of LNCS, pages 279–294. Springer, 2015.
[4] J. Borgström, U. Dal Lago, A. D. Gordon, and M. Szymczak. A lambda-calculus foundation
for universal probabilistic programming (long version). CoRR, abs/1512.08990, 2015.
[5] P. Cousot and M. Monerau. Probabilistic abstract interpretation. In Proceedings of ESOP
2012, volume 7211 of LNCS, pages 166–190. Springer, 2012.
[6] V. Danos and T. Ehrhard. Probabilistic coherence spaces as a model of higher-order probabilistic computation. Information and Computation, 209(6):966–991, 2011.
[7] V. Danos and R. Harmer. Probabilistic game semantics. ACM Transactions on Computational
Logic, 3(3):359–382, 2002.
[8] T. Ehrhard, C. Tasson, and M. Pagani. Probabilistic coherence spaces are fully abstract for
probabilistic PCF. In Proceedings of POPL 2014, pages 309–320. ACM, 2014.
[9] L. M. Ferrer Fioriti and H. Hermanns. Probabilistic termination: Soundness, completeness,
and compositionality. In Proceedings of POPL 2015, pages 489–501. ACM, 2015.
[10] T. Gallay. Théorie de la mesure et de l’intégration. 2009. Course notes available online at
http://im2ag-webmath.e.ujf-grenoble.fr/enseignement2/IMG/pdf/integrationa.pdf.
[11] S. Goldwasser and S. Micali. Probabilistic encryption. Journal of Computer and System
Sciences, 28(2):270–299, 1984.
[12] N. D. Goodman. The principles and practice of probabilistic programming. In Proceedings
of POPL 2013, pages 399–402. ACM, 2013.
[13] N. D. Goodman and A. Stuhlmüller. The design and implementation of probabilistic programming languages. http://dippl.org, 2014.
[14] N. D. Goodman and J. B.
http://probmods.org, 2014.

Tenenbaum.

Probabilistic

models

of

cognition.

[15] N. D. Goodman, V. K. Mansinghka, D. M. Roy, K. Bonawitz, and J. B. Tenenbaum. Church:
a language for generative models. In D. A. McAllester and P. Myllymäki, editors, Proceedings
of UAI 2008, pages 220–229. AUAI Press, 2008.
[16] A. D. Gordon, T. A. Henzinger, A. V. Nori, and S. K. Rajamani. Probabilistic programming.
In M. B. Dwyer and J. Herbsleb, editors, Proceedings of FOSE 2014, pages 167–181. ACM,
2014.
[17] W. K. Hastings. Monte Carlo sampling methods using Markov chains and their applications.
Biometrika, 57:97–109, 1970.
[18] M. D. Homan and A. Gelman. The no-u-turn sampler: Adaptively setting path lengths in
Hamiltonian Monte Carlo. Journal of Machine Learning Research, 15:1593–1623, 2014.
[19] C. Hur, A. V. Nori, S. K. Rajamani, and S. Samuel. A provably correct sampler for probabilistic programs. In P. Harsha and G. Ramalingam, editors, Proceedings of FSTTCS 2015,
volume 45 of LIPIcs, pages 475–488. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015.
[20] C. Jones. Probabilistic Non-determinism. PhD thesis, University of Edinburgh, 1990. Available as Technical Report CST-6390.
[21] C. Jones and G. D. Plotkin. A probabilistic powerdomain of evaluations. In Proceedings of
LICS 1989, pages 186–195. ACM, 1989.
59

[22] O. Kiselyov. Problems of the lightweight implementation of probabilistic programming, 2016.
Poster at PPS’2016 workshop.
[23] D. Kozen. Semantics of probabilistic programs. In Proceedings of FOCS 1979, pages 101–114.
IEEE Computer Society, 1979.
[24] C. D. Manning and H. Schütze. Foundations of statistical natural language processing. MIT
Press, 1999.
[25] V. K. Mansinghka, D. Selsam, and Y. N. Perov. Venture: a higher-order probabilistic programming platform with programmable inference. CoRR, abs/1404.0099, 2014.
[26] N. Metropolis, A. W. Rosenbluth, M. N. Rosenbluth, A. H. Teller, and E. Teller. Equations of
state calculations by fast computing machines. Journal of Chemical Physics, 21(6):1087–1092,
1953.
[27] A. V. Nori, C. Hur, S. K. Rajamani, and S. Samuel. R2: an efficient MCMC sampler for
probabilistic programs. In C. E. Brodley and P. Stone, editors, Proceedings of AAAI 2014,
pages 2476–2482. AAAI Press, 2014.
[28] P. Panangaden. The category of Markov kernels. Electronic Notes in Theoretical Computer
Science, 22:171–187, 1999. In proceedings of PROBMIV 1998.
[29] P. Panangaden. Labelled Markov Processes. Imperial College Press, 2009.
[30] S. Park, F. Pfenning, and S. Thrun. A probabilistic language based upon sampling functions.
ACM Transactions on Programming Languages and Systems, 31:1, 2008.
[31] J. Pearl. Probabilistic reasoning in intelligent systems: networks of plausible inference. Morgan Kaufmann, 1988.
[32] N. Ramsey and A. Pfeffer. Stochastic lambda calculus and monads of probability distributions.
In Proceedings of POPL 2002, pages 154–165, 2002.
[33] S. J. Russell. Unifying logic and probability. Communications of the ACM, 58(7):88–97, 2015.
[34] A. Scibior, Z. Ghahramani, and A. D. Gordon. Practical probabilistic programming with
monads. In B. Lippmeier, editor, Proceedings of Haskell 2015, pages 165–176. ACM, 2015.
[35] S. Staton, H. Yang, C. Heunen, O. Kammar, and F. Wood. Semantics for probabilistic
programming: higher-order functions, continuous distributions, and soft constraints. CoRR,
abs/1601.04943, 2016.
[36] T. Tao. An Introduction to Measure Theory. AMS, 2011.
[37] S. Thrun. Robotic mapping: A survey. In G. Lakemeyer and B. Nebel, editors, Exploring
artificial intelligence in the new millennium, pages 1–35. Morgan Kaufmann, 2002.
[38] L. Tierney. Markov chains for exploring posterior distributions. The Annals of Statistics, 22
(4):1701–1728, 1994.
[39] D. Tolpin, J. van de Meent, and F. Wood. Probabilistic programming in Anglican. In
A. Bifet, M. May, B. Zadrozny, R. Gavaldà, D. Pedreschi, F. Bonchi, J. S. Cardoso, and
M. Spiliopoulou, editors, Proceedings of ECML PKDD 2015, Part III, volume 9286 of LNCS,
pages 308–311. Springer, 2015.
[40] N. Toronto.
Useful Languages for Probabilistic Modeling and
ence.
PhD thesis, Brigham Young University, Provo, UT, 2014.
https://www.cs.umd.edu/~ntoronto/papers/toronto-2014diss.pdf.

60

InferURL

[41] N. Toronto, J. McCarthy, and D. V. Horn. Running probabilistic programs backwards. In
J. Vitek, editor, Proceedings of ESOP 2015, volume 9032 of LNCS, pages 53–79. Springer,
2015.
[42] D. Wingate, A. Stuhlmüller, and N. D. Goodman. Lightweight implementations of probabilistic programming languages via transformational compilation. In G. J. Gordon and D. Dunson,
editors, Proceedings of AISTATS 2011, volume 15 of JMLR: Workshop and Conference Proceedings, pages 770–778. JMLR, 2011.

61

