Source-linked AI summary
Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints
Sam Staton, Hongseok Yang, Chris Heunen, Ohad Kammar, Frank Wood
TL;DR
Expressive probabilistic programming combines higher-order functions, continuous distributions, and soft constraints, but existing accounts based on simulation algorithms are difficult to handle and extend. The paper defines a metalanguage and gives operational and denotational semantics, proving their soundness and adequacy and using them to justify program equations, including one for sequential Monte Carlo.
Problem
Expressive probabilistic programming languages lack formal exact semantics, while Monte Carlo algorithms commonly used to explain them are difficult to handle and extend.
Source: §1 · p. 1Method
The paper defines a metalanguage and develops operational and denotational semantics for probabilistic computation with higher-order functions, continuous distributions, and soft constraints.
Source: §1 · p. 1Results
The denotational semantics is sound and adequate with respect to the operational semantics, and the paper demonstrates a key program equation for sequential Monte Carlo simulation.
Source: §1 · p. 2Takeaways & Limitations
The semantics justifies useful program equations and provides a basis for studying further probabilistic-language features and inference-algorithm correctness.
Source: §10 · p. 10Sampling can create countably infinite branching, so every branch may terminate even when the expected number of steps is infinite.
Source: §5.2 · p. 6
Abstract
from arXiv · showhide
We study the semantic foundation of expressive probabilistic programming languages, that support higher-order functions, continuous distributions, and soft constraints (such as Anglican, Church, and Venture). We define a metalanguage (an idealised version of Anglican) for probabilistic computation with the above features, develop both operational and denotational semantics, and prove soundness, adequacy, and termination. They involve measure theory, stochastic labelled transition systems, and functor categories, but admit intuitive computational readings, one of which views sampled random variables as dynamically allocated read-only variables. We apply our semantics to validate nontrivial equations underlying the correctness of certain compiler optimisations and inference algorithms such as sequential Monte Carlo simulation. The language enables defining probability distributions on higher-order functions, and we study their properties.
1. Introduction
The paper provides a formal foundation for expressive probabilistic programming, where programs specify models and generic inference algorithms answer queries. It develops operational and denotational semantics for higher-order programs with continuous distributions and soft constraints, then uses them to justify program equations and results.
1. Introduction
- The language considered supports higher-order functions, continuous distributions, and soft constraints, targeting the more expressive probabilistic programming languages.The paper names Anglican, Church, and Venture as examples of this more expressive class.Source: §1 · p. 1
- Existing accounts based on Monte Carlo algorithms are difficult to handle and extend, motivating formal exact semantics for expressive probabilistic programming languages.Probabilistic programming combines programming constructs with probabilistic primitives to express models and support generic inference.Source: §1 · p. 1
- Operational semantics handles continuous distributions through stochastic relations on measurable configurations, while first-order denotational semantics interprets types as measurable spaces and terms as measurable functions.The operational semantics is also easily extended to higher-order programs.Source: §1 · p. 1
- A functor category supplies well-behaved function spaces for higher-order denotational semantics and supports continuous distributions by lifting the probability-distribution monad.Observations are interpreted using probability distributions with continuous density.Source: §1 · pp. 1–2
- The denotational semantics is sound and adequate with respect to the operational semantics, allowing program equations to be checked while respecting computational issues.The paper demonstrates a key program equation for sequential Monte Carlo simulation.Source: §1 · p. 2
- Every first-order-type term is equal to one without λ-abstractions or application, and is therefore interpreted as a measurable function.This is stated as Proposition 8.3.Source: §1 · p. 2
2. Preliminaries
The preliminaries establish measurable spaces and the measure-theoretic constructions used to interpret probabilistic programs. They also define measurable functions, stochastic relations, and indicators.
2. Preliminaries
- A measurable space is a set equipped with a σ-algebra, a family of subsets closed under complements and countable unions.A measure assigns values to measurable sets, is zero on the empty set, and is countably additive over disjoint sets; a probability measure has total mass one.Source: §2 · p. 2
- The paper builds measurable spaces from discrete sets, countable sums and products, the reals, and spaces of probability measures.For countable discrete spaces, distributions are specified by point probabilities summing to one.Source: §2 · p. 2
- A function is measurable when preimages of measurable sets are measurable, and a measure can be pushed forward along such a function.The pushed-forward measure assigns each target set the source measure of its preimage.Source: §2 · p. 2
- A stochastic relation assigns an output probability distribution to each input while requiring measurable dependence on the input.Stochastic relations correspond to measurable functions into probability-measure spaces and compose associatively.Source: §2 · p. 2
- The indicator expression [ϕ] denotes 1 when predicate ϕ holds and 0 otherwise.Source: §2 · p. 2
3. A first-order language
The first-order language is a permissive semantic metalanguage for Bayesian models, built around sampling, scoring, and normalization. Its types and effects distinguish deterministic computations from probabilistic ones.
3. A first-order language
- The language is a semantic metalanguage for practical probabilistic computation, with permissive syntax intended to support compilation and mathematical study rather than direct use.It includes infinitary type and term constructors and constants for measurable functions.Source: §3 · p. 2
Types and terms
- Types denote measurable spaces, including reals, probability measures, products, and sums; deterministic and probabilistic typing distinguish terms with sampling or scoring effects.Probabilistic terms may sample and score execution traces, while deterministic terms have no such effects.Source: §3 · p. 2
Language-specific constructs
- The language includes standard distributions and measurable functions, with sample drawing from a distribution and score multiplying the current execution trace’s score.A zero score is a hard constraint that rejects a trace; other scores are soft constraints, often encoding data likelihoods.Source: §3 · pp. 2–3
Normalization
- Normalization converts probabilistic computations into posterior distributions and model evidence by combining prior probabilities with likelihood scores.In the example, the two traces have prior probabilities 0.25 and 0.75, with scores 5.0 and 2.0, respectively.Source: §3 · p. 3
- 2.75 is the example program’s average score; the posterior probability of true rises from 0.25 to 0.45 because true better matches the datum.The program combines a Bernoulli prior with an exponential likelihood for the observation.Source: §3 · p. 3
Language-specific constructs
- Gaussian distributions with zero standard deviation are defined as unit-standard-deviation Gaussians to avoid an undefined case.Source: §3 · p. 3
4. Denotational semantics
The section interprets first-order terms over measurable spaces, mapping probabilistic computations to measures on score–result pairs. It uses the resulting program equations to justify transformations, including a sequential Monte Carlo resampling step.
4. Denotational semantics
- Probabilistic terms map each context valuation to a measure over score–result pairs, formed by pushing the prior through likelihood and return value.Source: §4 · p. 3
- The commutative-monad interpretation validates let/return equations, including reordering independent computations as an optimization [37, §5.5].The reordering equations require free-variable assumptions to avoid variable capture.Source: §4 · pp. 3–4
- Normalization integrates out scores to form an unnormalized posterior, then normalizes it when average score is neither zero nor infinite.Source: §4 · pp. 3–4
- The equations expose infinite model-evidence errors and encode the Beta–Bernoulli conjugate-prior relationship used to optimize probabilistic programs.Source: §4 · p. 4
- The normalization map ι is not a monad morphism, and Fubini failure prevents a commutative monad of all measures.Source: §4 · p. 4
4.1 Sequential Monte Carlo simulation
- Renormalize after a top-level score, record model evidence, and resample the normalized distribution for the continuation; infinite-evidence errors trigger rollback.This avoids too many executions with low scores; the rollback case does not arise in most sequential Monte Carlo applications.Source: §4.1 · p. 4
5. Operational semantics
The operational semantics models probabilistic execution with configurations and measurable transition behavior, including continuous sampling. The paper establishes termination and correspondence between operational and denotational semantics.
5. Operational semantics
- Operational semantics provides computational intuitions and is easier to extend to higher-order functions; the authors expect these intuitions to aid future study of approximate inference such as sequential Monte Carlo.Source: §5 · p. 4
- Configurations pair a term with an environment, letting the semantics handle continuous values without assigning positive probability to individual real-valued transitions.The environment supplies values for the term’s free variables.Source: §5 · p. 4
5.1 Reduction
- For uncountable indecomposable types, transitions use labelled Markov processes; decomposable types use discrete probabilistic branching.Together these approaches define the stochastic relation for probabilistic reduction.Source: §5.1 · p. 5
5.2 Termination
- Probabilistic evaluation terminates with probability 1, while deterministic evaluation is a function.The language omits recursion; individual branches terminate, although the expected number of steps can be infinite.Source: §5.2 · p. 6
5.3 Soundness
- The operational and denotational semantics satisfy the paper’s soundness result, and adequacy identifies denotation with the operational outcome distribution.The denotation is the pushforward of the operational evaluation measure to values.Source: §5.3 · p. 7
6. A higher-order language
The language extends its first-order core with functions and thunks, making program fragments first-class. These constructs support probabilistic functions and expectations over distributions on higher types.
6. A higher-order language
- Functions and thunks let variables stand for program fragments, making programs first-class citizens.Source: §6 · p. 7
- Function types represent deterministic functions, thunks represent suspended probabilistic programs, and function types returning thunks represent probabilistic functions.Source: §6 · p. 7
- Separate function and thunk types allow different calling conventions, including reifying sampling and normalization in distinct ways.The normalization function takes a suspended probabilistic program and returns its normalized result.Source: §6 · p. 7
- Higher types support probability distributions over programs and an expectation operation for distributions on types that may themselves be higher-order.The operation takes a thunked probabilistic term and a nonnegative function, then computes the function’s expectation over that distribution.Source: §6 · p. 7
7. Higher-order operational semantics
The higher-order operational semantics extends reduction with function application and thunk forcing. Under its sampling restriction, evaluation still terminates, including for probabilistic terms.
7. Higher-order operational semantics
- Operationally, sampling is restricted to distributions over measurable types, while probabilistic terms and thunks may still have higher-order types.Source: §7 · p. 7
7.1 Reduction
- Higher-order reduction adds β-reduction for function application and a redex that forces a thunked computation.Source: §7.1 · p. 7
7.2 Termination
- Deterministic evaluation is a function, and probabilistic evaluation reaches a value with probability 1, even when configurations contain higher-order terms.The termination proof uses an invariant formulated through unary logical relations.Source: §7.2 · pp. 7–8
8. Higher-order denotational semantics
The higher-order denotational semantics interprets probabilistic programs in a functor category that supports function types while retaining the first-order semantics. It is conservative at first-order types, and its soundness and adequacy connect denotational meanings with operational behavior.
8. Higher-order denotational semantics
- Probabilistic judgements are interpreted using a monad, with thunk and force relating computations to values of distribution type.The higher-order semantics extends the first-order interpretation; deterministic and probabilistic terms are interpreted as natural transformations.Source: §8 · p. 8, §8.2 · p. 9
8.1 Semantic model
- A functor category provides function spaces with currying while preserving the structure needed to interpret the first-order language.The model treats real-valued variables as read-only memory cells, and higher-order functions as measurable functions on those inputs.Source: §8 · p. 8, §8.1 · p. 8
- Distributions over functions are represented by probability distributions over measurable codes and an evaluation function, modulo renaming the codes.The lifted monad T captures the importance-sampling semantics advocated by the designers of Anglican.Source: §8.1 · pp. 8–9
8.2 Conservativity
- At first-order types, the higher-order semantics is conservative: it preserves and reflects term equality, and every term has an equal first-order representative.Consequently, even terms using thunk, abstraction, and application at first-order types denote measurable functions.Source: §8.2 · p. 9
8.3 Soundness
- The higher-order denotational semantics is sound and adequate with respect to the operational semantics, extending adequacy to higher types.Soundness requires Assumption 7.1; at higher types, adequacy is nontrivial because evaluation does not reduce under thunk or λ.Source: §8.3 · p. 9
9. Continuous densities
The language incorporates continuous probability densities as density types, allowing likelihood-based soft constraints to be expressed using scoring. This use of densities has a boundary: normalization can produce measures without continuous densities.
9. Continuous densities
- Density types represent continuous probability-density functions that integrate to one over a measurable space with a chosen σ-finite measure.The semantic model requires the base category to contain the interpretation of each density type.Source: §9 · pp. 9–10
- A likelihood-based soft constraint can be encoded as score(ev(f, x)) in the first-order language, without the higher-order categorical machinery.Here f is a continuous density and x is the observed datum; measurability of evaluation relies on density continuity.Source: §9 · p. 10
- norm(t) need not produce a measure with continuous density; norm(return(42.0)) produces a discontinuous Dirac measure.Importance sampling with proposal g is described for the case where g has support R.Source: §9 · p. 10
10. Conclusion and future work
The paper defines a metalanguage for higher-order probabilistic programs with continuous distributions and soft constraints, and gives operational and denotational semantics that justify program equations. It identifies additional language features and Monte Carlo inference algorithms as directions for future work.
10. Conclusion and future work
- The paper defines a metalanguage for higher-order probabilistic programs with continuous distributions and soft constraints, with operational and denotational semantics and semantically justified program equations.The authors propose studying recursion, function memoisation, measure-zero conditioning, disintegration, exchangeability, and correctness of Monte Carlo inference algorithms as future work.Source: §10 · p. 10