uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
A Lambda-Calculus Foundation for Universal Probabilistic Programming
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
Univ Bologna, I-40126 Bologna, Italy.;INRIA, Rocquencourt, France..
Microsoft Res, Cambridge, England.;Univ Edinburgh, Edinburgh EH8 9YL, Midlothian, Scotland..
Univ Edinburgh, Edinburgh EH8 9YL, Midlothian, Scotland..
2016 (English)In: SIGPLAN notices, ISSN 0362-1340, E-ISSN 1558-1160, Vol. 51, no 9, 33-46 p.Article in journal, Meeting abstract (Refereed) Published
Abstract [en]

We develop the operational semantics of an untyped probabilistic lambda-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 lambda-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.

Place, publisher, year, edition, pages
2016. Vol. 51, no 9, 33-46 p.
Keyword [en]
Probabilistic Programming, Lambda-calculus, MCMC, Machine Learning, Operational Semantics
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:uu:diva-317713DOI: 10.1145/2951913.2951942ISI: 000393580700006OAI: oai:DiVA.org:uu-317713DiVA: diva2:1082573
Conference
21st ACM SIGPLAN International Conference on Functional Programming (ICFP), SEP 18-24, 2016, Nara, JAPAN
Funder
Swedish Research Council, 2013-4853
Available from: 2017-03-17 Created: 2017-03-17 Last updated: 2017-03-17Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Search in DiVA

By author/editor
Borgström, Johannes
By organisation
Computing Science
In the same journal
SIGPLAN notices
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 7 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf