Differential Linear Logic (sometimes called DiLL) is a system that extends classical Linear Logic with three additional rules for , as well as formal sums of proofs.
In addition to the usual rules for the exponentials, differential linear logic comes with coweakening, cocontraction and codereliction rules for . Rendered in one-sided sequent syntax, the rules take the form
In addition to these, there is a way to sum proofs of the same sequent, i.e. a rule of the form
When written in a term calculus, this rule says that if then . Of course, this includes the empty sum , which is a proof of any sequent . This has a slightly paraconsistent feel to it, but it shouldn't be interpreted that way. Instead, this logic is inherently a partial logic (unlike CLL), and not all proofs are "fully defined" objects. In fact, the empty sum is the least defined proof of a sequent.
The fragment without the promotion rule of classical linear logic is sometimes called . It is said that promotion is the only rule of DiLL which generates infinitary behaviour.
The relationship to the differential calculus is perhaps better seen in terms of the categorical semantics of DiLL.
Suppose we are in a symmetric monoidal closed category (sometimes also known as an autonomous category). Suppose we have a map on objects which is meant to model the exponential. Codereliction and coweakening can then be interpreted by arrows
Now, construct the following morphism:
We can think of a morphism as a "regular" ordinary function: its domain is "replicable", so it can use its argument as many times as needed. Precomposing by , we get
Currying this, we obtain . Thus, assigns to every input in a linear approximation , which can be thought of as the derivative at that point of the input. Indeed, in some models of DiLL this coincides with the derivative.
Please expand.
Because of the close relationship between DiLL, partiality, nondeterminism etc., it is believed and/or conjectured that DiLL has a close relationship with concurrency.
This argument has been corroborated by [Ehrhard and Laurent 2010], who encode a finitary -calculus (i.e. a -calculus without replication) in DiLL, up to bisimulation.
Ehrhard, Thomas. 2018. ‘An Introduction to Differential Linear Logic: Proof-Nets, Models and Antiderivatives’. Mathematical Structures in Computer Science 28 (7): 995–1060. https://doi.org/10.1017/S0960129516000372. [arXiv]
@article{ehrhard_2018,
title = {An introduction to differential linear logic: proof-nets, models and antiderivatives},
volume = {28},
issn = {0960-1295, 1469-8072},
shorttitle = {An introduction to differential linear logic},
doi = {10.1017/S0960129516000372},
number = {7},
journal = {Mathematical Structures in Computer Science},
author = {Ehrhard, Thomas},
month = aug,
year = {2018},
pages = {995--1060}
}
Ehrhard, Thomas, and Olivier Laurent. 2010. ‘Interpreting a Finitary Pi-Calculus in Differential Interaction Nets’. Information and Computation 208 (6): 606–33. https://doi.org/10.1016/j.ic.2009.06.005.
@article{ehrhard_2010,
title = {Interpreting a finitary pi-calculus in differential interaction nets},
volume = {208},
issn = {08905401},
doi = {10.1016/j.ic.2009.06.005}
number = {6},
journal = {Information and Computation},
author = {Ehrhard, Thomas and Laurent, Olivier},
year = {2010},
pages = {606--633}
}