Termination and semantics of probabilistic lambda calculus

Thesis

This thesis gives a complete method for proving the almost sure termination of probabilistic programs, in a simply-typed higher-order language with continuous random variables and an explicit recursion construct. The method is based on supermartingales and ranking functions, which are a probabilistic version of a loop variant, as described in similar work by McIver, Morgan, Kaminski and Katoen in the setting of a first-order imperative language. The basic version of this method is extended in three ways. Sparse ranking functions permit more flexibility in how the ranking functions may be defined, so that a sparse ranking function only needs to be defined at a subset of program states, which makes providing ranking functions much more convenient. Antitone ranking functions have a weaker condition on the rate of decrease than the basic version of ranking functions, so that they can be applied to programs that terminate arbitrarily slowly. Ranking functions with respect to alternative reduction strategies allow the order in which the program is assumed to evaluate in the ranking function to deviate somewhat from the actual reduction strategy used, again making it more convenient to define ranking functions. All of these extensions may be combined, and it is proven that if a program has an antitone sparse ranking function with respect to any reduction strategy, it is almost surely terminating.

There is also an overview of probabilistic programming, with a particular focus on some of the many different ways of defining a formal semantics for probabilistic lambda calculus. The last extension of the ranking function method, relating to alternative reduction strategies, makes use of a novel variant on the operational trace-based semantics with a limited confluence result despite the random sampling. This confluent trace semantics may be of interest beyond just its application to proving almost sure termination.

Authors: Kenyon-Roberts, A

• DOI: 10.5287/ora-avq2yomgg
• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: University of Oxford
• Language: English
• Keywords: semantics; program semantics; probabilistic programming; supermartingales; ranking functions; almost sure termination; PPCF; confluence; termination; SPCF; lambda calculus
• Subjects: Programming languages (Electronic computers)--Semantics; Lambda calculus; Computer programs--Termination