Linear Logic, Monoidal Categories and Abstract Models of Differentiation and Integration

线性逻辑、幺半范畴与微分与积分的抽象模型

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

The goal of my project will be to continue to explore the theory of monoidal categories, especially using the techniques of linear logic. A model of linear logic is a monoidal category equipped with a monad (an endofunctor satisfying several naturality conditions). In previous work, we have defined the notion of differential category. These are models of linear logic with an additional operator which allows one to differentiate morphisms. To any model of linear logic, one can associate a second category, its Kleisli category. For differential categories, this category is a category of smooth maps. The corresponding logic, differential linear logic, was introduced by Ehrhard and Regnier. This then gives us a categorical and logical foundation for considering abstract theories of differentiation. There is an evident relationship between our notion of differential category and the more traditional notion from algebraic geometry of a Kahler module of differential forms associated to a commutative algebra. Both canonically associate to an algebra a module equipped with a derivation. But in the case of differential categories, the novelty is that one can express further differentiation rules such as the chain rule. However differential categories lack the universal property defining Kahler modules. With this in mind, we developed the notion of Kahler category which adds in an appropriate notion of universality and showed that in a very general setting, codifferential categories are Kahler. This work revealed the previously unobserved importance of monads and their algebras in Kahler theory. We are looking into extending the classical Hochschild-Kostant-Rosenberg theorem characterizing the cohomology of smooth algebras to the setting of Kahler categories. As part of this work, it is necessary to define the notion of a smooth monad in analogy to the smooth algebras of the original HKR-theorem. FInally, we are working on an extension of these ideas to the noncommutative setting, drawing our inspiration from noncommutative geometry. It also makes sense to consider the integral calculus from the logical and categorical viewpoint we have developed. The result would be something like a multi-object version of Rota-Baxter algebras. Rota-Baxter algebras are associative algebras with an endomorphism which satisfies an abstraction and generalization of the integration by parts formula. There is a naturally occurring Rota-Baxter operator in the Connes-Kreimer Hopf algebra associated to renormalization in quantum field theory. In the past, in joint work with Panangaden, we showed that proof nets, a graph-theoretic syntax for specifying proofs in linear logic, can be interpreted as formal operators in a simple calculus inspired by Feynman diagrams. A notion of integral linear logic in which we have a logical interpretation of a Rota-Baxter operator, may prove useful in deepening this correspondence.

我的项目的目标将是继续探索monoidal范畴理论，特别是使用线性逻辑的技术。线性逻辑的模型是一个配备有单子（满足几个自然性条件的内函子）的monoidal范畴。在以前的工作中，我们已经定义了微分范畴的概念。这些模型的线性逻辑与额外的运营商，使之能够区分态射。对于任何线性逻辑模型，我们都可以将第二个范畴，即克莱斯利范畴联系起来。对于微分范畴，这个范畴是光滑映射的范畴。相应的逻辑，微分线性逻辑，由Ehrhard和Regnier介绍。这样，我们就有了一个范畴的和逻辑的基础来考虑抽象的分化理论。 在我们的微分范畴概念和与交换代数相关联的微分形式的Kahler模的代数几何中的更传统的概念之间存在着明显的关系。两者都规范地将一个代数与一个带有导子的模联系起来。但在微分范畴的情况下，新颖之处在于人们可以表达更进一步的微分规则，如链式规则。然而，微分范畴缺乏定义Kahler模的泛性质。 考虑到这一点，我们发展了卡勒范畴的概念，它增加了一个适当的普遍性概念，并表明在一个非常一般的设置，余微分范畴是卡勒。这项工作揭示了以前未观察到的重要性单子和他们的代数在卡勒理论。我们正在研究扩展经典的Hochschild-Kostant-Rosenberg定理，刻画光滑代数的上同调到Kahler范畴的设置。作为这项工作的一部分，有必要定义一个光滑单子的概念，类似于原来的HKR定理的光滑代数。最后，我们正在努力将这些想法扩展到非对易的环境，从非对易几何中汲取灵感。 从我们所发展的逻辑和范畴的观点来考虑积分也是有意义的。其结果将类似于Rota-Baxter代数的多对象版本。Rota-Baxter代数是具有满足分部积分公式的抽象和推广的自同态的结合代数。 在与量子场论中的重整化有关的Connes-Kreimer Hopf代数中，存在一个自然出现的Rota-Baxter算子。在过去，在与Panangelo的联合工作中，我们证明了证明网，一种在线性逻辑中指定证明的图论语法，可以被解释为受费曼图启发的简单微积分中的形式运算符。积分线性逻辑的概念，其中我们有一个逻辑解释的Rota-Baxter运营商，可能会被证明是有用的深化这一对应关系。