Linear Logic refines Intuitionnistic Logic by taking into account the resources used during the proof and program computation. In the past decades, it has been extended to various frameworks. The most famous are indexed linear logics which can describe the resource management or the complexity analysis of a program. From an other perspective, Differential Linear Logic is an extension which allows the linearization of proofs. In this article, we merge these two directions by first defining a differential version of Graded linear logic: this is made by indexing exponential connectives with a monoid of differential operators. We prove that it is equivalent to a graded version of previously defined extension of finitary differential linear logic. We give a denotational model of our logic, based on distribution theory and linear partial differential operators with constant coefficients.
翻译:线性逻辑通过考虑证明与程序计算过程中使用的资源,对直觉主义逻辑进行了精化。在过去的几十年中,它已被扩展至多种框架。最著名的是索引线性逻辑,可用于描述程序的资源管理或复杂度分析。从另一视角看,微分线性逻辑是一种允许证明线性化的扩展。本文通过首先定义分级线性逻辑的微分版本,将这两个方向融合:这是通过用微分算子的幺半群索引指数连接词实现的。我们证明其等价于先前定义的有限微分线性逻辑扩展的分级版本。基于分布理论及常系数线性偏微分算子,我们给出了该逻辑的指称模型。