Linear logic, finiteness spaces and bicategories

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

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.