From Bayesian Notation to Pure Racket
via Discrete Measure-Theoretic Probability in λZFC
Neil Toronto and Jay McCarthy
PLT @ Brigham Young University, Provo, Utah, USA
neil.toronto@gmail.com and jay@cs.byu.edu

Abstract. Bayesian practitioners build models of the world without regarding how difficult it will be to answer questions about them. Whenanswering questions, they put off approximating as long as possible, andusually must write programs to compute converging approximations.
Writing the programs is distracting, tedious and error-prone, and wewish to relieve them of it by providing languages and compilers.
Their style constrains our work: the tools we provide cannot approximate
early. Our approach to meeting this constraint is to 1) determine theirnotation’s meaning in a suitable theoretical framework; 2) generalize ourinterpretation in an uncomputable, exact semantics; 3) approximate theexact semantics and prove convergence; and 4) implement the approximating semantics in Racket (formerly PLT Scheme). In this way, wedefine languages with at least as much exactness as Bayesian practitioners have in mind, and also put off approximating as long as possible.
In this paper, we demonstrate the approach using our preliminary work
on discrete (countably infinite) Bayesian models.
Keywords: Semantics, Domain-specific languages, Probability theory

1

Introduction

Bayesian practitioners define models, or probabilistic relationships among objects of study, without regard to whether future calculations are closed-form or
tractable. They are loath to make simplifying assumptions. (If some probabilistic phenomenon is best described by an unsolvable integral or infinitely many
distributions, so be it.) When they must approximate, they often create twomodels: an “ideal” model first, and a second model that approximates it.
Because they create models without regard to future calculations, they usually must accept approximate answers to queries about them. Typically, they
adapt algorithms that compute converging approximations in programming languages they are familiar with. The process is tedious and error-prone, and involves much performance tuning and manual optimization. It is by far the mosttime-consuming part of their work—and also the most automatable part.
They follow this process to adhere to an overriding philosophy: an approximate answer to the right question is worth more than an exact answer to an
approximate question. Thus, they put off approximating as long as possible.

We must also adhere to this philosophy because Bayesian practitioners areunlikely to use a language that requires them to approximate early, or thatapproximates earlier than they would. We have found that a good way to put
the philosophy into practice in language design is to create two semantics: an“ideal,” or exact semantics first, and a converging, approximating semantics.
1.1

Theory of Probability

Measure-theoretic probability is the most successful theory of probability in precision, maturity, and explanatory power. In particular, it explains every Bayesianmodel. We therefore define the exact semantics as a transformation from Bayesian
notation to measure-theoretic calculations.
Measure theory treats finite, countably infinite, and uncountably infinite
probabilistic outcomes uniformly, but with significant complexity. Though there
are relatively few important Bayesian models that require countably many outcomes but not uncountably many, in our preliminary work, we deal with only
countable sets. This choice avoids most of measure theory’s complexity while
retaining its functional structure, and still requires approximation.
1.2

Approach and Target Language

For three categories of Bayesian notation, we
1. Manually interpret an unambiguous subclass of typical notation.
2. Mechanize the interpretation with a semantic function.
3. If necessary, create an approximation and prove convergence.
4. Implement the approximation in Racket [3] (formerly PLT Scheme).
This approach is most effective if the target language can express measuretheoretic calculations and is similar to Racket in structure and semantics.
To this end, we are concurrently developing λZFC : an untyped, call-by-value
lambda calculus extended with sets as values, and primitive set operators that
correspond with the Zermelo-Fraenkel axioms and Choice. Mixing lambdas andsets has been done in automated theorem proving [17, 18, 5]; it is possible todefine exact real arithmetic, and easy to express infinite set operations and infinite sums. For this paper, we assume those operations are already defined. We
freely use syntactic sugar like infix, summation, set comprehensions, and patternmatching definitions. In short, we intend λZFC to be contemporary mathematics
with well-defined lambdas, or a practical lambda calculus with infinite sets.
For example, image is a map-like primitive set operator corresponding to
the replacement axiom schema. If f is a lambda and A is a set, image f A ={f x | x ∈ A} applies f to every element of A and returns the set of results.
Besides lambdas, λZFC has an another class of applicable values: set-theoretic
functions, or mappings. A mapping is just a set of pairs (x, y) where each x
is unique. If g is a mapping and x is in its domain, g x returns the y for which(x, y) ∈ g. Restricting a lambda f to a domain A returns a mapping:f A = {(x, f x) | x ∈ A} = image (λx. (x, f x)) A(1)

Mappings can also be restricted using (1). We often write mappings as λ(x ∈ A).e
instead of (λx.e) A . We think of (A, f ) as a lazy mapping.
Though λZFC has no formal type system, we find it helpful to reason abouttypes informally. When we do, A ⇒ B is a lambda or mapping type, A → B is
the set of total mappings from A to B, and a set is a membership proposition.
1.3

Bayesian Languages

