Higher categories, rewriting and complexity

This project falls within the EPSRC research areas "Information and communication technologies" and "Mathematical sciences".

Category theory has proved fruitful in logic and computer science, as a principled language to model proofs and processes. Higher category theory widens the scope of this language by including a hierarchy of reductions and equivalences between these objects, represented by higher cells. These cells are best manipulated in a diagrammatic language where topological equivalence captures structural isomorphisms. These diagrams form a generic toolkit to reason about particular theories, which has been successfully applied to information flow in quantum protocols for example.

The goal of our project is to use this toolkit for new applications in computer science and logic. First, recasting existing theories into this higher categorical framework can shine a new light on these theories. A simple change of language can have important consequences, as it can build bridges between fields. For instance, compact closed categories have been used to draw a connection between distributional semantics in linguistics and the foundations of quantum physics, which has led to new results in computational linguistics. Second, this enables the research community to share common theoretical and practical tools. On the theoretical side, mathematical results such as coherence theorems give rise to generic diagrammatic languages which can be used for a wide range of purposes. On the practical side, computer-assisted theorem provers such as Globular can help manipulate complex objects and check properties about them. These tools are crucial to turn intuitive visual evidence into solid machine-checked proofs. Third, this alternative point of view can lead to new results, or to more elegant proofs of existing theorems.

Let us give a concrete example of the application of higher category theory in logic. Linear logic designates a family of substructural logics, i.e. logics where the use of structural rules such as weakening or contraction are constrained. These systems give resource-aware calculi, which are useful to control the computational complexity of the underlying processes. They are usually presented by means of a set of rules to deduce sequents, organized into proof trees. To eliminate some spurious details about proof trees, linear logicians usually translate them to graph-based representations called proof nets. These graphical representations are ad-hoc in the sense that they are tailored specifically for these deduction systems. They suffer from some deficiencies, the main one being that not all nets correspond to valid proofs: a computationally expensive correction criterion has to be enforced. It turns out that for the multiplicative fragment of linear logic, a three-dimensional graphical calculus can be obtained via its categorical semantics. By design, this calculus has a trivial correctness criterion, as any surface diagram built on the given generators is correct. We now hope to use these diagrams to obtain a novel decision procedure for the equality of proofs for Multiplicative Linear Logic.