(PLDI 2021) On Probabilistic Termination of Functional Programs with Continuous Distributions
We study termination of higher-order probabilistic functional programs with recursion, stochastic conditioning and sampling from continuous distributions.
Reasoning about the termination probability of programs with continuous distributions is hard, because the enumeration of terminating executions cannot provide any non-trivial bounds. We present a new operational semantics based on traces of intervals, which is sound and complete with respect to the standard sampling-based semantics, in which (countable) enumeration can provide arbitrarily tight lower bounds. Consequently we obtain the first proof that deciding almost-sure termination (AST) for programs with continuous distributions is $\Pi^0_2$-complete. We also provide a compositional representation of our semantics in terms of an intersection type system.
In the second part, we present a method of proving AST for non-affine programs, i.e., recursive programs that can, during the evaluation of the recursive body, make multiple recursive calls (of a first-order function) from distinct call sites. Unlike in a deterministic language, the number of recursion call sites has direct consequences on the termination probability. Our framework supports a proof system that can verify AST for programs that are well beyond the scope of existing methods.
We have constructed prototype implementations of our method of computing lower bounds of termination probability, and AST verification.
Fri 17 JunDisplayed time zone: Pacific Time (US & Canada) change
10:40 - 12:00
|(OOPSLA 2020) Scaling Exact Inference for Discrete Probabilistic Programs|
|(POPL 2021) A Pre-Expectation Calculus for Probabilistic Sensitivity|
Alejandro Aguirre IMDEA Software Institute and T.U. of Madrid (UPM), Gilles Barthe MPI-SP, Germany / IMDEA Software Institute, Spain, Justin Hsu Cornell University, Benjamin Lucien Kaminski Saarland University and University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja Technical University of Denmark
|(PLDI 2021) On Probabilistic Termination of Functional Programs with Continuous Distributions|
|(POPL 2021) Paradoxes of probabilistic programming|
Jules Jacobs Radboud University