Linear logic, finiteness spaces and bicategories

线性逻辑、有限空间和二分类

• 批准号: RGPIN-2022-03900
• 负责人: Blute, Richard
• 金额: $ 1.31万
• 依托单位: University of Ottawa
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2022
• 资助国家: 加拿大
• 起止时间: 2022-01-01 至 2023-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=759200
• 关键词: Linear; logic; finiteness; spaces; bicategories

I work in a branch of mathematics known as category theory. The algebra of category theory can be used to reveal profound relationships between seemingly quite disparate mathematical structures. A category is (typically) a class of mathematical structures (objects) and structure-preserving functions between them (arrows). A functor allows one to map one category to another. This simple idea can yield surprisingly deep results and consistently has done so since the creation of category theory in 1945. More specifically, I work in categorical logic, which in recent years has been quite an active field of mathematics. My colleagues and I take fundamental principles of logic and apply them to other areas of mathematics using category theory. One can form a category for which the objects are formulas in a given logic and the arrows are deductive proofs of those formulas. The specific logic I primarily use is linear logic. Linear logic, defined by Jean-Yves Girard, is a logic with a resource-sensitive inference rule structure. It has been of fundamental importance in computer science where one is interested in optimal use of time and resources in performing a calculation. It has also been of great value in understanding some of the more abstract approaches to quantum mechanics. There is a specific model of linear logic due to Thomas Ehrhard called the category of finiteness spaces. In addition to being a rich model of linear logic which has sufficient structure to model the many connectives of that logic, it has a strong computational property as well. When applying finiteness spaces in a specific way in certain computational settings, the summations that would a priori be infinite and hence either fail to exist or be difficult to compute become finite. This idea, which was developed by myself and various coauthors, has already led to a number of exciting results. My primary research will be to continue applying this idea to more complex settings. One area for which I suspect this idea will yield strong results is in the algebraic approach to enumerative combinatorics. Many of the strongest results in this field have followed from Rota's abstract approach to Mobius inversion. Mobius inversion originally arose in number theory as a relation between arithmetic functions, but Rota's generalization applies much more broadly. In this setting, summations must be proven to be finite. We have already shown that some of the basic examples of Mobius inversion fit into our finiteness spaces framework, but there is a great deal more work to be done. Finally, there is a more complex version of the notion of category called a bicategory. In this definition, we allow not just objects and arrows, but higher-order arrows that go between arrows. The algebra of this idea is quite daunting, but there are a great many important applications. Finiteness spaces have already been shown to yield new examples of bicategories, and I intend to explore this idea further.

我研究的是一个叫做范畴论的数学分支。范畴论的代数可以用来揭示看似完全不同的数学结构之间的深刻关系。范畴（通常）是一类数学结构（对象）和它们之间保持结构的函数（箭头）。函子允许将一个类别映射到另一个类别。这个简单的想法可以产生令人惊讶的深刻结果，并且自1945年范畴论创立以来一直如此。更具体地说，我研究的是近年来相当活跃的数学领域——范畴逻辑。我和我的同事将逻辑的基本原理运用到范畴论的其他数学领域。人们可以形成一个范畴，其中对象是给定逻辑中的公式，箭头是这些公式的演绎证明。我主要使用的逻辑是线性逻辑。线性逻辑是由Jean-Yves Girard定义的一种具有资源敏感推理规则结构的逻辑。在计算机科学中，当人们对执行计算时时间和资源的最佳利用感兴趣时，它具有重要的基础意义。它在理解量子力学的一些更抽象的方法方面也有很大的价值。线性逻辑有一个特殊的模型是由Thomas Ehrhard提出的，叫做有限空间的范畴。它不仅是一个丰富的线性逻辑模型，具有足够的结构来模拟该逻辑的许多连接词，而且还具有很强的计算性。当在特定的计算环境中以特定的方式应用有限空间时，先验的和是无限的，因此要么不存在，要么难以计算，变成有限的。这个想法是由我和其他合作者提出的，已经产生了许多令人兴奋的结果。我的主要研究将是继续把这个想法应用到更复杂的环境中。我怀疑这个想法将产生强有力结果的一个领域是枚举组合学的代数方法。这个领域的许多最有力的结果都是从罗塔对莫比乌斯反演的抽象方法中得到的。莫比乌斯反转最初作为算术函数之间的关系出现在数论中，但罗塔的推广应用得更广泛。在这种情况下，必须证明求和是有限的。我们已经证明了莫比乌斯反演的一些基本例子适合我们的有限空间框架，但还有很多工作要做。最后，范畴概念还有一个更复杂的版本，叫做双范畴。在这个定义中，我们不仅允许对象和箭头，还允许在箭头之间的高阶箭头。这个想法的代数是相当令人生畏的，但有很多重要的应用。有限空间已经被证明可以产生双范畴的新例子，我打算进一步探索这个想法。