Recursion, guarded recursion and computational effects

这个由三部分组成的项目开发了关于计算机程序和新型编程语言的新的推理方法。递归程序经常将任务委托给其他程序，但也有一些程序更进一步：它们将任务委托给自己。这种编程风格被称为“递归”。如果做得好，它是一种强大的技术，因为它将程序员的注意力集中在如何将难题分解为更容易的部分这一关键问题上。这些部分变得越来越容易，直到它们完全简单，不需要进一步的授权。但是当递归做得不好时，程序只是无休止地委托，系统挂起。因此，我们需要能够正确地推理使用递归的程序，以确保这类问题不会发生。一种特别强大的程序推理方法被称为“指称语义”，其中每一段代码都对应于一些数学实体，我们可以直接推理这些实体。但是开发推理方法，特别是指称语义，取决于程序是用什么语言编写的。因此，开发支持递归程序推理的编程语言形式是很重要的。该项目的第一部分研究了一种称为“按推值调用”的基本理论语言中的递归，该语言已被证明提供了许多种程序的构建块。目前，在这种情况下，递归程序的指称语义是未知的，这意味着它是不可能给一个定义良好的意义部分程序。我们将通过开发一个合适的指称语义学来纠正这一点。这个阶段的成功程度将直接大大简化这个项目后两个阶段的开发。守护递归有些程序以一种特殊的方式使用递归：每次程序将一个任务委托给自己时，它就打印一条消息。这就是所谓的“保护递归”。它消除了程序挂起的风险，这是一种不受欢迎的行为，而是程序不断与用户交互。这些消息可以用来跟踪程序的执行进度，因此保护递归更容易推理。项目的第二部分也是主要部分研究保护递归，目的是开发一种语言，提供使用保护递归的程序的构建块。它将通过收集现有语言的各种指称语义，然后寻找模式来实现。第三部分，我们将使用一般递归的程序描述为使用保护递归的程序。为此，我们在程序每次委托任务时附加一条“打印消息”指令。这使得递归受到保护，并且更容易推理。一旦我们完成了推理，我们就隐藏消息，确保程序的真实的用户看不到它们，所以从他们的角度来看，递归是不受保护的。我们用这个想法给指称语义的语言与一般递归，在目前被认为具有挑战性的设置。这将说明保护递归对于任意递归程序的重要性。

This three-part project develops new ways of reasoning about computer programs and new kinds of programming language.RecursionPrograms frequently delegate tasks to other programs, but there are some programs that take this a step further: they delegate tasks to themselves. This style of programming is called "recursion". When it is done well, it is a powerful technique, because it focuses the programmer's attention on the key question of how to break down their hard problem into easier parts. And the parts get easier and easier until they are completely straightforward and no further delegation is required. But when recursion is done badly, the program just keeps delegating endlessly and the system hangs. Therefore, we need to be able to reason correctly about programs that use recursion, to make sure this kind of problem does not happen. One particularly powerful way of reasoning about programs is called "denotational semantics", where every piece of code corresponds to some mathematical entity, and we can reason directly about those entities. But developing reasoning methods, and denotational semantics in particular, depends on what language the programs are written in. So it is important to develop forms of programming language that support reasoning about recursive programs. The first part of the project investigates recursion in a fundamental theoretical language called "call-by-push-value", which has been shown to provide the building blocks from which many kinds of programs are made. At present, denotational semantics for recursive programs in this setting are not known, which means that it is impossible to give a well-defined meaning to parts of programs. We shall rectify this by developing a suitable denotational semantics. The degree of success of this stage will directly and greatly simplify the development of the later two stages of this project.Guarded recursionSome programs employ recursion in a special way: every time the program delegates a task to itself, it prints a message. This is called "guarded recursion". It eliminates the risk of the program hanging, which is an undesirable behaviour, and instead the program continually interacts with the user. The messages can be used to track the progress of the program's execution, and for this reason guarded recursion is easier to reason about.The second and main part of the project investigates guarded recursion, with the aim of developing a language that provides the building blocks of programs using guarded recursion. It will do this by collecting various denotational semantics of existing languages and then looking for patterns.For the third part, we describe a program using general recursion into a program using guarded recursion. To do so, we attach a "print message" instruction each time the program delegates a task. That makes the recursion guarded, and easier to reason about. Once we have completed our reasoning, we hide the messages, making sure that the real user of the program cannot see them, so from their viewpoint the recursion is not guarded. We use this idea to give denotational semantics to a language with general recursion, in a setting currently considered challenging. This will illusrate the importance of guarded recursion for arbitrary recursive programs.