Computer Science and Artificial Intelligence Laboratory
Technical Report
MIT-CSAIL-TR-2008-025

May 3, 2008

Random-World Semantics and Syntactic
Independence for Expressive Languages
David McAllester, Brian Milch, and Noah D. Goodman

m a ss a c h u se t t s i n st i t u t e o f t e c h n o l o g y, c a m b ri d g e , m a 02139 u s a — w w w. c s a il . mi t . e d uRandom-World Semantics and Syntactic Independence for Expressive Languages
David McAllester

Brian Milch

Noah D. Goodman

Toyota Technological Institute at Chicago
Chicago, IL 60637
mcallester@tti-c.org

MIT CSAIL
Cambridge, MA 02139
milch@csail.mit.edu

MIT Brain and Cognitive Sciences
Cambridge, MA 02139
ndg@mit.edu

Abstract

First we consider expressivity. We are not satisfied with alanguage merely as expressive as first order logic. We would
like to be able to express, for instance, the notion of reachability — the notion that one given state is reachable fromanother using given operations. A simple consequence ofthe compactness theorem is that reachability is not definablein first order logic. More generally, first order logic does
not support recursive definitions. Also, even in highly expressive first-order probabilistic languages such as Bayesian
logic (Milch et al. 2005), there is no straightforward way todefine new procedures and use them in several places in amodel, or to define distributions over structured data types
such as lists or graphs.
To gain sufficient expressivity we turn to functional programming languages, which support recursive definitions aswell as a rich ontology of structured data types. We consider languages where the logical formulas are taken to be
the Boolean expressions of a programming language, possibly extended with additional forms of quantification. The
use of programming languages as a foundation for logicalreasoning has a long tradition in the formal methods community (Kaufmann, Manolios, & Moore 2000; Gordon &Melham 1993; Bertot & Castran 2004). The syntactic independence criterion developed here is independent of theparticular choice of programming language.
Next we consider various forms of probabilistic semantics. A common way of combining probability with programming is to introduce a random number generator. We
can introduce the expression rand() into the language,
and define the language’s semantics in terms of a random(stochastic) evaluation process. This is analogous to the useof the standard random number generator in C: each timethe evaluator evaluates the expression rand() it generates a
new random number. Random-evaluation semantics is usedin Avi Pfeffer’s modeling and inference system IBAL (Pfeffer 2001), as well as a number of other probabilistic programming languages (Koller, McAllester, & Pfeffer 1997;
Ramsey & Pfeffer 2002; Park, Pfenning, & Thrun 2005).
Random-evaluation semantics is not a random-world semantics. Consider a logical formula of the form Φ ∧ ¬Φ.
Under any random-world semantics this logical formula will
have probability zero, as we show below. But under randomevaluation semantics, the two occurrences of the formula Φ
can have different values in a single evaluation, since differ-

We consider three desiderata for a language combining logic
and probability: logical expressivity, random-world semantics, and the existence of a useful syntactic condition for probabilistic independence. Achieving these three desiderata simultaneously is nontrivial. Expressivity can be achieved byusing a formalism similar to a programming language, butstandard approaches to combining programming languages
with probabilities sacrifice random-world semantics. Naive
approaches to restoring random-world semantics undermine
syntactic independence criteria. Our main result is a syntactic
independence criterion that holds for a broad class of highly
expressive logics under random-world semantics. We explore
various examples including Bayesian networks, probabilistic
context-free grammars, and an example from Mendelian genetics. Our independence criterion supports a case-factor inference technique that reproduces both variable eliminationfor BNs and the inside algorithm for PCFGs.

Introduction
We are interested in the combination of logic and probability. In particular we consider the following three desiderata
for formal languages which simultaneously have both a logical and a probabilistic semantics.
1. The logical formulas should be expressive. They should
support a rich ontology of types such as lists and graphs
and should support function composition and recursive
definitions.
2. The language should have a random-world semantics.
The semantics should be defined by a probability distribution (or measure) on a set of worlds where each logicalformula is either true or false in each world, according to
the semantics of the underlying logic.
3. The language should have a useful syntactic criteria forprobabilistic independence.
Our main technical result is the validity of a set of inference
rules for a broad class of expressive probabilistic languages.
One of these rules, a consequence of random-world semantics, guarantees that logically equivalent formulas have thesame probability. Another is a syntactic criteria for probabilistic independence which allows the program structure to
be exploited for inference. Before presenting the main result, however, we elaborate on each of the above desiderata.
1

