Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

From Differential Linear Logic to Coherent Differentiation

Thomas Ehrhard

TL;DR

This work introduces coherent differentiation (CD), a principled framework that makes differential reasoning deterministic within differential linear logic. It builds a summability structure on a linear category, enabling controlled addition of morphisms and a differentiation monad via a distributive law between the summability functor ${f S}$ and the exponential comonad. The theory is instantiated in elementary models such as coherence spaces and probabilistic coherence spaces, and it extends to closed settings and fixpoints, yielding a rich interplay between denotational and syntactic descriptions. The CD syntax (PCF_cd) and its operational and denotational semantics culminate in adequacy and determinism results, and pave the way for Taylor expansions and iterated derivatives in a deterministic, resource-aware setting.

Abstract

In this survey, we present in a unified way the categorical and syntactical settings of coherent differentiation introduced recently, which shows that the basic ideas of differential linear logic and of the differential lambda-calculus are compatible with determinism. Indeed, due to the Leibniz rule of the differential calculus, differential linear logic and the differential lambda-calculus feature an operation of addition of proofs or terms operationally interpreted as a strong form of nondeterminism. The main idea of coherent differentiation is that these sums can be controlled and kept in the realm of determinism by means of a notion of summability, upon enforcing summability restrictions on the derivatives which can be written in the models and in the syntax.

From Differential Linear Logic to Coherent Differentiation

TL;DR

This work introduces coherent differentiation (CD), a principled framework that makes differential reasoning deterministic within differential linear logic. It builds a summability structure on a linear category, enabling controlled addition of morphisms and a differentiation monad via a distributive law between the summability functor and the exponential comonad. The theory is instantiated in elementary models such as coherence spaces and probabilistic coherence spaces, and it extends to closed settings and fixpoints, yielding a rich interplay between denotational and syntactic descriptions. The CD syntax (PCF_cd) and its operational and denotational semantics culminate in adequacy and determinism results, and pave the way for Taylor expansions and iterated derivatives in a deterministic, resource-aware setting.

Abstract

In this survey, we present in a unified way the categorical and syntactical settings of coherent differentiation introduced recently, which shows that the basic ideas of differential linear logic and of the differential lambda-calculus are compatible with determinism. Indeed, due to the Leibniz rule of the differential calculus, differential linear logic and the differential lambda-calculus feature an operation of addition of proofs or terms operationally interpreted as a strong form of nondeterminism. The main idea of coherent differentiation is that these sums can be controlled and kept in the realm of determinism by means of a notion of summability, upon enforcing summability restrictions on the derivatives which can be written in the models and in the syntax.
Paper Structure (27 sections, 57 theorems, 92 equations, 7 figures)

This paper contains 27 sections, 57 theorems, 92 equations, 7 figures.

Table of Contents

  1. Notations and terminology
  2. Differentiation in LL
  3. A first attempt: the derivative of a stable function
  4. Coming back to differentiation in LL
  5. Coherence and determinism
  6. Summability structures in a linear setting
  7. Partial monoids
  8. Summability structures
  9. The monad structure of ${\mathsf S}$
  10. Compatibility of the summability structure with the tensor product and the internal hom
  11. Summability in a cartesian category
  12. Summability in the elementary situation
  13. The differential structure
  14. The induced differentiation monad
  15. Partial derivatives
  16. ...and 12 more sections

Key Result

Lemma 4.1

Let $(M,0,\mathord +)$ be a partial commutative monoid. Let $\vec{a}\in M^n$ and let $f:\{1,\dots,n\}\to\{1,\dots,n\}$ be a bijection. The sequence $\vec{a}$ is summable iff $(a_{f(1)},\dots,a_{f(n)})$ is summable, and then $\sum_{i=1}^na_i=\sum_{i=1}^na_{f(i)}$.

Figures (7)

  • Figure 1: Typing rules for $\mathsf{PCF}_\mathsf{cd}$
  • Figure 2: Definition of $\partial(x,M)$
  • Figure 3: Typing rules for stacks
  • Figure 4: Context associated with a stack
  • Figure 5: Transition rules for states --- pushing onto the stack
  • ...and 2 more figures

Theorems & Definitions (150)

  • Remark 3.1
  • Definition 4.1
  • Remark 4.1
  • Definition 4.2
  • Lemma 4.1
  • Definition 4.3
  • Theorem 4.1
  • Lemma 4.2
  • proof
  • Definition 4.4
  • ...and 140 more