A lambda-calculus foundation for universal probabilistic programming

Abstract : We develop the operational semantics of an untyped probabilis-tic λ-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 correct-ness. 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.
Type de document :
Communication dans un congrès
International Conference on Functional Programming, 2016, Nara, Japan. pp.33 - 46, 2016, 〈10.1145/2951913.2951942〉
Liste complète des métadonnées

Littérature citée [36 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01400890
Contributeur : Ugo Dal Lago <>
Soumis le : mardi 22 novembre 2016 - 15:59:47
Dernière modification le : mercredi 10 octobre 2018 - 10:09:13
Document(s) archivé(s) le : lundi 20 mars 2017 - 22:46:42

Fichier

mh-lambda.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Johannes Borgström, Ugo Dal Lago, Andrew Gordon, Marcin Szymczak. A lambda-calculus foundation for universal probabilistic programming. International Conference on Functional Programming, 2016, Nara, Japan. pp.33 - 46, 2016, 〈10.1145/2951913.2951942〉. 〈hal-01400890〉

Partager

Métriques

Consultations de la notice

301

Téléchargements de fichiers

162