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
• 财政年份: 2019
• 资助国家: 加拿大
• 起止时间: 2019-01-01 至 2020-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=675585
• 关键词: 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.

我的项目的目标是继续探索一元范畴的理论，特别是使用线性逻辑的技术。线性逻辑模型是一个带有Monad(满足几个自然性条件的内函子)的Monid范畴。在以前的工作中，我们定义了差分范畴的概念。这些是带有附加运算符的线性逻辑模型，该运算符允许人们区分态射。对于任何线性逻辑模型，人们都可以将第二个范畴--它的Kleisli范畴联系起来。对于差分类别，该类别是平滑贴图的类别。相应的逻辑--微分线性逻辑是由Ehrhard和Regnier提出的。这为我们研究抽象的微分理论提供了一个范畴和逻辑基础。*在我们的微分范畴的概念和代数几何中更传统的概念之间存在着明显的关系，即与交换代数有关的微分形式的Kahler模。两者都典型地将一个带有导数的模与一个代数联系起来。但在区分范畴的情况下，新奇之处在于可以表达进一步的区分规则，如链式规则。然而，微分范畴缺乏定义Kahler模的普适性质。*考虑到这一点，我们提出了Kahler范畴的概念，它增加了一个适当的普适性概念，并表明在非常一般的背景下，余可微范畴是Kahler范畴。这项工作揭示了单子及其代数在卡勒理论中以前没有被观察到的重要性。我们考虑将刻画光滑代数上同调的经典Hochschild-Kostant-Rosenberg定理推广到Kahler范畴。作为这项工作的一部分，有必要定义光滑单子的概念，类似于原始HKR-定理的光滑代数。最后，我们从非对易几何中汲取灵感，将这些思想扩展到非对易环境。从我们发展的逻辑和范畴的观点来考虑积分学也是有意义的。其结果将类似于罗塔-巴克斯特代数的多对象版本。Rota-Baxter代数是具有自同态的结合代数，它满足分部积分公式的抽象和推广。*在Connes-Kreimer Hopf代数中有一个自然产生的Rota-Baxter算符，它与量子场论中的重整化有关。在过去，在与Panangden的合作中，我们证明了证明网，一种在线性逻辑中指定证明的图论语法，可以解释为受Feynman图启发的简单演算中的形式算子。积分线性逻辑的概念，其中我们有一个罗塔-巴克斯特算子的逻辑解释，可能被证明对深化这种对应很有用。