Sciweavers

CORR
2016
Springer

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

7 years 12 months ago
Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints
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.
Sam Staton, Hongseok Yang, Chris Heunen, Ohad Kamm
Added 31 Mar 2016
Updated 31 Mar 2016
Type Journal
Year 2016
Where CORR
Authors Sam Staton, Hongseok Yang, Chris Heunen, Ohad Kammar, Frank Wood
Comments (0)