SPLASH 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
Fri 22 Oct 2021 11:05 - 11:20 at Zurich F - PLDI 2021 Papers 4 Chair(s): Baris Kasikci

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 22 Oct

Displayed time zone: Central Time (US & Canada) change

10:50 - 12:10
PLDI 2021 Papers 4SIGPLAN Papers at Zurich F
Chair(s): Baris Kasikci University of Michigan, USA
10:50
15m
Talk
Compiling Stan to Generative Probabilistic Languages and Extension to Deep Probabilistic Programming
SIGPLAN Papers
Guillaume Baudart IBM Research, USA, Javier Burroni , Martin Hirzel IBM Research, Louis Mandel IBM Research, Avraham Shinnar IBM Research
11:05
15m
Talk
On Probabilistic Termination of Functional Programs with Continuous Distributions
SIGPLAN Papers
Raven Beutner University of Oxford, C.-H. Luke Ong University of Oxford
11:20
15m
Talk
SPPL: Probabilistic Programming with Fast Exact Symbolic Inference
SIGPLAN Papers
Feras Saad Massachusetts Institute of Technology, Martin C. Rinard Massachusetts Institute of Technology, Vikash K. Mansinghka MIT
DOI
11:35
15m
Talk
Cyclic Program Synthesis
SIGPLAN Papers
Shachar Itzhaky Technion, Hila Peleg Technion, Nadia Polikarpova University of California at San Diego, Reuben N. S. Rowe University of Kent, Ilya Sergey National University of Singapore
DOI
11:50
20m
Live Q&A
Discussion, Questions and Answers
SIGPLAN Papers