On Termination of Higher-Order Recursive Programs with Continuous Distributions

Hoare Prize
Raven Beutner

We study almost-sure termination (AST) of higher-order probabilistic functional programs with recursion, stochastic conditioning and sampling from continuous distributions. In the first part of this work, we present a new interval-based operational semantics that we show sound and complete with respect to the standard sampling-based semantics `a la Borgstr¨om et al. [2016]. In contrast to the sampling-based semantics, in our semantics enumeration of terminating computations provides arbitrarily tight lower bounds on the probability of termination, making it attractive for program analysis. As a consequence we obtain, to the best of our knowledge, the first proof that deciding AST for programs with continuous distributions is Π02-complete. Extending the work of [Breuvart and Lago 2018] we give a compositional characterisation of our semantics in the form of an intersection type system that provides a local interpretation of AST. In the second part, we propose a framework to prove almost-sure termination for nonaffine programs, i.e., recursive programs that can make any number of recursive calls (of a first-order function) from a finite number of lexically different call-sites. While the number of recursion call-sites is irrelevant to qualitative questions about termination, we show that it is very much relevant in the quantitative setting of AST. Our framework over-approximates recursion by counting the number of recursive calls, reducing a program to a random walk for which we establish AST decidability in linear time. As a simple corollary we obtain a functional generalization of the zero-one law of termination by [McIver and Morgan 2005]. We show that our framework can be turned into a proof system that is easy to automate, and can verify AST for programs that are beyond the scope of existing methods.

Oxford University (Master Thesis) October 2020
Contact Data Privacy Policy Imprint
Home People Publications
More