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.