Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints

By S. Staton, Hongseok Yang, Chris Heunen, Ohad Kammar, Frank D. Wood. 2016

148 citations recorded by the source corpus.

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. This involves measure theory, stochastic labelled transition systems, and functor categories, but admits 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.Categories and Subject Descriptors CR-number [D.3]: Programming languages

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

In Probabilistic & Bayesian Methods

Citations in the corpus

An Introduction to Probabilistic Programming (2018, background): “(2016) also noticed that the posterior distribution fails to be defined in some models with certain observation distributions because the marginal likelihood of the observation can become infinite (Staton et al., 2016; Staton, 2017).”
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.”
Etalumis: Bringing Probabilistic Programming to Scientific Simulators at Scale (2019, unknown): “Probabilistic programming languages (PPLs) have semantics [67] that can be understood as Bayesian inference [13, 24, 26].”
A lambda-calculus foundation for universal probabilistic programming (2015, background): “The only previous work on formal semantics of λ-calculi with constraints and continuous distributions is recent work by Staton et al. (2016).”
Commutative Semantics for Probabilistic Programming (2017, background): “This sampling semantics, which has a more intensional ﬂavour and is closer to an operational intuition, is also considered by ´Scibor et al. [37] and Staton et al. [43], as well as Doberkat [7].”
Compiling Stan to generative probabilistic languages and extension to deep probabilistic programming (2021, background): “We can then define the semantics of a Stan program as a kernel [18, 30, 31], that is, a function {[p]} : D → ΣX → [0,∞] where ΣX denotes the σ -algebra of the parameter domain X , that is, the set of measurable sets of the product space of parameter values.”