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

Sam Staton, Hongseok Yang, Christiaan Heunen, Ohad Kammar, Frank Wood

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.
Original languageEnglish
Title of host publicationLICS '16 Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science
Place of PublicationNew York, USA
PublisherACM
Pages525-534
Number of pages10
ISBN (Print)978-1-4503-4391-6
DOIs
Publication statusPublished - 5 Jul 2016
Event31st Annual ACM/IEEE Symposium on Logic in Computer Science - New York City, United States
Duration: 5 Jul 20168 Jul 2016
http://lics.siglog.org/lics16/

Conference

Conference31st Annual ACM/IEEE Symposium on Logic in Computer Science
Abbreviated titleLICS 2016
CountryUnited States
CityNew York City
Period5/07/168/07/16
Internet address

Fingerprint Dive into the research topics of 'Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints'. Together they form a unique fingerprint.

Cite this