A Lambda-Calculus Foundation for Universal Probabilistic Programming
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 oλ-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.
Mon 19 Sep Times are displayed in time zone: Osaka, Sapporo, Tokyo change
10:45 - 12:25: Session 1Research Papers at Noh Theater Chair(s): Akimasa MorihataUniversity of Tokyo, Japan | |||
10:45 - 11:10 Talk | Farms, Pipes, Streams and Reforestation: Reasoning about Structured Parallel Processes using Types and Hylomorphisms Research Papers David Castro-PerezUniversity of St. Andrews, UK, Kevin HammondUniversity of St. Andrews, UK, Susmit SarkarUniversity of St. Andrews, UK DOI | ||
11:10 - 11:35 Talk | Dag-Calculus: A Calculus for Parallel Computation Research Papers Umut A. AcarCarnegie Mellon University, Arthur CharguéraudInria, France, Mike RaineyInria, France, Filip SieczkowskiInria, France DOI | ||
11:35 - 12:00 Talk | A Lambda-Calculus Foundation for Universal Probabilistic Programming Research Papers Johannes BorgströmUppsala University, Sweden, Ugo Dal LagoUniversity of Bologna, France, Andrew D. GordonMicrosoft Research, UK, Marcin SzymczakUniversity of Edinburgh, UK DOI | ||
12:00 - 12:25 Talk | Deriving a Probability Density Calculator (Functional Pearl) Research Papers DOI |