(work in progress)
Differential linear logic is an extension of linear logic. New inference rules are added which allow to differentiate proofs. Proofs must be understood as morphisms and the new inference rules are here to differentiate them. It was realised than in some denotational models of linear logic, the morphisms of the co-Kleisli category are differentiable, and it was then reflected in the syntax by these new inference rules. Thus, one really needs to take the point of view of computational trinitarianism in order to understand the transition from linear logic to differential linear logic. It is more difficult to understand naively the proofs of differential linear logic than the ones of linear logic.
Differential linear logic can be presented in different guises whether we include the additives or not, and whether we include the promotion or not. We start by presenting the version without additives and with promotion. We will refer to this logic as DiLL.
There are two ways to present the syntax in sequent calculus. With bilateral sequents or monolateral sequents. The first one is closer to the language of category theory but the second one allows to make the links with the syntax in proof nets and to divide by two the number of inference rules. Using the monolateral version (or proof nets) require to quotient the formulas by some equalities related to negation and De Morgan duality.
There are no novelties concerning formulas compared to linear logic. We will work with the formulas of Multiplicative Exponential Linear Logic (MELL). In the next subsection, the difference between MELL and DiLL will appear as additional inference rules.
Formulas are given by induction starting from atoms and applying connectives. In accordance with the tradition, formulas and atoms are denoted in the same way by upper case letters:
If we want to use the monolateral sequent calculus (or proof nets), formulas must be quotiented by the following equalities:
Notice that some equalities are implied by other ones and thus we could give a shorter list. We have preferred writting directly all the equalities of pratical use.
Inference rules will allow us to build proofs. Notice that compared to MELL, we need the ability to sum proofs. We give an explicit rule for this summation of proofs. We give also a rule for null proofs. Finally, the new inference rules are: coderiliction, cocontraction, coweakening, sum of proofs, null proof.
There is a rewriting system which, given an instance of the cut rule in a proof, reduces the proof by making the cut go higher in the proof. There is the key cases which induce important commuting diagrams in the categorical semantics and the commuting cases which are less important. The idea is that when a cut arrives at the beginning of the proof, ie. at the level of the leafs which are axioms, we can finally eliminate it by a last rewriting step. This is when the cut is made against an axiom rule, that we can eliminate it. We know that this rewriting system is strongly normalizing and that the normal forms are the cut-free proofs. It means that by using rewriting rules in the order you want, at the end you obtain a proof without cut, thus the name cut-elimination. It is important to know actually this rewriting system and not only that we can eleminate the cuts in a proof because this cut-elimination prodecure creates the commuting diagrams of the categorical semantics when we quotient the proofs by these cut-elimination steps.
We need a *-autonomous category in order to interpret the connectors and rules related to these connectors: $\otimes, \parr, 1, \bot, {}^{\perp}$.
This category must be enriched over commutative monoids in order to be able to interpret sum of proofs and null proofs.
We say that a *-autonomous category $\mathcal{C}$ is enriched over commutative monoids if it is enriched over commutative monoids as a symmetric monoidal category ie. every hom-set $\mathcal{C}[A,B]$ is a commutative monoid and $-\otimes-$ as well as $-;-$ are bilinear over morphisms ie. preserve addition and zero in every variable.
The tricky part is to interpret the exponentials $!,?$. We just need to add enough to interpret $!$, the interpretation of $?$ will follow by the $*$-autonomous structure. We need:
Thus, for every object $A$, we will have that $!A$ is a bimonoid. $!$ will be a comonad. The coderiliction is added on top of this structure.
(…)
(…)
We start from a proof of $!A \vdash B$ and by using as only exponential rules cocontraction and codereliction, we obtain a proof of $!A \vdash A \multimap B$. In the co-Kleisli category we thus go from a morphism $f:A \rightarrow B$, which must be interpreted as a smooth function, to a morphism $df: A \rightarrow (A \multimap B)$. It is the differential of $f$ which associates to every point of $A$ the linear approximation of $f$ around this point.
(…)
Original articles:
Thomas Ehrhard, Laurent Regnier: The differential lambda-calculus, Theor. Comput. Sci. 309 1 (2003) 1–41 (doi:10.1016/S0304-3975(03)00392-X)
Thomas Ehrhard, Laurent Regnier: Differential interaction nets, Theor. Comput. Sci. 364 2 (2006) 166–195 (doi:10.1016/j.tcs.2006.08.003)
Review:
Recent work on categorical semantics:
Last revised on October 27, 2022 at 15:48:58. See the history of this page for a list of all contributions to it.