Higher category theory in computer science

从根本上说，范畴论是关于结构和相互作用的数学理论。多年来，数学、它的子领域、计算机科学和物理学之间有着紧密的联系，范畴论是一种统一的语言。高等范畴论是范畴论的延伸，使它既能研究自身，也能研究其他自然的高维现象。这样的研究有可能为计算和组合性的高分类建模奠定一个统一框架的基础。这个项目的目的有两个主要目标：发展高范畴理论来模拟计算和组成现象；高等范畴论技术在解决问题中的应用。为此，我们开发了基于web的证明助手同伦。有限表示（无限符号）-类别及其基础理论，特别是这个工具使我们的研究方法新颖。而不是仅仅提供纸笔证明，传统的数学，我们也旨在提供计算机形式化的证明在适当的地方。这种工作的需要在于高范畴论的复杂性——许多定义是对很好理解的低维结构的直观的常规概括，在高维中是非常大的，这很适合计算机辅助方法，如“同伦。io”。我们研究的第二个重点是（传统的）范畴理论，使用更高范畴的工具。在将单范畴理论应用于理论计算机科学方面已经有了大量的知识，通过更好地了解范畴理论本身，我们可以为自己配备更好的工具，从而带来新的发展。例如，（乘法）线性逻辑自然地由*自治范畴建模。对于更高的范畴，我们可以把*自治范畴看作是一个有分类的Frobenius代数，并用弦图对它们进行推理。这是一个非常有用的工具，它允许我们学习*自治类别，从而导致对线性逻辑的新见解，并最终可以应用于计算机科学（例如，作为具有资源管理的编程语言的高级类型系统的形式化，如Rust），带来完整的通信循环。图解推理，可以被看作是这样一种更高范畴的技术，已经被牛津大学的基础、结构和量子小组成功地利用，极大地简化了量子理论。我们的雄心是，这项研究有一天将成为解决数学科学中长期存在的问题所需的当代数学的一部分，例如量子引力理论，或对数学中相等的哲学问题的正式检查，或对现代编程语言或复杂交互系统中高级特征的语义的更好理解。该项目属于EPSRC理论计算机科学研究领域。

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.