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

Abstract

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.

Cited by in corpus (28)

• Disintegration and Bayesian Inversion via String Diagrams
• A Convenient Category for Higher-Order Probability Theory
• A Domain Theory for Statistical Probabilistic Programming
• Measurable Cones and Stable, Measurable Functions
• Etalumis: Bringing Probabilistic Programming to Scientific Simulators at Scale
• Differentially Private Bayesian Programming
• Commutative Monads for Probabilistic Programming Languages
• Probabilistic call by push value
• Probabilistic Programming with Densities in SlicStan: Efficient, Flexible and Deterministic
• The Theory of Traces for Systems with Nondeterminism, Probability, and Termination
• Automatic Alignment in Higher-Order Probabilistic Programming Languages
• Multinomial and Hypergeometric Distributions in Markov Categories
• Correctness of Sequential Monte Carlo Inference for Probabilistic Programming Languages
• Synthetic topology in Homotopy Type Theory for probabilistic programming
• Distribution Bisimilarity via the Power of Convex Algebras
• Planning as Inference in Epidemiological Models
• Hijacking Malaria Simulators with Probabilistic Programming
• Optimal Approximate Sampling from Discrete Probability Distributions
• The Random Conditional Distribution for Higher-Order Probabilistic Inference
• A Fibrational Tale of Operational Logical Relations: Pure, Effectful and Differential
• Control-Data Separation and Logical Condition Propagation for Efficient Inference on Probabilistic Programs
• Supermartingales, Ranking Functions and Probabilistic Lambda Calculus
• Approximations in Probabilistic Programs
• Quasi-Measurable Spaces: A Convenient Foundation of Probability Theory
• Towards Verified Stochastic Variational Inference for Probabilistic Programs
• Parallelizable Feynman-Kac Models for Universal Probabilistic Programming
• Probabilistic Programs with Stochastic Conditioning
• Universal Semantics for the Stochastic Lambda-Calculus