A Lambda-Calculus Foundation for Universal Probabilistic Programming

Understand

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.