Higher category theory in computer science

点击翻译按钮获取中文摘要

Fundamentally, category theory is the mathematical theory of structure and interactions. For many years, there have been strong links between mathematics, its subfields, computer science, and physics, with category theory as a unifying language. Higher category theory is a extension of category theory to enable it to both study itself, and other naturally higher dimensional phenomena. Such research has the potential to lay the foundations for a consolidated framework for the higher-categorical modelling of computation and compositionality.The aims of this project fall under two main goals the development of higher category theory to model computational and compositional phenomena; the application of higher category-theoretic techniques to solve problems.Towards this aim, we develop the web-based proof assistant 'homotopy.io' for finitely-presented (infinity symbol)-categories and its underlying theory, and in particular this tool makes our research methodology novel. Rather than solely providing pen-and-paper proofs, as is traditional in mathematics, we also aim to give computer-formalised proofs where appropriate. The need for such an undertaking lies in the complexity of higher category theory - many definitions which are intuitively routine generalisations of well-understood lower-dimensional structure are prohibitively large in higher dimensions, and this lends itself well to a computer-aided approach à la 'homotopy.io'.Our second focus of study is (traditional) category theory, using the tools of higher categories. There is a wealth of knowledge already on applying 1-category theory to theoretical computer science at large, and by gaining better insight into category theory itself we equip ourselves with better tools which can lead to new developments. For example, (multiplicative) linear logic is naturally modelled categorically by *-autonomous categories. With higher categories, we can consider *-autonomous categories as a categorified Frobenius algebra and reason about them with string diagrams. This is a tremendously useful tool that allow us to learn about *-autonomous categories, which in turn leads to new insight into linear logic, and ultimately this can be applied to computer science (say, as a formalisation for an advanced type system for a programming language with resource management, like Rust), bringing the correspondence full-circle.Diagrammatic reasoning, which can be regarded as such a higher-categorical technique, has already been successfully exploited by the Foundations, Structures, and Quantum group, at Oxford, to vastly simplify quantum theory. It is an ambition that this research will one day be a piece of the contemporary mathematics required to solve long-standing problems throughout the mathematical sciences, such as a theory of quantum gravity, or a formal examination of the philosophical problem of equality in mathematics, or a greater understanding of the semantics of advanced features in modern programming languages or complex interacting systems.This project falls within the EPSRC Theoretical Computer Science research area.