ent random choice can be made in a second evaluation of Φ.
So the formula Φ∧¬Φ can evaluate to true. A related consequence of the lack of random-world semantics is that if one
wants to reason about a random function — say, a function
color mapping balls to colors — one cannot simply use afunction in the programming language. Calling color on
the same ball multiple times would yield different values. To
create a random mapping in a random-evaluation language,
one must explicitly construct a data structure, such as a listof ball–color pairs.
Next we consider memoization semantics, in which one
passes a “name” argument (perhaps an integer or a character
string) to the random number generator; we write rand(n)where n is a name for the random number. Later calls to
the random number generator with the same name return thesame number. Memoization guarantees that the same expression evaluates to the same value when it is evaluated asecond time. We then get that Φ ∧ ¬Φ must evaluate tofalse. Under memoization semantics we can think of the“world” as being a mapping from names to numbers — aworld picks a single random number for each name. Thisis the approach taken in probabilistic Horn abduction (Poole
1993) and PRISM (Sato & Kameya 2001).
The difficulty with memoization semantics involves thedesire for syntactic criterion for independence. Under memoization semantics each expression of the form rand(n)can be viewed as an independent random variable — wehave one random variable for each name n. Two logical formulas are independent if they involve disjoint sets of randomvariables; the problem is that it can be difficult to syntactically determine what random variables influence the valueof a given formula. This follows because procedures cancreate names for random variables in arbitrary ways.
Finally we consider a new form of semantics we callnumber-tree semantics. As in memoization semantics, we
add an argument to the random number generator. We still
write rand(t), but now t is a conceptual data structure
called a number tree. A number tree is an infinitely deep,
infinitely branching tree in which every node is labeled witha real number in the interval [0, 1]. A number tree is a sourceof random numbers and rand(t) simply denotes the number at the root of t. We will show that by working with variables ranging over number trees, it is possible to formulate
a syntactic independence criterion. Number-tree semantics
satisfies all three of the stated desiderata.

define cloudy(t)fc (t.cloudy)
define fc (t)rand(t) < 0.5
define rain(t)fr (cloudy(t),t.rain)
define fr (c,t)
if c then (rand(t) < 0.8)
else (rand(t) < 0.2)
define sprinkler(t)fs (cloudy(t),t.sprinkler)
define fs (c,t)
if c then (rand(t) < 0.1)
else (rand(t) < 0.5)
define wet(t)fw (rain(t),sprinkler(t),t.wet)define fw (r,s,t)
if r ∨ s then (rand(t) < 0.9)
else (rand(t) < 0.1)

Figure 1: Program for the sprinkler example.

Given the basic notion of a number tree, other details ofa particular programming language are fairly arbitrary —number-tree semantics can be used as an extension of any
functional programming language. We give a formal treatment for a particular family of languages below. Here we
present the ideas of number tree semantics and the desiderata through examples, with programming language features
introduced as they are used.
We begin with a simple Bayesian network — the classic“sprinkler” example. In this example, whether the grass is
wet (W ) depends on whether it has rained recently (R) andwhether the sprinkler has been on recently (S). The probabilities of R and S both depend on whether it is cloudy (C).
A program for this scenario is shown in Fig. 1. In the figure,the parameter t ranges over number trees and all procedures
return Boolean values. The procedures fc , fr , fs and fw implement conditional probability tables. Each such proceduretakes some number of parent values, plus a number tree containing “random” numbers, and returns the value of a node.
In a typed programming language one typically has expressions of type Boolean which we will call logical formulas. Let Φ be a logical formula in which the number tree variable t occurs as the only free variable. Given a value (a number tree) for the variable t, the formula Φ has a well-defined
truth value. We let Pt [Φ] be the probability that when t is
assigned to a random tree (with every number selected uniformly in [0, 1]) we have that Φ evaluates to true. Given thefunction definitions in Fig. 1, we can write expressions suchas Pt [wet(t)] for the probability that the grass is wet, orPt [sprinkler(t) ∧ wet(t)]/Pt [wet(t)] for the conditional probability that the sprinkler was on given that thegrass is wet.

