A Lambda-Calculus Foundation for Universal Probabilistic Programming

TL;DR

This paper establishes a formal operational semantics for a probabilistic lambda-calculus with continuous distributions, providing a foundation for universal probabilistic programming languages and proving the correctness of trace MCMC inference.

Contribution

It adapts lambda-calculus semantics to continuous distributions, formalizes trace MCMC, and proves its correctness for higher-order probabilistic languages.

Findings

Proves equivalence of big-step and small-step semantics.

Defines sampling-based semantics matching distribution-based semantics.

Provides the first rigorous correctness proof for trace MCMC in higher-order languages.

Abstract

We develop the operational semantics of an untyped probabilistic lambda-calculus with continuous distributions, 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 integrating over all 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.