Semantics And Termination Of Probabilistic Lambda Calculus

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

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.