Semantics And Termination Of Probabilistic Lambda Calculus

利用概率编程技术，涉及随机输入和部分观测的复杂统计模型可以由计算机处理，通过推理算法生成后验概率分布(或者在某些情况下从后验概率分布中随机抽样)。与这些程序相关的一个关键问题是几乎肯定会终止的验证。当然，任何算法如果要提供答案，就必须终止，但除此之外，还有许多结果依赖于几乎肯定会终止的假设。例如，一些推理算法，如哈密顿蒙特卡罗，只对程序的子集有效，包括AST程序。本文将给出高阶语言中几乎必然终止性的证明方法。首先，将排序函数的方法推广到具有连续概率分布的高阶语言。这里的关键结果是，如果变量可以与程序状态相关联，并且程序状态的界限在下面，并且足够快地降低预期，那么就可以得出结论，该程序是AST。文中还证明了这一结果的几个推广，使得这些变体的排序函数的构造变得更加简单和普遍。首先，只需要在程序状态的子集上定义排序函数。其次，如果允许排序函数降低的速度在某些限制内变化，则可以使用该方法证明更多种类的程序(终止得更慢)正在终止。第三，定义了迹语义的一种新的合流变体，允许定义相对于替代约简策略的终止(通常意义上的终止是在通常意义上的终止)，使得该方法的用户能够更多地利用lambda演算的灵活性，该方法在理论上是广泛适用的，但它不太适合于自动验证，需要大量的代数操作。终止验证的自动化将允许将这一工具包括在用于执行概率程序的解释器中，帮助他们确保只应用被证明是正确的算法。表示计算机可检查的校样的一种强大方式是使用依赖类型的语言。这些语言允许将证明嵌入到语言本身中，确保任何类型良好的程序都会终止，同时仍然允许比简单类型的lambda演算等程序更广泛的程序。我论文的第二部分将把这种方法扩展到概率语言和几乎必然的终止性，将AST证明嵌入到语言中，从而开发出构造演算(或其他依赖类型的系统)的概率版本，其中每个好类型的程序几乎肯定是终止性的。这些证明系统的灵活性也应该使其他终止性证明方法，如排序函数方法，作为程序嵌入语言中成为可能，我打算使用现有的终止性证明方法包括几个这样的例子。这样做的好处是，构造的概率演算的正确性证明足以证明任何可用这些技术中的任何一种终止处理的程序，而其他一切都是机器可检查的。这些证明方法的变体可以在不损失严密性和相对较少的努力的情况下使用。此外，如果这是作为另一个程序的一部分实现的，如用于检查终止的解释器，则程序员可以使用该程序涵盖的任何其他证明方法，而不必调整解释器以适应它。该项目属于EPSRC编程语言和编译器、验证和正确性、理论计算机科学以及统计和应用概率研究领域。我一直在和卢克·王合作。

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.