Linear logic, finiteness spaces and bicategories

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

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.