Linear logic, finiteness spaces and 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.