Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Unifying Graded Linear Logic and Differential Operators

Flavien Breuvart, Marie Kerjean, Simon Mirwasser

TL;DR

This work unifies graded linear logic with differential operators by indexing exponentials with a monoid of linear partial differential operators (LPDOcc). It introduces two main calculi: DB_{ S}LL, a promotion-free differential extension of graded B_SLL, and IDiLL, a heavier index-augmented differential LL, both supported by a distribution-theoretic denotational model. A core achievement is a cut-elimination procedure for DB_{ S}LL, predicated on the additive-splitting property of the LPDOcc monoid, and demonstrated coherence with a denotational semantics based on distributions, smooth functions, and fundamental solutions. The paper also outlines a pathway to a promotion-inclusive extension and discusses semantic-categorical implications, connecting logical proof theory with differential operator theory. Overall, it advances a concrete bridge between resource-sensitive logics and applied analysis, with potential applications to differential equations and graded type systems.

Abstract

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.

Unifying Graded Linear Logic and Differential Operators

TL;DR

This work unifies graded linear logic with differential operators by indexing exponentials with a monoid of linear partial differential operators (LPDOcc). It introduces two main calculi: DB_{ S}LL, a promotion-free differential extension of graded B_SLL, and IDiLL, a heavier index-augmented differential LL, both supported by a distribution-theoretic denotational model. A core achievement is a cut-elimination procedure for DB_{ S}LL, predicated on the additive-splitting property of the LPDOcc monoid, and demonstrated coherence with a denotational semantics based on distributions, smooth functions, and fundamental solutions. The paper also outlines a pathway to a promotion-inclusive extension and discusses semantic-categorical implications, connecting logical proof theory with differential operator theory. Overall, it advances a concrete bridge between resource-sensitive logics and applied analysis, with potential applications to differential equations and graded type systems.

Abstract

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.
Paper Structure (15 sections, 2 theorems, 9 equations, 1 figure)

This paper contains 15 sections, 2 theorems, 9 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Historical context
  3. Contributions
  4. Outline
  5. Linear logic and its extensions
  6. Distribution theory as a semantical interpretation of DiLL
  7. Smooth models of Classical $\mathsf{DiLL}$
  8. Metrizable spaces and their dual
  9. Vector spaces of finite dimension
  10. Interpreting $\mathsf{DiLL}_0$
  11. Differential operators as an extension of $\mathsf{DiLL}_0$
  12. Indexed linear logics: resources, effects and coeffects
  13. A differential $\mathsf{B_{\mathcal{S}}LL}$
  14. Formulas and proofs
  15. Definition of the cut elimination procedure

Key Result

Proposition 2.4

LPDOcc distribute over convolution, meaning that $D(\phi \ast \psi) = D(\phi) \ast \psi = \phi \ast D(\psi)$ for any $\phi, \psi \in \oc E$.

Figures (1)

  • Figure 1: Exponential rules of $\mathsf{DB_{\mathcal{S}}LL}$

Theorems & Definitions (8)

  • Remark 2.1
  • Remark 2.2
  • Definition 2.3
  • Proposition 2.4: Hormander, 1963
  • Theorem 2.5: name = Malgrange-Ehrenpreis
  • Definition 2.6
  • Remark 3.1
  • Definition 3.2