Higher category theory in computer science

计算机科学中的高级范畴论

• 批准号: 2218955
• 金额: --
• 依托单位: University of Oxford
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2019
• 资助国家: 英国
• 起止时间: 2019 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2218955
• 关键词: Higher; category; theory; 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.

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