What is the sequent calculus for differential linear logic? [closed]

Question

I have searched, but only managed to turn up the presentation in interaction nets. I'd be equally interested in a categorical model of DiLL.

Answer 1

Although this is well-known to experts, it is surprisingly difficult to find a paper explicitly presenting the sequent calculus of (classical) differential linear logic (DiLL). The following one is a rare example:

Michele Pagani, The Cut-Elimination Theorem for Differential Nets with Boxes. In Proceedings of TLCA, LNCS 5608, pp. 219-233, 2009.

The definition is at p.3 of that paper. To make my answer a bit more self-contained, let me write the rules which are specific to DiLL, the other ones being exactly those of classical linear logic (which are much easier to find, e.g. Wikipedia). First there are rules dual to dereliction, contraction and weakening, which are (unsurprisingly) called codereliction, cocontraction and coweakening: $$ \frac{\vdash\Gamma,A}{\vdash\Gamma,!A} \qquad\qquad \frac{\vdash\Gamma,!A\quad\vdash\Delta,!A}{\vdash\Gamma,\Delta,!A} \qquad\qquad \frac{}{\vdash\,!A} $$ These rules are "dual" to the structural rules of linear logic in the sense that, if contraction and weakening behave like par and $\bot$, cocontraction and coweakening behave like $\otimes$ and $1$, respectively.

There are also the two rules dealing with sums, which are necessary in a differential context: $$ \frac{}{\vdash\Gamma} \qquad\qquad\qquad \frac{\vdash\Gamma\quad\vdash\Gamma}{\vdash\Gamma} $$ The first one tells you that every formula (hence every sequent) has a proof corresponding to $0$ (the zero of the vector space). The second one tells you that any two proofs of any formula may be added (because we are in a vector space).

The above paper also includes the so-called mix rule (and its nullary version), but those are not unanimously taken to be part of DiLL, just as they are not usually taken to be part of linear logic, although they are perfectly consistent with the system(s) and in fact virtually every denotational semantics of (differential) linear logic is a model of mix.

In any case, the rules themselves don't tell you much, it's cut-elimination that gives you their meaning. This is of course equivalent to giving a denotational semantics for them, which brings us to your second question, concerning categorical models of DiLL. I believe that the following survey by Thomas Ehrhard is an excellent introduction to the topic and should cover most of the ground:

Thomas Ehrhard, An introduction to differential linear logic: proof-nets, models and antiderivatives. Mathematical Structures in Computer Science 28(7):995-1060, 2018.

(It is funny that even this paper fails to include an explicit definition of the sequent calculus of DiLL. In fact, it is implicitly given in Sect. 1.4 but you need to know it already to see it).

Answer 2

If you're interested in a categorical semantics of differential linear logic, you probably want to look at Blute, Cockett, and Seeley's differential categories.

1. This is a recent paper revisiting the basic notion of differential categories.
2. This paper shows that the category of convenient vector spaces is a differential category.
3. The coKleisli category of a differential category is a cartesian differential category, which gives you the normal rules for differential calculus.