The Bayesian notation we interpret falls into three categories:
1. Expressions, which have no side effects, with RJ·K : λZFC ⇒ λZFC .
2. Queries, which observe side effects, with PJ·K , DJ·K : propositions ⇒ λZFC .
3. Statements, which create side effects, with MJ·K : statements ⇒ λZFC .
We use λZFC as a term language for all of our mathematics. We write Bayesian
notation in sans serif, Racket in fixed width, common keywords in bold andinvented keywords in bold italics. We omit proofs for space.

2

The Expression Language

2.1

Background Theory: Random Variables

Most practitioners of probability understand random variables as free variables
whose values have ambient probabilities. But measure-theoretic probability defines a random variable X as a total mapping
X : Ω → SX

(2)

where Ω and SX are sets called sample spaces, with elements called outcomes.
Random variables define and limit what is observable about any outcome ω ∈ Ω,
so we call outcomes in SX observable outcomes.
Example 1. Suppose we want to encode, as a random variable E, the act ofobserving whether the outcome of a die roll is even or odd.
A complicated way is to define Ω as the possible states of the universe.
E : Ω → {even, odd } must simulate the universe until the die is still, and thenrecognize the outcome. Hopefully, the probability that E ω = even is 12 .
A tractable way defines Ω = {1, 2, 3, 4, 5, 6} and E ω = even if ω ∈ {2, 4, 6},otherwise odd . The probability that E ω = even is the sum of probabilities ofevery even ω ∈ Ω, or 16 + 16 + 61 = 12 .
If we are interested in observing only evenness, we can define Ω = {even, odd },each with probability 21 , and E ω = ω.
tu
Random variables enable a kind of probabilistic abstraction. The example
does it twice. The first makes calculating the probability that E ω = eventractable. The second is an optimization. In fact, redefining Ω, the randomvariables, and the probabilities of outcomes—without changing the probabilitiesof observable outcomes—is the essence of measure-theoretic optimization.
Defining random variables as functions is also a good factorization: it separates nondeterminism from assigning probabilities. It allows us to interpret
expressions involving random variables without considering probabilities at all.

RJXK = X

RJxK = pure x

RJvK = pure v

RJ(ef e1 . . . en )K = ap ∗ RJef K RJe1 K . . . RJen Kqy
R λx1 . . . xn .e = λω.λx1 . . . xn . (RJeK ω)pure c = λω.c,ap ∗ F X1 . . . Xn = λω. ((F ω) (X1 ω) . . . (Xn ω))

Fig. 1. Random variable expression semantics. The source and target language are bothλZFC . Conditionals and primitive operators are trivial special cases of application.

2.2

Interpreting Random Variable Expressions As Computations

When random variables are regarded as free variables, arithmetic with randomvariables is no different from deterministic arithmetic. Measure-theoretic probability uses the same notation, but regards it as implicit pointwise lifting (as invector arithmetic). For example, if A, B and C are random variables, C = A + B
means C ω = (A ω) + (B ω), and B = 4 + A means B ω = 4 + (A ω).
Because we write all of our math in λZFC , we can extend the class of randomvariables from Ω → SX to Ω ⇒ SX . Including lambdas as well as mappings
makes it easy to interpret unnamed random variables: 4 + A, or (+ 4 A), means
λω. (+ 4 (A ω)). Lifting constants allows us to interpret expressions uniformly:
if we interpret + as Plus = λω.+ and 4 as Four = λω.4, then (+ 4 A) means
λω. ((Plus ω) (Four ω) (A ω))(3)

We abstract lifting and application with the combinators
pure c = λω.c∗

ap F X1 . . . Xn = λω. ((F ω) (X1 ω) . . . (Xn ω))(4)so that (+ 4 A) means ap ∗ (pure +) (pure 4) A = · · · = λω. (+ 4 (A ω)).
These combinators define an idiom [13], which is like a monad but can impose
a partial order on computations. Our random variable idiom instantiates theenvironment idiom with the type constructor (I a) = (Ω ⇒ a) for some Ω.
RJ·K (Fig. 1), the semantic function that interprets random variable expressions, targets this idiom. It does mechanically what we have done manually, andadditionally interprets lambdas. For simplicity, it follows probability convention
by assuming single uppercase letters are random variables. Fig. 1 assumes syntactic sugar has been replaced; e.g. that application is in prefix form.
RJ·K may return lambdas that do not converge when applied. These lambdas
do not represent random variables, which are total. We will be able to recover
mappings by restricting them, as in RJ(+ 4 A)K Ω .
2.3

Implementation in Racket

