Semantics And Termination Of Probabilistic Lambda Calculus

With the techniques of probabilistic programming, complex statistical models involving random inputs and partial observations can be processed by computers, with inference algorithms generating the posterior probability distribution (or in some cases random samples from it). A key problem relating to these programs is the verification of almost sure termination. Naturally any algorithm must terminate if it is to ever provide an answer, but beyond that, there are many results that depend on the assumption of almost sure termination. For example, some inference algorithms like Hamiltonian Monte Carlo are valid only for a subset of programs, including the AST ones. My thesis will provide methods for proving almost sure termination in the context of higher-order languages.
First, the method of ranking functions is extended to higher-order languages with continuous probability distributions. The key result here is that if a variant can be associated with program states that is bounded below and decreases in expectation sufficiently quickly, it follows that the program is AST. Several extensions of this result are also proved that make the construction of these variants, the ranking functions, much simpler and more general. First, the ranking function only needs to be defined at a subset of program states. Second, if the speed at which the ranking function decreases is allowed to vary, within certain limits, a greater variety of programs (which terminate more slowly) can be proven to be terminating using this method. Third, a new confluent variant of trace semantics is defined that allows termination with respect to alternative reduction strategies (from which termination in the usual sense follows) to be defined, allowing the user of this method to take advantage of more of the flexibility of the lambda calculus.
This method is broadly applicable in theory, but it is not so suitable for automatic verification, requiring significant algebraic manipulation. The automation of verification of termination would allow this facility to be included in the interpreters used to execute probabilistic programs, helping them ensure they only apply algorithms that are provably correct. One powerful way of representing computer-checkable proofs is with dependently typed languages. These languages allow proofs to be embedded within the language itself, ensuring that any well-typed program is terminating while still allowing a much broader range of programs than something like simply-typed lambda calculus. The second part of my thesis will extend this approach to probabilistic languages and almost sure termination, embedding the AST proofs within the language thereby developing a probabilistic version of the calculus of constructions (or some other dependently typed system) in which every well-typed program is almost surely terminating.
The flexibility of these proof systems should also make it possible to embed other termination proof methods, such as the ranking function method, as programs within the language, and I intend to include several examples of this using existing termination proof methods. The advantage of this is that the correctness proof for the probabilistic calculus of constructions is then sufficient to prove any program treatable with any of these techniques terminating, with everything else being machine checkable. Variants on those proof methods could be used with no loss of rigour and relatively little effort. Additionally, if this were implemented as part of another program such as an interpreter to check termination, any other proof method covered by this one can then be used by the programmer without having to adjust the interpreter to accommodate it.
This project falls within the EPSRC programming languages & compilers, verification & correctness, theoretical computer science, and statistics & applied probability research areas. I have been collaborating with Luke Ong.