Resources and co-resources: a junction between semantics and descriptive complexity

We live in an information age, when computers and the software that drives them permeate every aspect of our society.
There are two fundamentally important aspects of computation.

- One concerns the resources needed to perform computational tasks: how many computational steps are needed, how much computer memory, etc.

- The other concerns our ability to master the staggering complexity of the computer systems we create and use. The only way of managing this complexity is to use principles of modularity and abstraction, so that at each step of our design and construction of the system, we see only a very limited piece, whose complexity we can master.

While the study of each of these aspects of computing has been greatly advanced as computer science has developed, currently we have a very limited understanding of how they relate to each other.
Building on our previous work, this project aims to greatly
enhance our common understanding of these issues, and to develop new mathematical tools and methods for studying computation based on this. This can lead in turn to new possibilities for fundamental advances in the field.

This research proposal is of a foundational character. Thus its most direct impact will be on Knowledge and People. These in turn have potential economic and social impact.


Knowledge impact:
The immediate scientific impact of our work will be to develop new connections and cross-fertilisations between two scientific communities: in logic and algorithms, and in semantics and type theory.
Both the new results we aim to achieve, and even more the new techniques and approaches we will develop, will be important outputs of the project.

There is also potential for wider impact, in both computer science and mathematics. In computer science, beyond the theoretical communities we have already mentioned, there is potential impact on the programming language community, especially in functional programming, and on the algorithmic side, the database and constraint satisfaction communities.
In mathematics, our work is related to logic (positive model theory) and combinatorics (structural approaches of Nesetril et al).
There are also connections with algebra (category theory and universal algebra).

People impact:
A key form of impact for this project will be on people, developing new skills and perspectives among people working in a number of different areas.
These will include those working directly on the project, including the project partners, who will acquire an enhanced unified perspective,
which they can in turn impart to the wider community.
We also see the ideas of the project spreading outwards in wider circles, into the functional programming and constraint satisfaction communities.
More widely yet, we believe that the core ideas of resources and co-resources, their monadic/comonadic formulation, and their direct application to central notions of definability and descriptive complexity, have an elegance and fundamental character which make them suitable for presentation in graduate-level courses, and eventually in standard curricula. This has the potential to influence the coming generation of computer scientists in giving a richer and more unified view of the discipline.

Pathway to Economic impact:
Our ideas on structural, high-level descriptions of meta-algorithms such as Courcelle's theorem have the potential to influence software development. The ability to mediate between high-level, structural descriptions and efficient algorithms is at the core of software development, and our work can contribute to this.