Number-Tree Semantics
We define a number tree to be a tree each node of which islabeled with a real number in the interval [0, 1], and where
each node has a countably infinite number of children. The
children are indexed by character strings. If t is a number
tree and s is a character string, we write t.s to denote thesubtree of t reached by going down the branch named bys. The tree t.s is recursively a number tree. The expression
rand(t) denotes the number labeling the root of the number tree t. We will define a probabilistic semantics where
each number in a number tree is selected independently anduniformly from the interval [0, 1].
2

Inference Rules

Inference in Bayesian Networks

We now present a set of inference rules for a formalism combining logic and probability under number-tree semantics.
We begin with an inference rule for case analysis. To formulate this rule, it is convenient to define the set of feasible
values for an expression e. First, for any logical formula Φ
we define the formula ∃t [Φ] to be true if there exists a number tree such that Φ is true when the variable t is interpreted
as that tree. The feasible values for an expression e, denotedVt [e], can then be defined as follows (where v ranges overvalues specified by the specific language):
Vt [e] = {v : ∃t [e = v]}
We can express the operation of case anaylsis with the following equation.
X
Pt [Φ] =Pt (Φ ∧ e = v)
(1)

Here we show that the inference rules of the previous section
are sufficient for the analysis of Bayesian networks. We will
analyze the sprinkler example, the generalization to arbitrary
Bayesian networks is straightforward. Consider evaluating
the probability Pt [wet(t) = w]. By logical equivalence(2) we can replace each random variable (each node of the
network) by the appropriate call to a conditional probability
table procedure yielding:!
#"fr (fc (t.cloudy), t.rain),fs (fc (t.cloudy), t.sprinkler),
Pt fw
=w
t.wet
We can now do a case anlysis (1) on the unobserved nodes(all nodes other than the observed node wet(t)) yielding:!
fr (fc (t.cloudy), t.rain), fw
fs (fc (t.cloudy), t.sprinkler),
=w 


X
t.wet


Pt 

∧fr (fc (t.cloudy), t.rain) = r


r,s,c

 ∧fs (fc (t.cloudy), t.sprinkler) = s∧fc (t.cloudy), t.sprinkler) = cv∈Vt [e]In case analysis one reduces a probability to a sum of simpler
probabilities. The choice of the expression e on which to do
the case analysis is heuristic.
Logical inference can be used to rewrite logical expressions, replacing a logical formula by an equivalent simpler
one. In a random-world semantics these logical equivalencies are respected by the probabilistic aspect of the language.
This principle can be expressed as follows:
Pt [Φ] = Pt [Ψ] if ∀t [Φ ⇔ Ψ](2)
We now give a syntactic independence criterion that follows from the number-tree semantics. Define a subtree
expression to be an expression of the form t.c1 .c2 . . . cn
where each ci is a character string constant: for example,
t.left.right . Now consider two subtree expressions t.α
and t.β where α and β are each sequences of character string
constants. We say that t.α is syntactically independent oft.β provided that neither α nor β is a prefix of the other.
For example, t.left.right and t.left.left are syntactically independent but t.left.right and t.left arenot. Syntactically independent subtree expressions denotedisjoint substrees. The number labels in disjoint subtrees
are independent. Now consider two logical formulas Φ ad Ψ
and a number tree variable t.
Definition 1. Two formulas Φ and Ψ are syntactically independent with respect to number tree variable t if for every
pair of an occurrence of t in Φ and an occurrence of t in Ψ
we have that the occurrence of t in Φ occurs inside a subtree
expression t.α and the occurrence of t in Ψ occurs inside a
subtree expression t.β where t.α and t.β are syntacticallyindependent.
The main technical contribution of this paper is number
tree semantics and the observation that under number tree
semantics, the following factorization rule holds:
Pt [Φ ∧ Ψ] = Pt [Φ]Pt [Ψ] if Φ and Ψ are synt. ind. (3)Finally, we have the following contraction rule whereΦ[t.c] is a logical formula and t is a number tree varaible
such that every occurrence of t in Φ[t.c] occurs inside thesubtree expression t.c.
Pt [Φ[t.c]] = Pt [Φ[t]](4)

