A lambda-calculus foundation for universal probabilistic programming
By Johannes Borgström, Ugo Dal Lago, A. Gordon, Marcin Szymczak. 2015
115 citations recorded by the source corpus.
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.
Subfields: Artificial Intelligence, Probabilistic & Bayesian Methods
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Artificial Intelligence
- Hongseok Yang
- Frank D. Wood
- Jan-Willem van de Meent
- David Tolpin
- S. Staton
- Yura N. Perov
- Brooks Paige
- Tom Rainforth
In Probabilistic & Bayesian Methods
- Hongseok Yang
- Frank D. Wood
- Jan-Willem van de Meent
- David Tolpin
- S. Staton
- Yura N. Perov
- Brooks Paige
- Tom Rainforth
Citations in the corpus
- Design and Implementation of Probabilistic Programming Language Anglican (2016, background): “Formal semantics for an idealized version of Anglican or other higher-order probabilistic programming languages are introduced in [4, 24]; in general though, specifying semantics of higher-order probabilistic programming languages is an open problem.”
- Commutative Semantics for Probabilistic Programming (2017, background): “B¨orgstrom et al. [4] call this a sampling semantics by contrast with the distribution semantics that we have considered here.”
- A convenient category for higher-order probability theory (2017, unknown): “’s operational (not denotational as in this paper) semantics for a higher-order probabilistic programming language with continuous distributions [6], which has been used to justify a basic inference algorithm for the language.”