Supermartingales, Ranking Functions and Probabilistic Lambda Calculus

TL;DR

This paper presents advanced methods using ranking supermartingales to prove almost sure termination of higher-order probabilistic lambda calculus programs, extending existing techniques with weaker restrictions and greater flexibility.

Contribution

It introduces antitone and sparse ranking functions, and extends the approach to alternative reduction strategies, significantly broadening the applicability of termination proofs in higher-order probabilistic programming.

Findings

Antitone ranking functions have weaker decrease restrictions.

Sparse ranking functions simplify and extend the applicability.

Methods can prove termination of complex higher-order programs.

Abstract

We introduce a method for proving almost sure termination in the context of lambda calculus with continuous random sampling and explicit recursion, based on ranking supermartingales. This result is extended in three ways. Antitone ranking functions have weaker restrictions on how fast they must decrease, and are applicable to a wider range of programs. Sparse ranking functions take values only at a subset of the program's reachable states, so they are simpler to define and more flexible. Ranking functions with respect to alternative reduction strategies give yet more flexibility, and significantly increase the applicability of the ranking supermartingale approach to proving almost sure termination, thanks to a novel (restricted) confluence result which is of independent interest. The notion of antitone ranking function was inspired by similar work by McIver, Morgan, Kaminski and Katoen in the setting of a first-order imperative language, but adapted to a higher-order functional language. The sparse ranking function and confluent semantics extensions are unique to the higher-order setting. Our methods can be used to prove almost sure termination of programs that are beyond the reach of methods in the literature, including higher-order and non-affine recursion.