Recursion, guarded recursion and computational effects

This three-part project develops new ways of reasoning about computer programs and new kinds of programming language.

Recursion

Programs 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 recursion

Some 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.

The research in this project is connected to several important concerns for the development of software:

- how to reason about programs to ensure that they meet appropriate
specifications, do not contain bugs and do not hang;

- how to divide a programming task between several programmers in a way that enables them to work separately, so that the coding scales with the size of the system;

- how to compile and optimize programs in a way that preserves the meaning and does not introduce bugs;

- above all, how to design and extend programming languages so as to facilitate the previous objectives.

While the project is theoretical and so its immmediate impact will be on other academic researchers, it contributes to the development of better solutions to these problems, which will benefit the software industry by enabling code to be developed faster and more correctly. In turn this will benefit society, which suffers from non-working software due to incorrect code, and from a lack of suitable software due to the slow rate of development.

Rather than concentrating on a specific programming task or problem, we examine general structures that arise in different kinds of program. Just as cells are the building blocks of living organisms, and molecules and atoms are the building blocks of matter, it has been shown using mathematical models that there are also building blocks of programs. By recognizing these and knowing their properties, and analyzing other kinds of programs in a similar way, we will be better able to produce correct code.

The main part of this work will, if successful, give a new way of writing programs that are intended to interact with users repeatedly without hanging. At present this can be done only in very restricted ways, but by extracting the building blocks of those programs we hope to construct a flexible language that will make such programs easier to write.