Now by logical equivalence (2) this is equivalent to:
fw (r, s, t.wet) = wX ∧fr (c, t.rain) = rPt ∧fs (c, t.sprinkler) = s r,s,c∧fc (t.cloudy) = s
Now by syntactic independence (3) we can factor this as:
P [f (r, s, t.wet) = w]
 t w
X 
Pt [fr (c, t.rain) = r]Pt [fs (c, t.sprinkler) = s]r,s,c Pt [fc (t.cloudy) = c]Finally, by contraction (4) this can be rewritten as:
P [f (r, s, t) = w]
 t w
X 
Pt [fr (c, t) = r]Pt [fs (c, t) = s]r,s,c Pt [fc (t) = c]
This is the standard sum of product expression for the probability of evidence in a Bayesian network. Standard algorithms can be used to evaluate this expression.

A Mendelian Genetics Model
Fig. 2 shows a program for Mendelian genetics. Each individual has a genotype, represented as a mapping from loci(places where genes are located) to pairs of alleles (versionsof a gene). The variable t ranges over number trees. In thisexample the programming language is taken to include data
structures build with data constructors where foo[x,y]denotes the a data structure with top level tag foo and which
includes the data structures x and y as parts. the expression
match(v, p, b1 , b2 ) matches the value v against the patternp and, if the match is successful, evaluate b1 under the variable bindings generated by the match, and other wise returns
the value of b2 . In this code data structures are sometimes
used rather than character strings to select a child of a given
3

define genotype(x, t)match(x, child[id, f, m],mate(genotype(f, t), genotype(m, t),t.conception[x]),genotypePrior(t.origin[x]))define CFTfrom(x, t)case ProdFrom(x, t.center) of
pair[y,z] :node[x, CFTfrom(y, t.left),
CFTfrom(z, t.right)]
terminal[a] : terminal[a]define mate(g1, g2, t)
hpair(meiosis(g1, t.left),meiosis(g2, t.right))

define CFT(t) CFTfrom(s[], t)define yield(z)case z ofnode[x, zleft, zright] :append(yield(zleft), yield(zright))
terminal[a] : list(a)define meiosis(g, t)
lambda loc
match(g(loc), pair[a, b](if rand(t.loc) < 0.5 then a else b),
error[])

define CFstring(t) yield(CFT(t))

define hpair(f,g)
lambda x
pair[f(x),g(x)]Figure 3: Program that uses a PCFG to define a distribution
over trees.
Figure 2: Program for Mendelian genetics.

Probabilistic Context-Free Grammars
The program in Fig. 3 defines a procedure CFTFrom thattakes a nonterminal symbol from the PCFG and a number tree, and returns a syntax tree generated by the PCFG
using the random numbers in the number tree. This isdone in such a way that when the number tree is generated at random in the standard way we get the probability distribution on output trees appropriate for the given
PCFG. The procedure ProdFrom takes a nonterminal anda number tree and returns the right hand side of a production from the given nonterminal. We assume that theprobability distribution over the value of ProdFrom(x, t)
is determined by the parameters of a given PCFG. The expression case e of p1 :b1 p2 : b2 is an abbreviation formatch(e,p1 ,b1 ,match(e,p2 ,b2 ,error[])).
Given the procedure ProdFrom, we can define the procedure CFT (for context-free tree) shown in Fig. 3. The procedure makes it clear that the left and right subtrees are independent with respect to the randomness introduced by thetree t. This would be true even if the left and right subtrees
were computed by arbitrary procedures, provided that theleft and right subtrees were computed from the randomness
in t.left and t.right respectively.
The procedure yield in Fig. 3 computes the string
yielded by a given syntax tree. Putting everything together,
the procedure CFString returns the yield of a randomly
generated tree.

