Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Internship report: Coherent differentiation in models of Linear Logic

Aymeric Walch

TL;DR

This internship report proves that the deriving transformation of a differential category with a categorical product always induces a coherent differentiation, which ensures that coherent differentiation is indeed a generalization of differential categories.

Abstract

Coherent differentiation was introduced by Ehrhard in order to generalize differential categories to a setting in which the sum is only partially defined, in order to account for the deterministic nature of most models of computation. This internship report proves that the deriving transformation of a differential category with a categorical product always induces a coherent differentiation. This ensures that coherent differentiation is indeed a generalization of differential categories.

Internship report: Coherent differentiation in models of Linear Logic

TL;DR

This internship report proves that the deriving transformation of a differential category with a categorical product always induces a coherent differentiation, which ensures that coherent differentiation is indeed a generalization of differential categories.

Abstract

Coherent differentiation was introduced by Ehrhard in order to generalize differential categories to a setting in which the sum is only partially defined, in order to account for the deterministic nature of most models of computation. This internship report proves that the deriving transformation of a differential category with a categorical product always induces a coherent differentiation. This ensures that coherent differentiation is indeed a generalization of differential categories.

Paper Structure

This paper contains 21 sections, 6 theorems, 6 equations.

Table of Contents

  1. A (brief) introduction to categorical semantic
  2. A small and non exhaustive reminder on proof systems
  3. Why categories are natural viewpoints on semantic
  4. Exhibiting the structure that $\IfStrEqCase{0}{{0}{\mathcal{L}} {1}{\mathcal{C}} {2}{\mathcal{D}} {3}{\mathcal{E}}} []$ must have
  5. An introduction to linear logic
  6. Symetric monoidal categories
  7. Deducing the syntax from the semantic
  8. About the weakening and contraction rules
  9. The Seely isomorphisms
  10. The structure of $!$
  11. Differentiation in some models of linear logic
  12. Coherent differentiation
  13. Pre-summability structure
  14. Summability structure
  15. The differentiation operator
  16. ...and 6 more sections

Key Result

Theorem 1

The cut rule is admissible in LJ. In other word: for any proof using the cut rule, there exists a proof of the same sequent that does not use the cut rule. Besides, the proof of this theorem gives an explicit procedure called the cut elimination procedure that takes as input any proof using the cut

Theorems & Definitions (60)

  • Definition 1
  • Definition 2
  • Definition 3
  • Definition 4
  • Definition 5
  • Remark 1
  • Theorem 1: Cut elimination
  • Definition 6
  • Definition 7: Models
  • Definition 8
  • ...and 50 more