Differential Linear Logic

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.

Rules of DiLL

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

\frac{
}{
	\vdash ! A
}
\qquad
\frac{
	\vdash \Gamma, !A
  \quad
  \vdash \Delta, !A
}{
	\vdash \Gamma, \Delta, !A
}
\qquad
\frac{
	\vdash \Gamma, A
}{
	\vdash \Gamma, !A
}

In addition to these, there is a way to sum proofs of the same sequent, i.e. a rule of the form

\frac{
	\vdash \Gamma \quad \dots \quad \vdash \Gamma
}{
	\vdash \Gamma
}

When written in a term calculus, this rule says that if s_i : \Gamma then (\sum_{i} s_i) : \Gamma. Of course, this includes the empty sum 0 : \Gamma, which is a proof of any sequent \Gamma. 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 \textsf{DiLL}_0. It is said that promotion is the only rule of DiLL which generates infinitary behaviour.

Relationship to differentiation

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 X \mapsto !X which is meant to model the ! exponential. Codereliction and coweakening can then be interpreted by arrows

	\bar{d}_X : X \to !X
  \qquad
  \bar{c}_X : {!X} \otimes !X \to !X

Now, construct the following morphism:

\bar{\partial}_X =
	{!X} \otimes X
  	\xrightarrow{\textsf{id} \otimes \bar{d}_X}
  !X \otimes !X 
  	\xrightarrow{\bar{c}_X}
  X

We can think of a morphism f : !X \to Y as a "regular" ordinary function: its domain is "replicable", so it can use its argument as many times as needed. Precomposing by \bar{\partial}_X, we get

f \circ \bar{\partial}_X : {!X} \otimes X \to Y

Currying this, we obtain \lambda(f \circ \bar{\partial}_X) : {!X} \to (X \multimap Y). Thus, \lambda(f \circ \bar{\partial}_X) assigns to every input in !X a linear approximation X \multimap Y, 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.

Differential \lambda-calculus

Please expand.

Relationship to concurrency

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 \pi-calculus (i.e. a \pi-calculus without replication) in DiLL, up to bisimulation.

References

• There is an introductory survey on DiLL:

@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}
}

• An encoding of a finitary \pi-calculus in DiLL is investigated in

@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}
}