number tree. We assume that there is some standard invertable way of coercing data structures to character strings(such as a print method). Individuals with known parents are
represented as data structures of the form child[i, f, m],where i is a unique identifier, f is the individual’s father,and m is the individual’s mother. Individuals with unknown
parents can be represented using any other data structures.
Thus, we might define a family tree as:
let steve = founder[’steve’]let jane = founder[’jane’]let alice = child[’alice’, steve, jane]
let phil = child[’phil’, steve, jane]
let jim = founder[’jim’]let bob = child[’bob’, jim, alice]

The definition of the genotype function in Fig. 2 saysthat if the individual x, has the form child[id, f, m],then his genotype is generated by the mate procedureon the parent genotypes, using the random numbers inthe subtree t.conception[x]. Otherwise, his genotype is generated by genotypePrior using the subtree
t.origin[x]. We omit the specification of any particular prior. The mate procedure performs meiosis—a processthat chooses one allele from the pair at each locus—on bothparent genotypes, using separate sets of random numbers.
The result of meiosis is a haplotype: a function mapping
each locus to a single allele. The paternal and maternal haplotypes are combined into a genotype by the deterministic
function hpair.

The Inside Algorithm
We now show that our inference rules are sufficient to derive
the inside algorithm. Suppose that we want to compute a
probability of the following form where s is a given stringof terminal symbols.

The haplotype returned by meiosis is defined by alambda-expression that takes a locus loc, interprets the
genotype value g(loc) as a pair pair[a, b], and returns a or b with equal probability. A separate random number t.loc is used for each locus. Note that becuse t.loc
has a fixed value, the resulting haplotype function will return a fixed allele if it is invoked multiple times on the same
locus.

Pt [yield(CFTfrom(X[],t))=s]
We can first apply case analysis (1) on
ProdFrom(X[],t.center[]). For length(s)>1
the resulting case probability is zero unless the production
4

yields a pair of the form pair[y, z], where y and z arenonterminal symbols. For the pair cases we are left withcomputing probabilities of the following form.

yield(CFTfrom(X[],t))=s
Pt∧ProdFrom(X[],t.center[])=pair[y, z]

