Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints
This work addresses foundational issues in probabilistic programming for researchers and developers, but it is incremental as it builds on existing languages like Anglican, Church, and Venture.
The paper tackles the problem of providing a formal semantic foundation for expressive probabilistic programming languages that include higher-order functions, continuous distributions, and soft constraints, by developing operational and denotational semantics for a metalanguage and proving soundness, adequacy, and termination, with applications to validating compiler optimizations and inference algorithms like sequential Monte Carlo simulation.
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.