Figure 2 shows RV and a snippet of RV/kernel, the macros that implement RJ·K.
RV fully expands expressions into Racket’s kernel language, allowing RV/kernel to(define-syntax (RV/kernel stx)
(syntax-parse stx[( Xs:ids e:expr)(syntax-parse #’e #:literal−sets (kernel-literals)[X:id #:when (free-id-in? #’Xs #’X) #’X]
[x:id#’(pure x)][(quote c)#’(pure (quote c))][(%#plain-app e ...) #’(ap∗ (RV/kernel Xs e) ...)]....)]))(define-syntax (RV stx)
(syntax-parse stx[( Xs:ids e:expr)#‘(RV/kernel Xs #,(local-expand #’e ’expression empty))]))

Fig. 2. A well-embedded implementation of RJ·K.

transform any pure Racket expression into a random variable. Both use Racket’s
new syntax-parse library [2]. RV/kernel raises a syntax error on set!, but there
is no way to disallow applying functions that have effects.
Rather than differentiate between kinds of identifiers, RV takes a list of known
random variable identifiers as an additional argument. It wraps other identifierswith pure, allowing arbitrary Racket values to be random variables.

3

The Query Language

It is best to regard statements in Bayesian notation as specifications for the
results of later observations. We therefore interpret queries before interpretingstatements. First, however, we must define the state objects that queries observe.
3.1

Background Theory: Probability Spaces

In practice, functions called distributions assign probabilities or probability
densities to observable outcomes. Practitioners state distributions for certain
random variables, and then calculate the distributions of others.
Measure-theoretic probability generalizes assigning probabilities and densities using probability measures, which assign probabilities to sets of outcomes.
There are typically no special random variables: all random variable distributions
are calculated from one global probability measure.
It is generally not possible to assign meaningful probabilities to all subsets ofa sample space Ω—except when Ω is countable. We thus deal here with discrete
probability measures P : P(Ω) → [0, 1]. Any discrete probability measure isuniquely determined by its value on singleton sets, or by a probability massfunction P : Ω → [0, 1]. It is easy to convert P to a probability measure:X
sum P A =
P ω
(5)
ω∈A

Then P = sum P . Converting the other direction is also easy: P e = P {e}.
A discrete probability space (Ω, P ) embodies all probabilistic nondeterminism introduced by statements. It is fine to think of Ω as the set of all possible
states of a write-once memory, with P assigning a probability to each state.
3.2

Background Theory: Queries

Any probability can be calculated from (Ω, P ). For example, suppose we wantto calculate, as in Example 1, the probability of an even die outcome. We must
apply P to the correct subset of Ω. Suppose that Ω = {1, 2, 3, 4, 5, 6} and thatP = [1, 2, 3, 4, 5, 6 → 16 ] determines P. The probability that E outputs even is
P {ω ∈ Ω | E ω = even} = P {2, 4, 6} = sum P {2, 4, 6} =

1
2

(6)

This is a probability query.
Alternatively, we could use a distribution query to calculate E’s distribution PE , and then apply it to {even}. Measure-theoretic probability elegantly
defines PE as P ◦ E −1 , but for now we do not need ameasure. We only need theprobability mass function PE e = sum P E −1 {e} . Applying it yields
PE even = sum P E −1 {even} = sum P {2, 4, 6} = 12(7)More abstractly, we can calculate discrete distribution queries using
−1dist X (Ω, P ) = λ(x ∈ SX ).sum P X Ω {x}(8)where SX = image X Ω. Recall that X Ω converts X, which may be a lambda,
to a mapping with domain Ω, on which preimages are well-defined.
3.3

Interpreting Query Notation

When random variables are regarded as free variables, special notation P[·] replaces applying P and sets become propositions. For example, a common way towrite “the probability of an even die outcome” in practice is P[E = even].
The semantic function RJ·K turns propositions about random variables into
predicates on Ω. The set corresponding to the proposition is the preimage of−1{true}. For E = even, for example, it is RJE = evenK Ω {true}. In general,
−1
sum P RJeK Ω {true} = dist RJeK (Ω, P ) true
(9)
calculates P[e] when e is a proposition; i.e. when RJeK : Ω ⇒ {true, false}.
Although probability queries have common notation, there seems to be nocommon notation that denotes distributions per se. The typical workarounds
are to write implicit formulas like P[E = e] and to give distributions suggestive
names like PE . Some theorists use L[·], with L for law, an obscure synonym of
distribution. We define DJ·K in place of L[·]. Then DJEK denotes E’s distribution.
Though we could define semantic functions PJ·K and DJ·K right now, we are
putting them off until after interpreting statements.

(struct mapping (domain proc)#:property prop:procedure (λ (f x) ((mapping-proc f) x)))(struct fmapping (default hash)#:property prop:procedure(λ (f x) (hash-ref (fmapping-hash f) x (fmapping-default f))))(define appx-z (make-parameter +inf.0))(define (finitize ps)(match-let∗ ([(mapping Ω P) ps][Ωn (cotake Ω (appx-z))][qn (apply + (map P Ωn))])(mapping Ωn (λ (ω) (/ (P ω) qn)))))(define ((dist X) ps)(match-define (mapping Ω P) ps)(fmapping 0 (for/fold ([h (hash)]) ([ω (in-list Ω)])
(hash-set h (X ω) (+ (P ω) (hash-ref h (X ω) 0))))))

Fig. 3. Implementation of finite approximation and distribution queries in Racket.

3.4

Approximating Queries

Probabilities are real numbers. They remain real in the approximating semantics;
we use floating-point approximation and exact rationals in the implementation.
Arbitrary countable sets are not finitely representable. In the approximating
semantics, we restrict Ω to recursively enumerable sets. The implementation
encodes them as lazy lists. We trust users to not create “sets” with duplicates.
When A is infinite, sum P A is an infinite series. With A as a lazy list, it iseasy to compute a converging approximation—but then approximate answers to
distribution queries sum to values less than 1. Instead, we approximate Ω andnormalize P , which makes the sum finite and the distributions proper.
Suppose (ω1 , ω2 , . . .) is an enumeration of Ω. Let z ∈ N be the length of theprefix Ωz = {ω1 , . . . , ωz } and let Pz ω = (P ω)/(sum P Ωz ). Then Pz converges
to P . We define finitize (Ω, P ) = (Ωz , Pz ) with z ∈ N as a free variable.
3.5

Implementation in Racket

Fig. 3 shows the implementations of finitize and dist in Racket. The free variable z appears as a parameter appx-z: a variable with static scope but dynamic
extent. The cotake procedure returns the prefix of a lazy list as a finite list.
To implement dist, we need to represent mappings in Racket. The applicablestruct type mapping represents lazy mappings with possibly infinite domains. A
mapping named f can be applied with (f x). We do not ensure x is in the domain
because checking is semidecidable and nontermination is a terrible error message.
For distributions, checking is not important; the observable domain is.

However, we do not want dist to return lazy mappings. Doing so is inefficient:
every application of the mapping would filter Ω. Further, dist always receives
a finitized probability space. We therefore define fmapping for mappings thatare constant on all but a finite set. For these values, dist builds a hash table bycomputing the probabilities of all preimages in one pass through Ω.
We do use mapping, but only for probability spaces and stated distributions.

4

Conditional Queries

For Bayesian practitioners, the most meaningful queries are conditional queries:
those conditioned on, or given, some random variable’s value. (For example, theprobability an email is spam given it contains words like “madam,” or the distribution over suspects given security footage.) A language without conditional
queries is of little more use to them than a general-purpose language.
Measure-theoretic conditional probability is too involved to accurately summarize here. When P is discrete, however, the conditional probability of set A
given set B (i.e. asserting that ω ∈ B), simplifies to
P[A | B] = (P A ∩ B)/(P B)(10)

In theory and practice, P[ · | · ] is special notation. As with P[·], practitioners
apply it to propositions. They define it with P[eA | eB ] = P[eA ∧ eB ]/P[eB ].
Example 2. Extend Example 1 with random variable L ω = low if ω ≤ 3, else
high. The probability that E = even given L = low isPP ω1
P[E = even ∧ L = low]ω∈{2}P
= 61 = 31 (11)=P[E = even | L = low] =P ωP[L = low]2ω∈{1,2,3}

Less precisely, there are proportionally fewer even outcomes when L = low.

tuConditional distribution queries ask how one random variable’s output influences the distribution of another. As with unconditional distribution queries,
practitioners work around a lack of common notation. For example, they might
write the distribution of E given L as P[E = e | L = l] or PE|L .
It is tempting to define PJ · | · K in terms of PJ·K (and DJ · | · K in terms of DJ·K).
However, defining conditioning as an operation on probability spaces insteadof on queries is more flexible, and it better matches the unsimplified measure
theory. The following abstraction returns a discrete probability space in whichΩ is restricted to the subset where random variable Y returns y:−1cond Y y (Ω, P ) = (Ω 0 , P 0 ) where Ω 0 = Y Ω {y}P 0 = λ(ω ∈ Ω 0 ).(P ω)/(sum P Ω 0 )(12)Then P[E = even | L = low] means dist E (cond L low (Ω, P )) even.
We approximate cond by applying finitize to the probability space. Its
implementation uses finite list procedures instead of set operators.

5

The Statement Language

Random variables influence each other through global probability spaces. However, because practitioners regard random variables as free variables instead of asfunctions of a probability space, they state facts about random variable distributions instead of facts about probability spaces. Though they call such collectionsof statements models,1 to us they are probabilistic theories. A model is a
probability space and random variables that imply the stated facts.
Discrete conditional theories can always be written to conform toti ::= Xi ∼ ei ; ti+1 | Xi := ei ; ti+1 | ea = eb ; ti+1 | (13)Further, they can always be made well-formed : an ej may refer to some Xi
only when j > i (i.e. no circular bindings). We start by interpreting the mostcommon kind of Bayesian theories, which contain only distribution statements.
5.1

Interpreting Common Conditional Theories

Example 3. Suppose we want to know only whether a die outcome is even or odd,
high or low. If L’s distribution is PL = [low , high 7→ 21 ], then E’s distribution
depends on L’s output.
Define PE|L : SL → SE → [0, 1] by PE|L low = [even 7→ 13 , odd 7→ 23 ] and
PE|L high = [even 7→ 23 , odd 7→ 31 ].2 The conditional theory could be writtenL ∼ PL ; E ∼ PE|L L(14)
If L is a measure-theoretic random variable, PE|L L does not type-check:L : Ω → SL is clearly not in SL . The intent is that E’s distribution depends on
L, and that PE|L specifies how.
tu
We can regard L ∼ PL as a constraint:
for every model (Ω, P, L), dist L (Ω, P )must be PL . Similarly, E ∼ PE|L L means E’s conditional distribution is PE|L .
We have been using the model Ω = {1, 2, 3, 4, 5, 6}, P =[1, 2, 3, 4, 5, 6 7→ 61 ], andthe obvious E and L. It is not hard to verify that this is also a model:Ω = {low , high} × {even, odd }L ω = ω1E ω = ω2

P = [(low , even) , (high, odd ) 7→ 61 , (low , odd ) , (high, even) 7→ 62 ](15)

The construction of Ω, L and E in (15) clearly generalizes, but P is trickier.
Fully justifying the generalization (including that it meets implicit independence
assumptions that we have not mentioned) is rather tedious, so we do not do it
here. But, for the present example, it is not hard to check these facts:P ω = (PL (L ω)) × PE|L (L ω) (E ω)
q
 y
(16)
or P = R (PL L) × PE|L L E
1
2

In the colloquial sense, probably to emphasize their essential incompleteness.
Usually, PE|L : SE × SL → [0, 1]. We reorder and curry to simplify interpretation.

dist ps X (Ω, P ) = (Ω, P, PX ) where SX = image X Ω
PX = λ(x ∈ SX ).sum P
˛−1` 0 0 ´where Ω 0 = Y ˛Ω {y}cond ps Y y (Ω, P ) = Ω , P ,

“ ˛
”
−1
X ˛Ω {x}`´
P 0 = λ(ω ∈ Ω 0 ).(P ω)/ sum P Ω 0extend ps Ki (Ωi−1 , Pi−1 ) = (Ωi , Pi , Xi )where Si0 ω = domain (Ki ω),`´Ωi = (ω ∈ Ωi−1 ) × Si0 ω

Xi ω = ωj (where j = length of any ω ∈ Ωi−1 ),`´
run ps m = x where (Ω, P, x) = m {()}, λω.1

Pi = RJPi−1 × (Ki Xi )K

Fig. 4. State monad functions that represent queries and statements. The state isprobability-space-valued.

qy
If KL = RJPL K and KE = R PE|L L —which interpret (14)’s statements’right-hand sides—then P = RJ(KL L) × (KE E)K. This can be generalized.
Definition 1 (discrete product model). Given a well-formed, discrete conditional theory X1 ∼ e1 ; . . . ; Xn ∼ en , let Ki : Ω ⇒ Si → [0, 1], Ki = RJei K foreach 1 ≤ i ≤ n. The discrete product model of the theory is
t n
|
n
Y
Ω=
Si
Xi ω = ωi (1 ≤ i ≤ n)
P =R
(Ki Xi )
(17)

×
i=1

i=1

Theorem 1 (semantic intent). The discrete product model induces the statedconditional distributions and meets implicit independence assumptions.
When writing distribution statements, practitioners tend to apply first-order
distributions to simple random variables. But the discrete product model allows
any λZFC term ei whose interpretation is a discrete transition kernel RJei K :Ω ⇒ Si → [0, 1]. In measure theory, transition kernels are used to build productspaces such as (Ω, P ). Thus, RJ·K links Bayesian practice to measure theory andrepresents an increase in expressive power in specifying distributions, by turning
properly typed λZFC terms into precisely what measure theory requires.
5.2

Interpreting Statements as Monadic Computations

Some conditional theories state more than just distributions [12, 21]. Interpretingtheories with different kinds of statements requires recursive, rather than wholetheory, interpretation. Fortunately, well-formedness amounts to lexical scope,making it straightforward to interpret statements as monadic computations. We
use the state monad with probability-space-valued state.
We assume the state monad’s return s and bind s . Fig. 4 shows the additional
dist ps , cond ps and extend ps . The first two simply reimplement dist and cond .
But extend ps , which interprets statements, needs more explanation.

MJXi := ei ; ti+1 K = bind s (return s RJei K) λXi .MJti+1 K

MJXi ∼ ei ; ti+1 K = bind s (extend ps RJei K) λXi .MJti+1 K

MJea = eb ; ti+1 K = bind s (cond ps RJea K RJeb K) λ .MJti+1 K

MJK = return s (X1 , . . . , Xn )`´
DJeK m = run ps bind s m λ(X1 , . . . , Xn ).dist ps RJeK`´DJeX | eY K m = λy.DJeX K bind s m λ(X1 , . . . , Xn ).MJeY = yK
PJeK m = DJeK m true,

PJeA | eB K m = DJeA | eB K m true true

Fig. 5. The conditional theory and query semantic functions.

According to (17), interpreting Xi ∼ ei results in Ωi = Ωi−1 × Si , with Si
extracted from Ki : Ωi−1 ⇒ Si → [0, 1]. A more precise type for Ki is thedependent type (ω : Ωi−1 ) ⇒ (Si0 ω) → [0, 1], which reveals a complication. To
extract Si , we first must extract theSrandom variable Si0 : Ωi−1 → P(Si ). So let
Si0 ω = domain (Ki ω); then Si = (image Si0 Ωi−1 ).
But this makes query implementation inefficient: if the union has little overlap
or is disjoint, P will assign 0 to most ω. In more general terms, we actually havea dependent cartesian product (ω ∈ Ωi−1 ) × (Si0 ω), a generalization of thecartesian product.3 To extend Ω, extend ps calculates this product instead.
Dependent cartesian products are elegantly expressed using the set monad:[
return v x = {x}bind v m f =(image f m)
(18)
Then (a ∈ A) × (B a) = bind v A λa.bind v (B a) λb.return v (a, b).
Fig. 5 defines MJ·K, which interprets conditional theories containing definition, distribution, and conditioning statements as probability space monadcomputations. After it exhausts the statements, it returns the random variables.
Returning their names as well would be an obfuscating complication, which we
avoid by implicitly extracting them from the theory before interpretation. (However, the implementation explicitly extracts and returns names.)
DJeK expands to a distribution-valued computation
and runs it with theempty probability space (Ω0 , P0 ) = {()}, λω.1 . DJeX | eY K conditions theprobability space and hands off to DJeX K. PJ·K is defined in terms of DJ·K.
5.3

Approximating Models and Queries

We compute dependent cartesian products of sets represented by lazy lists in away similar to enumerating N × N. (It cannot be done with a monad as in theexact semantics, but we do not need it to.) The approximating versions of dist ps
and cond ps apply finitize to the probability space.
3

The dependent cartesian product also generalizes disjoint union to arbitrary index
sets. It is often called a dependent sum and denoted Σa : A.(B a).

5.4

Implementation in Racket

MJ·K’s implementation is MDL. Like RV, it passes random variable identifiers, but
it accumulates them. For example, (MDL [] ([X ∼ Px])) expands to([X] (bind/s (extend/ps (RV [] Px)) (λ (X) (ret/s (list X)))))

where [X] is the updated list of identifiers and the rest is a model computation.
We store theories in transformer bindings so queries can expand them later.
For example, (define-model die-roll [L ∼ Pl] [E ∼ (Pe/l L)]) expands to(define-syntax die-roll #’(MDL [] ([L ∼ Pl] [E ∼ (Pe/l L)])))The macro with-model introduces a scope in which a theory’s variables are visible.
For example, (with-model die-roll (Dist L E)) looks up die-roll and expands
it into its identifiers and computation. Using the identifiers as lambda arguments,
Dist (the implementation of DJ·K) builds a query computation as in Fig. 5, andruns it with (mapping (list empty) (λ (ω) 1)), the empty probability space.
Using these identifiers would break hygiene, except that Dist replaces thelambda arguments’ lexical context. This puts the theory’s exported identifiers inscope, even when the theory and query are defined in separate modules. Because
queries can access only the exported identifiers, it is safe.
Aside from passing identifiers and monkeying with hygiene, the macros arealmost transcribed from the semantic functions.
Examples. Consider a conditional distribution with the first-order definition(define (Geometric p)(mapping N1 (λ (n) (∗ p (expt (- 1 p) (- n 1))))))

where N1 is a lazy list of natural numbers starting at 1. Nahin gives a delightfully
morbid use for Geometric in his book of probability puzzlers [15].
Two idiots duel with one gun. They put only one bullet in it, and take turns
spinning the chamber and firing at each other. They know that if they each takeone shot at a time, player one usually wins. Therefore, player one takes one shot,
and after that, the next player takes one more shot than the previous player,
spinning the chamber before each shot. How probable is player two’s demise?
The distribution over the number of shots when the gun fires is (Geometric1/6). Using this procedure to determine whether player one fires shot n:(define (p1-fires? n [shots 1])(cond [(n . <= . 0) #f][else (not (p1-fires? (- n shots) (add1 shots)))]))

we compute the probability that player one wins with
(with-model (model [winning-shot ∼ (Geometric 1/6)])(Pr (p1-fires? winning-shot)))

Nahin computes 0.5239191275550995247919843—25 decimal digits—with custom MATLAB code. At appx-z ≥ 321, our solution computes the same digits.
(Though it appends the digits 9..., so Nahin should have rounded up!) Implementing it took about five minutes. But the problem is not Bayesian.

This is: suppose player one slyly suggests a single coin flip to determine
whether they spin the chamber before each shot. You do not see the duel, butlearn that player two won. What is the probability they spun the chamber?
Suppose that the well-known Bernoulli and discrete Uniform conditional
distributions are defined. Using these first-order conditional distributions andRacket’s cond, we can state a fairly direct theory of the duel:(define-model half-idiot-duel[spin? ∼ (Bernoulli 1/2)][winning-shot ∼ (cond [spin?
[else(Geometric 1/6)](Uniform 1 6)])])

Then (Pr spin? (not (p1-fires? winning-shot))) converges to about 0.588.
Bayesian practitioners would normally create a new first-order conditional
distribution WinningShot, and then state [winning-shot ∼ (WinningShot spin?)].
Most would like to state something more direct—such as the above theory, whichplainly shows how spin?’s value affects winning-shot’s distribution. However,
without a semantics, they cannot be sure that using the value of a cond (or ofany “if”-like expression) as a distribution is well-defined. That winning-shot has
a different range for each value of spin? makes things more uncertain.
As specified by RJ·K, our implementation interprets (cond ...) above as astochastic transition kernel. As specified by MJ·K, it builds the probability space
using dependent cartesian products. Thus, the direct theory really is well-defined.
The most direct theory has infinitely many statements, one for each possible
shot. Supporting such theories is future work.

6

Why Separate Statements and Queries?

Whether queries should be allowed inside theories is a decision with subtle effects.
Theories are sets of facts. Well-formedness imposes a partial order, but every
linearization should be interpreted equivalently. Thus, we can determine whether
two kinds of statements can coexist in theories by determining whether they
can be exchanged without changing the interpretation. This is equivalent todetermining whether the corresponding monad functions commute.
The following definitions suppose a conditional theory t1 ; . . . ; tn in which
exchanging some ti and ti+1 (where i < n) is well-formed. Applying semantic
functions in the definitions yields definitions that are independent of syntax but
difficult to read, so we give the syntactic versions.
Definition 2 (commutativity). We say that ti and ti+1 commute when
MJt1 ; . . . ; ti ; ti+1 ; . . . ; tn K (Ω0 , P0 ) = MJt1 ; . . . ; ti+1 ; ti ; . . . ; tn K (Ω0 , P0 ).

This notion of commutativity is too strong: distribution statements would
never commute with each other. We need a weaker test than equality.

Definition 3 (equivalence in distribution). Suppose X1 , . . . , Xk are definedin t1 , . . . , tn . Let m = MJt1 , . . . , tn K, and m0 be a (usually different) probability
space monad computation. We write m ≡D m0 and call m and m0 equivalent
in distribution when DJX1 , . . . , Xk K m = DJX1 , . . . , Xk K m0 .

The following says ≡D is like observational equivalence with query contexts:
Theorem 2 (context). DJeX | eY K m = DJeX | eY K m0 for all random variables RJeX K and RJeY K if and only if m ≡D m0 .
Definition 4 (commutativity in distribution). We say ti and ti+1 commutein distribution when MJt1 ; . . . ; ti ; ti+1 ; . . . ; tn K ≡D MJt1 ; . . . ; ti+1 ; ti ; . . . ; tn K.
Theorem 3. The following table summarizes commutativity of condps , distps
and extendps in the probability space monad:
condpsextendps
distps

=
=
≡D
6 D
≡
=
=
condps extendps distps

By Thm. 3, if we are to maintain the idea that theories are sets of facts, wecannot allow both conditioning and query statements.

7

Related Work

Our approach to semantics is similar to abstract interpretation: we have a concrete (exact) semantics and a family of abstractions parameterized by z (approximating semantics). We have not framed our approach this way because
our approximations are not conservative, and would be difficult to formulate as
abstractions when parameterized on a random source (which we intend to do).
Bayesian practitioners occasionally create languages for modeling and queries.
Analyzing their properties is usually difficult, as they tend to be defined by implementations. Almost all of them compute converging approximations and supportconditional queries. When they work as expected, they are useful.
Koller and Pfeffer [9] efficiently compute exact distributions for the outputs ofprograms in a Scheme-like language. BUGS [11] focuses on efficient approximate
computation for probabilistic theories with a finitely many statements, with
distributions that practitioners typically use. BLOG [14] exists specifically toallow stating distributions over countably infinite vectors. BLAISE [1] allows
stating both distribution and approximation method for each random variable.
Church [4] is a Scheme-like probabilistic language with approximate inference,and focuses on expressiveness.
Kiselyov [8] embeds a probabilistic language in O’Caml for efficient computation. It uses continuations to enumerate or sample random variable values,and has a fail construct for the complement of conditioning. The sampler looks
ahead for fail and can handle it efficiently. This may be justified by commutativity (Thm. 3), depending on interaction with other language features.
There is a fair amount of semantics work in probabilistic languages. Most of
it is not motivated by Bayesian concerns, and thus does not define conditioning.
Kozen [10] defines the meaning of bounded-space, imperative “while” programs
as functions from probability measures to probability measures. Hurd [6] provesproperties about programs with binary random choice by encoding programs
and portions of measure theory in HOL.
Jones [7] develops a domain-theoretic variation of probability theory, andwith it defines the probability monad, whose discrete version is a distributionvalued variation of the set or list monad. Ramsey and Pfeffer [20] define theprobability monad measure-theoretically and implement a language for finite
probability. We do not build on this work because the probability monad does
not build a probability space, making it difficult to reason about conditioning.
Pfeffer also develops IBAL [19], apparently the only lambda calculus withfinite probabilistic choice that also defines conditional queries. Park [16] extends
a lambda calculus with probabilistic choice, defining it for a very general classof probability measures using inverse transform sampling.

8

Conclusions and Future WorkFor discrete Bayesian theories, we explained a large subclass of notation as
measure-theoretic calculations by transformation into λZFC . There is now atleast one precisely defined set of expressions that denote discrete conditional
distributions in conditional theories, and it is very large and expressive. We gavea converging approximating semantics and implemented it in Racket.
Now that we are satisfied that our approach works, we turn our attention to
uncountable sample spaces and theories with infinitely many statements.
Following measure-theoretic structure in our preliminary work should makethe transition to uncountable spaces fairly smooth. The functional structure of
the exact semantics will not change, but some details will. The random variableidiom will be identical, but will require measurability proofs. We will still interpret statements as state monad computations, but with general probability
spaces as state instead of discrete probability spaces. We will use regular conditional probability in cond ps , extend ps will calculate product σ-algebras andtransition kernel products, and dist ps will return probability measures. We will
not need to change RJ·K, DJ·K or PJ·K. Many approximations are available; themost efficient and general are sampling methods. We will likely choose sampling
methods that parallelize easily.
The most general constructive way to specify theories with infinitely many
primitive random variables is with recursive abstractions, but it is not clear
what kind of abstraction we need. Lambdas are suitable for most functional
programming, in which it is usually good that intermediate values are unobservable. However, they do not meet Bayesian needs: practitioners define theories
to study them, not to obtain single answers. If lambdas were the only abstraction, returning every intermediate value from every lambda would become goodpractice. Because we do not know what form abstraction will take, we will likely
develop it independently by allowing theories with infinitely many statements.
Model equivalence in distribution extends readily to uncountable spaces. It
defines a standard for measure-theoretic optimizations, which can only be donein the exact semantics. Examples are variable collapse, a probabilistic analogue

of constant folding that can increase efficiency by an order of magnitude, and aprobabilistic analogue of constraint propagation to speed up conditional queries.

References
1. Bonawitz, K.A.: Composable Probabilistic Inference with Blaise. Ph.D. thesis,
Massachusetts Institute of Technology (2008)
2. Culpepper, R.: Refining Syntactic Sugar: Tools for Supporting Macro Development.
Ph.D. thesis, Northeastern University (2010), to Appear
3. Flatt, M., PLT: Reference: Racket. Tech. Rep. PLT-TR-2010-1, PLT Inc. (2010),
http://racket-lang.org/tr1/
4. Goodman, N., Mansinghka, V., Roy, D., Bonawitz, K., Tenenbaum, J.: Church: alanguage for generative models. In: Uncertainty in Artificial Intelligence (2008)
5. Gordon, M.: Higher order logic, set theory or both? (1996), invited talk, TPHOLs,
Turku, Finland
6. Hurd, J.: Formal Verification of Probabilistic Algorithms. Ph.D. thesis, Universityof Cambridge (2002)
7. Jones, C.: Probabilistic Non-Determinism. Ph.D. thesis, University of Edinburgh(1990)
8. Kiselyov, O., Shan, C.: Monolingual probabilistic programming using generalizedcoroutines. In: Uncertainty in Artificial Intelligence (2008)
9. Koller, D., McAllester, D., Pfeffer, A.: Effective Bayesian inference for stochastic
programs. In: 14th National Conference on Artificial Intelligence (August 1997)
10. Kozen, D.: Semantics of probabilistic programs. In: Foundations of Computer Science (1979)
11. Lunn, D.J., Thomas, A., Best, N., Spiegelhalter, D.: WinBUGS – a Bayesian modelling framework. Statistics and Computing 10(4) (2000)
12. Mateescu, R., Dechter, R.: Mixed deterministic and probabilistic networks. Annalsof Mathematics and Artificial Intelligence (2008)
13. McBride, C., Paterson, R.: Applicative programming with effects. Journal of Functional Programming 18(1) (2008)
14. Milch, B., Marthi, B., Russell, S., Sontag, D., Ong, D., Kolobov, A.: BLOG: Probabilistic models with unknown objects. In: International Joint Conference on Artificial Intelligence (2005)
15. Nahin, P.J.: Duelling Idiots and Other Probability Puzzlers. Princeton University
Press (2000)
16. Park, S., Pfenning, F., Thrun, S.: A probabilistic language based upon sampling
functions. Transactions on Programming Languages and Systems 31(1) (2008)
17. Paulson, L.C.: Set theory for verification: I. From foundations to functions. Journalof Automated Reasoning 11, 353–389 (1993)
18. Paulson, L.C.: Set theory for verification: II. Induction and recursion. Journal ofAutomated Reasoning 15, 167–215 (1995)
19. Pfeffer, A.: The design and implementation of IBAL: A general-purpose probabilistic language. In: Statistical Relational Learning. MIT Press (2007)
20. Ramsey, N., Pfeffer, A.: Stochastic lambda calculus and monads of probability
distributions. In: Principles of Programming Languages (2002)
21. Toronto, N., Morse, B.S., Seppi, K., Ventura, D.: Super-resolution via recapture
and Bayesian effect modeling. In: Computer Vision and Pattern Recognition (2009)