A Lambda-Calculus Foundation for Universal Probabilistic Programming

Johannes Borgstrom, Ugo Dal Lago, Andrew D. Gordon, Marcin Szymczak

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

Abstract

We develop the operational semantics of an untyped probabilistic λ-calculus with continuous distributions, and both hard and soft constraints, as a foundation for universal probabilistic programming languages such as CHURCH, ANGLICAN, and VENTURE. Our first contribution is to adapt the classic operational semantics of λ-calculus to a continuous setting via creating a measure space on terms and defining step-indexed approximations. We prove equivalence of big-step and small-step formulations of this distribution-based semantics. To move closer to inference techniques, we also define the sampling-based semantics of a term as a function from a trace of random samples to a value. We show that the distribution induced by integration over the space of traces equals the distribution-based semantics. Our second contribution is to formalize the implementation technique of trace Markov chain Monte Carlo (MCMC) for our calculus and to show its correctness. A key step is defining sufficient conditions for the distribution induced by trace MCMC to converge to the distribution-based semantics. To the best of our knowledge, this is the first rigorous correctness proof for trace MCMC for a higher-order functional language, or for a language with soft constraints.
Original languageEnglish
Title of host publicationProceedings of the 21st ACM SIGPLAN International Conference on Functional Programming
Place of PublicationNara, Japan
PublisherACM
Pages33-46
Number of pages14
ISBN (Electronic)978-1-4503-4219-3
DOIs
Publication statusPublished - 4 Sep 2016
Event21st ACM SIGPLAN International Conference on Functional Programming - Nara, Japan
Duration: 18 Sep 201624 Sep 2016
https://conf.researchr.org/home/icfp-2016

Publication series

NameACM SIGPLAN Notices
PublisherACM
Number9
Volume51
ISSN (Print)0362-1340
ISSN (Electronic)1558-1160

Conference

Conference21st ACM SIGPLAN International Conference on Functional Programming
Abbreviated titleICFP 2016
CountryJapan
CityNara
Period18/09/1624/09/16
Internet address

Fingerprint

Dive into the research topics of 'A Lambda-Calculus Foundation for Universal Probabilistic Programming'. Together they form a unique fingerprint.

Cite this