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.