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.
翻译:线性逻辑通过考虑证明与程序计算过程中所使用的资源,对直觉主义逻辑进行了精细化。过去数十年间,线性逻辑已扩展至多种框架。其中最著名的是索引线性逻辑,它能够描述程序的资源管理或复杂度分析。从另一视角看,微分线性逻辑作为一种扩展,允许对证明进行线性化处理。本文通过首先定义分级线性逻辑的微分版本,将这两个研究方向相融合:其实现方式是用微分算子幺半群对指数连接词进行索引。我们证明该体系等价于先前定义的有限微分线性逻辑扩展的分级版本。基于分布理论与常系数线性偏微分算子,我们给出了该逻辑的指称语义模型。