is part of its syntax. We let τc be the type associated withthe term constant c and τx be the type associated with thevariable x. We have the standard notion of free and boundvariable occurrence. A term with no free variables is called
closed. Each type expression τ denotes a set [τ ]. We assume
each type constant C is associated with a specified set [C].
We take [τ1 → τ2 ] to be the set of all functions from [τ1 ] to[τ2 ]. We are only interested in well-typed exressions. We
write ` e : τ to mean that e is well-typed with type τ . We
have ` c : τc and ` x : τx . We also have ` e1 (e2 ) : σ provided ` e1 : (τ → σ) and ` e2 : τ , and ` (λ x e) : τx → σprovided ` e : σ.
We assume that each term constant c is associated witha value [c] ∈ [τc ]. We define a type-respecting variable interpretation to be a mapping α on variables with the property that for any variable x we have α(x) ∈ [τx ]. We write
α[x := v] for the variable interpretation that is identical toα except that it maps x to v. The semantics has the property that if ` e : τ then then for any type-respecting variableinterpretation α we have [e]α ∈ [τ ]. This property follows
immediately by induction on expressions under the following definition of the value of expressions.

Next
we
case
on
the
value
of
length(yield(CFTFrom(y,t.left[]))).
This
gives a probability of the following form.
#"
yield(CFTfrom(X[],t))=s
Pt ∧ProdFrom(X[],t.center[])=pair[y, z]∧Length(CFTfrom(y,t.left[]))=k
Now by logical equivalence (2) this is equivalent to a probability of the following form.
"#
ProdFrom(X[],t.center[])=pair[y, z]
Pt ∧yield(CFTfrom(y,t.left[]))=s1∧yield(CFTfrom(z,t.right[]))=s2
Here s1 consists of the first k symbols in s, and s2 is theremainder of s. We can now use syntactic independence(3) and contraction (4) to reduce this to a product of probabilities two of which are recursively of the original form.
Dynamic programming on the probability problems of theoriginal form yields the inside algorithm.

[c]α
[x]α
[e1 (e2 )]αFormal Treatment[λx e]αWe start our formal discussion by defining number trees, anda uniform measure on number trees. Let C be the set of all
finite character strings. A node s is an element of C ∗ , theset of all finite sequences of finite character strings. Notethat C ∗ can naturally be seen as a tree, where the empty
sequence ∅ is the root node, and the parent of each non-root
node (c1 , . . . , cn , cn+1 ) is the node (c1 , . . . , cn ).
A number tree T is a function from C ∗ to [0, 1]. We use∗
T to denote the set of all number trees, [0, 1]C . For any
number tree T and character string c, the c-subtree of T ,denoted T .c, is that number tree T 0 such that for each nodes = (c1 , . . . , cn ), T 0 (s) = T ((c, c1 , . . . , cn )).
As an event space on number trees, we use the product∗σ-algebra B C , where B is the Borel σ-algebra on [0, 1]. We
define the measure Punif on number trees T such that foreach node s, the random variable T (s) has a uniform distribution on [0, 1], and all these random variables are mutuallyindependent. The existence and uniqueness of this Punif follow from Kolmogorov’s extension theorem.
We now consider a particular formal language. Formallyspecifying a programming language can be tedious. For
expediency we consider the simply-typed lambda calculus
with constants. We have the following grammar for types
and terms respectively.
τ ::=
e ::=

= [c]
= α(x)= [e1 ]α ([e2 ]α )= the function v 7→ [e]α[x:=v] for v ∈ [τx ]Multi-argument functions can be represented by Currying— we represent a function f : τ1 × τ2 → σ by a Curried
function τ1 → (τ2 → σ). We can take let x be e1 in e2
to be an abbreviation for (λ x e2 )(e1 ) and we can represent a nonrecursive procedure definition define f (x) e bylet f be (λ x e) in u where u is a program using the defined procedure f . For a closed term e we write [e] for [e]αwhere α is arbitrary.
The expressive power of the simply-typed lambda calculus depends on the set of constants included in the language.
For concreteness we consider a particular language definedby a particular set of constants. We take the type constants toconsist of string for the set of character stings, node for theset of lists of character strings, real for the set of real numbers, and Bool for the set containing “true” and “false”. The
term constants include real number constants and character
string constants. The constants also include the comparison
predicates < and = on real numbers and the Boolean operations such as disjunction and negation. They also includenil, cons, car, and cdr for making and manipulating
nodes (lists of character strings). Also, for each type τ wehave the conditional operator ifτ : Bool × τ × τ → τ .
This allows us to write conditional expressions at any type.
A number tree is a function from nodes to reals — the type
tree is taken to be an abbreviation for node → real. We
can represent rand(t) by t(nil) and the subtree operation,
as in t.c, can be defined in terms of node operations andlambda abstraction. We take this particular set of constantsfor the simply typed lambda calculus to define the languge
L0 . Of course we could consider other languages with moreconstants and richer type systems.

C | τ1 → τ2
c | x | e1 (e2 ) | λ x e

Here C denotes a type constant, c denotes a term constant,and x denotes a term variable. Here we use a somewhat nonstandard formulation where we assume that each term constant and term variable is associated with a fixed type which5

is true if there exists a value v in [τ ] such that Q is true of v.
We can also allow probabilities to be terms in the langauge.
We can add a constant P : (tree → Bool) → real where
P (Q) denotes the probability that Q is true of a random tree.
This would allow probability expressions to appear inside
the statements used in probability expressions. We do notknow whether the measurability theorem holds under (someformulation of) these more extreme extensions. If the measurability theorem fails we can, as a last resort, require thatthe programmer be careful to only construct probability expressions for measurable properties.

Our first formal result is the following.
Theorem 1. If Q is a closed expression of L0 of type tree →Bool then [Q] is a measurable predicate on trees, i.e., the setof T ∈ T such that [Q]α (T ) is true is a measurable set oftrees under the measure defined above.
Proof Sketch: At an intuitive level, this theorem follows from the fact that the simply-typed lamdba calculus isstrongly normalizing. We can compute the value of Q(T )using only a finite number of comparison operations on real
numbers. This implies that the set of T ∈ T satisfying Q
can be written as a union of sets each of which is defined bya finite number of interval restrictions at a finite number ofnodes. Without loss of generality we can assume that the interval restrictions have rational endpoints — an interval canbe written as a union of intervals with rational endpoints.
There are only countably many sets definable by rational interval restrictions at a finite number of nodes. Therefore theset of T satisfying Q can be written as a countable union of
measurable sets and is therefore measurable.
Now let t be a variable of type tree and let Φ be a Boolean
expression of L0 whose only free variable is t. Given theabove measurability theorem, we can define Pt [Φ] to be theprobability that Φ is true for a random tree t, which is bydefinition the measure of the set of trees T satisfying thepredicate [λt Φ]. We can also define ∃t [Φ] to be true if there
exists a tree T satisfying the predicate [λt Φ] and we can use∀t [Φ] as an abbreviation for ¬∃t [¬Φ].
We now formally verify the rules of inference stated earlier. For the case-analysis rule (1) we require that e also has
the property that its only free variable is t. Here we also
assume that e is Boolean, although this assumption is easily
relaxed in languages that support, say, integers and integer
arithmetic. For e Boolean the case-analysis rule becomesthe following:

Conclusion
We have developed a particular approach to the combination of logic and probability yielding certain desirable inference rules. These inference rules exhibit both randomworld semantics (2) and a syntactic independence principle(3). The rules apply to a formally defined set of highly expressive logical formulas — the expressions of type Boolean
in a rich typed lambda calculus. This approach to combining logic and probability, based on number-tree semantics,
holds over a wide variety of formal lambda calculi and programming languages. We believe that our inference rules
provide a new and more tractable foundation for automatedreasoning about the rich class of stochastic models definable
by stochastic programs.

References
Bertot, Y., and Castran, P. 2004. Interactive Theorem Proving and Program Development; Coq’Art: The Calculus ofInductive Constructions. Texts in Theoretical Computer
Science. Springer.
Gordon, M., and Melham, T. 1993. Introduction to HOL: A
theorem proving environment for higher order logic. Cambridge University Press.
Kaufmann, M.; Manolios, P.; and Moore, J. S. 2000.
Computer-Aided Reasoning: An Approach. Springer.
Koller, D.; McAllester, D. A.; and Pfeffer, A. 1997. Effective Bayesian inference for stochastic programs. In
Proc. 14th AAAI, 740–747.
Milch, B.; Marthi, B.; Russell, S.; Sontag, D.; Ong, D. L.;
and Kolobov, A. 2005. BLOG: Probabilistic models withunknown objects. In Proc. 19th IJCAI, 1352–1359.
Park, S.; Pfenning, F.; and Thrun, S. 2005. A probabilistic
language based upon sampling functions. In Proc. 32nd
POPL, 171–182.
Pfeffer, A. 2001. IBAL: A probabilistic rational programming language. In Proc. 17th IJCAI, 733–740.
Poole, D. 1993. Probabilistic Horn abduction and Bayesian
networks. Artificial Intelligence 64(1):81–129.
Ramsey, N., and Pfeffer, A. 2002. Stochastic lambda calculus and monads of probability distributions. In Proc. 29th
POPL, 154–165.
Sato, T., and Kameya, Y. 2001. Parameter learning of logic
programs for symbolic–statistical modeling. JAIR 15:391–
454.

Pt [Φ] = Pt [Φ ∧ Ψ] + Pt [Φ ∧ ¬Ψ]More generally, the case-analysis rule (1) is meaningful for` e : τ where the language contains a constant denoting
each element of the set [τ ]. The other inference rules holdas stated.
Theorem 2. Inference rules (2), (3) and (4) are valid for any
Boolean expressions Φ and Ψ of L0 whose only free variable
is the tree variable t.
A natural question is how expressive can one make thelanguage while preserving the validity of the above theorems. There is no problem in adding standard data types
such as records or structures. If we allow recursion thenwe need to be careful about termination. Of course recursive functions need not terminate in general. However, if
we are careful to only write terminating recursions then it
seems that the measurability theorem still holds — we cancompute the value of a predicate on trees using only a finite number of comparisons. It also seems likely that themeasurability theorem remains true if we allow recursions
that need not terminate on all inputs but still terminate withprobability one. Another natural extension is to introduce
quantification into the langauge. For any type τ we can add
a constant ∃τ : (τ → Bool) → Bool where have that ∃τ (Q)6