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