Recursion, guarded recursion and computational effects

Lead Research Organisation: University of Birmingham
Department Name: School of Computer Science

Abstract

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.

Planned Impact

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.

Publications

10 25 50
 
Description (1) In most programming languages, each piece of data has a type, such as the type of numbers or colours. A key question is when two types are essentially the same. I showed that the traditional answer doesn't work in general, whereas a new answer, based on the legitimacy of replacing one type by the other in any context, works in several different kinds of programming language. (2) In many programs, data stored at one place in computer memory includes the address of data at another location, and so forth. When several such programs delegate tasks to each other, and pass information about the addresses to each other, the resulting software is intricate and hard to reason about. We developed a model of such programs that helps us to reason about their behaviour. (3) We developed a general way of reasoning about when programs are equivalent that works (in particular) for programs whose behaviour is random. (4) We developed a general framework for giving meaning to programs that continue indefinitely to interact with users. (5) We found a way of reasoning about correctness of frameworks for giving meaning to programs that act on other programs by solely considering the program code itself. (6) We found a problem in a plausible model of programs that continue indefinitely to interact with users, because something in the model appears to continue operating whereas in fact it does not. (7) We found a way of modelling the set of possible behaviours of programs that interact with users; it works both for those that are guaranteed to eventually end and those that may continue indefinitely. (8) We found a way of structuring recursive programs that may also input and output and the equations that such programs satisfy. (9) We characterized the applicability of structures (known as "strength") that are used in functional programming where data is of one sort in a more general setting where there are several sorts of data.
Exploitation Route It might be studied for a wider variety of programming languages. It might enable software libraries written for one type to be applied to data of another type that is essentially the same in this new sense. It might make it easier to write higher-order programs with pointers without bugs.
Sectors Digital/Communication/Information Technologies (including Software)

URL http://www.cs.bham.ac.uk/~pbl/papers
 
Description effectfulhowe 
Organisation French Institute for Research in Computer Science and Automation
Country France 
Sector Private 
PI Contribution I suggested how earlier work done by other team members on reasoning about program equivalence for probabilistic programs could be seen as an instance of a more general technique.
Collaborator Contribution They worked out the details of my suggestion, and determined for which cases it would work.
Impact A paper " Effectful Applicative Bisimilarity: Monads, Relators and Howe's Method" published in the conference Logic in Computer Science, Reykjavik 2017, listed in the Publications section. Not multi-disciplinary.
Start Year 2016
 
Description sergeygoncharov 
Organisation Friedrich-Alexander University Erlangen-Nuremberg
Country Germany 
Sector Academic/University 
PI Contribution I contributed the overall goal of giving a universal property for algebraic structures (monads) that support iteration and cover a wider range of examples than previously studied. Also, I simplified some of the arguments.
Collaborator Contribution Sergey Goncharov contributed a substantial technical knowledge of earlier methods for a narrower range of results that he then applied to give our results.
Impact The paper "Coinductive resumption monads: guarded iterative and guarded Elgot", which appears in the proceedings of 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). The DOI is 10.4230/LIPIcs.CALCO.2019.13 but Crossref doesn't recognize this for some reason, and therefore Researchfish doesn't either.
Start Year 2017
 
Description stepstraces 
Organisation Radboud University Nijmegen
Country Netherlands 
Sector Academic/University 
PI Contribution I noticed an algebraic structure within my earlier work, developed the necessary concepts to formulate it in a general way, and simpilfied the resulting narrative.
Collaborator Contribution They provided several examples that were included within a framework they had previously developed.
Impact http://dx.doi.org/10.1007/978-3-030-00389-0_8
Start Year 2017