Linear Logic

Linear logic (LL) is a constructive substructural logic introduced by Jean-Yves Girard in the late 1980s Girard 1987.

The key idea in linear logic is that each assumption in a proof should be used exactly once: no more (no copying), but no less (no deleting).

The imposition of this limitation gives to linear logic a very particular flavour:

• conjunction splits into additive conjuction & ("with") and multiplicative conjuction \otimes ("tensor")
• disjunction splits into additive disjunction \oplus ("or") and multiplicative disjunction ⅋ ("par")

Sequent calculus

Linear logic can be defined in Gentzen's sequent logic. A sequent is an assertion conditioned on propositions (ranged over A, B, and so on) and takes the form:

A_1, A_2, ..., A_n \vdash B_1, B_2, ..., B_m

The propositions on the left hand side (LHS) of the turnstile (\vdash) are unordered and may contain multiple copies of the same proposition. Likewise, for the right hand side (RHS). The RHS may also be restricted so that it contains exactly one proposition, as is the case for intuitionistic linear logic (ILL).

A sequent is the syntactic structure that the inference rules of linear logic, defined below for classical linear logic (CLL), are applied to in order to build proofs.

Propositions on the LHS of the turnstile can be thought of as the assumptions of the assertion and those on the RHS of the turnstile are the conclusion.

Connectives and fragments

The dual of a proposition is denoted by (-)^\bot. For instance, P^\bot is the dual of P and it can be thought of as the negation of P.

Every proposition has a dual:

\top, \bot, 1, and 0 are called the units for the multiplicative and additive connectives and they are explained in the rules for CLL below.

There are (at least) two axes along which we can group the connectives of linear logic: positive vs negative ("polarity"), or multiplicative vs additive vs exponential vs quantifiers. This gives us a table as follows:

The table above is furthermore laid out such that side-by-side connectives are de Morgan dual; for example, (P \oplus P')^\bot \cong P^\bot \mathbin{\&} P'^\bot.

Please expand: MELL, IMELL, MEALL, FILL, CLL.

Rules of Classical Linear Logic

The inference rules for the connectives in classical linear logic (CLL) are divided into left and right rules. In left (right) rules, the formula containing the connective is on the LHS (RHS) of the sequent. The inference rules for connectives shown below are only for multiplicative and additive connectives-exponential and quantifier connectives are omitted.

Please expand: add rules for exponentials & quantifiers

Additive Rules

\begin{darray}{}
	\frac{\Gamma, \tau_1 \vdash \Delta}{\Gamma, \tau_1 \mathbin{\&} \tau_2 \vdash \Delta}\mathbf{\mathbin{\&}-L_1} && \frac{\Gamma, \tau_2 \vdash \Delta}{\Gamma, \tau_1 \mathbin{\&} \tau_2 \vdash \Delta}\mathbf{\mathbin{\&}-L_2} \\\\
  & \frac{\Gamma \vdash \tau_1, \Delta \;\;\;\; \Gamma \vdash \tau_2, \Delta}{\Gamma \vdash \tau_1 \mathbin{\&} \tau_2,  \Delta}\mathbf{\mathbin{\&}-R} \\\\
  & \frac{\Gamma, \tau_1 \vdash \Delta \;\;\;\; \Gamma, \tau_2 \vdash \Delta}{\Gamma, \tau_1 \oplus \tau_2 \vdash \Delta}\mathbf{\oplus-L} \\\\
  \frac{\Gamma \vdash \tau_1, \Delta}{\Gamma \vdash \tau_1 \oplus \tau_2, \Delta}\mathbf{\oplus-R_1} && \frac{\Gamma \vdash \tau_2, \Delta}{\Gamma \vdash \tau_1 \oplus \tau_2, \Delta}\mathbf{\oplus-R_2}
\end{darray}

Multiplicative Rules

\begin{darray}{}
	  \frac{\Gamma, \tau_1, \tau_2 \vdash \Delta}{\Gamma, \tau_1 \otimes \tau_2 \vdash \Delta}\mathbf{\otimes-L} && \frac{\Gamma_1 \vdash \tau_1, \Delta_1 \;\;\;\; \Gamma_2 \vdash \tau_2, \Delta_2}{\Gamma_1, \Gamma_2 \vdash \tau_1 \otimes \tau_2, \Delta_1, \Delta_2}\mathbf{\otimes-R} \\\\
    \frac{\Gamma_1, \tau_1 \vdash \Delta_1 \;\;\;\; \Gamma_2, \tau_2 \vdash \Delta_2}{\Delta_1, \Delta_2, \tau_1 \mathbin{⅋} \tau_2 \vdash \Delta_1, \Delta_2}\mathbf{\mathbin{⅋}-L} && \frac{\Gamma \vdash \tau_1, \tau_2, \Delta}{\Gamma \vdash \tau_1 \mathbin{⅋} \tau_2, \Delta}\mathbf{⅋-R}
\end{darray}

Nullary Constants

Each of the additive and multiplicative connectives have a corresponding nullary constant, which we refer to as unit. 1 is the unit for \otimes, 0 is the unit for \oplus, \bot is the unit for \mathbin{⅋}, and \top is the unit for \mathbin{\&}. The inference rules for each unit is shown below.

\begin{darray}{}
	\textbf{No left rules for $\top$} && \frac{}{\Gamma \vdash \top, \Delta}\mathbf{\top-R} \\\\
  \frac{\Gamma \vdash \Delta}{\Gamma, 1 \vdash \Delta}\mathbf{1-L} && \frac{}{\cdot \vdash 1}\mathbf{1-R} \\\\
  \frac{}{\Gamma, 0 \vdash \Delta}\mathbf{0-L} && \textbf{No right rules for 0} \\\\
  \frac{}{\bot \vdash \cdot}\mathbf{\bot-L} && \frac{\Gamma \vdash \Delta}{\Gamma \vdash \bot, \Delta}\mathbf{\bot-R}
\end{darray}

Structural Rules

The following are the structural rules for CLL: the axiom rule and the cut rule.

\begin{darray}{}
	\frac{}{\tau \vdash \tau}\mathbf{Ax} \\\\
  \frac{\Gamma \vdash \tau, \Delta \;\;\;\; \Delta', \tau \vdash \Delta'}{\Gamma, \Gamma' \vdash \Delta, \Delta'}\mathbf{Cut}
\end{darray}

Note that the (left- and right-) weakening and contraction rules are not admissible from any of the rules given above. That is, propositions may not be arbitrarily removed from or added to a sequent. Furthermore, if a judgement is provable, adding or removing any propositions from either the LHS or the RHS results in a judgement that is no longer provable. Intuitively, this means that propositions are treated as precious resources-they should not be dropped and they should not appear from nowhere.

Intuitionistic vs. Classical Linear Logic

When defined using sequents, intuitionistic linear logic (ILL) and classical linear logic (CLL) differ in the structure of the sequent used. In ILL, the RHS of the sequent contains exactly one proposition. In CLL, the RHS of the sequent contains 0 or more propositions.

This means that the Law of the Excluded Middle (LEM) is admissible in CLL, but not in ILL. For example, consider the Axiom rule in CLL:

\frac{}{P \vdash P}

The proposition P on the LHS can be moved to the RHS by dualizing it, resulting in:

\frac{}{\vdash P^\bot, P}

Finally, we may apply the \mathbin{⅋}-R rule to obtain the LEM:

\frac{}{\vdash P^\bot \mathbin{⅋} P}

Note that this cannot be done in ILL since the RHS is allowed to contain only one proposition.

However, the following is not provable in both ILL and CLL:

\vdash P^\bot \oplus P

This can be read as requiring evidence of either P^\bot or P, which is undecidable.

Computational interpretation

A Curry-Howard correspondence, i.e., a correspondence between logic and computation, has been established between linear logic and functional languages. This results in an interpretation of the terms in these languages as resources that are consumed.

Please expand: connection b/t LL and linear \lambda-calc

The connection between linear logic and session types has been explored by several works, including Caires and Pfenning 2010, Wadler 2012, and Carbone et al. 2016. Essentially, these works define a session-typed language of communicating processes and show that a correspondence exists between the inference rules of linear logic and the semantic rules of the language.

Caires and Pfenning proposed such a Curry-Howard correspondence where propositions are interpreted as (binary) session types, proofs as processes, and cut elimination as communication Caires and Pfenning 2010. This led to the development of the binary session-typed language \piDILL and a Curry-Howard correspondence between the language and ILL DeYoung et al. 2012. Inspired by \piDILL, Wadler developed the language CL based on CLL and established a Curry-Howard correspondence between the two Wadler 2012.

Carbone et al. also establish a Curry-Howard correspondence between a multiparty session-typed language called MCP and CLL Carbone et al. 2016.

Please expand: connection b/t LL and session types

Strong normalization

The original 1987 presentation failed to provide a complete proof of strong normalization of cut elimination, as Girard left a crucial lemma unproven.

In his PhD thesis Vincent Danos provided a proof of strong normalization for MELL. This was followed by work by many other people.

The first proof of strong normalization for full second-order CLL, due to Michele Pagani and Lorenzo Tortora de Falco, appeared in 2010:

@article{pagani_2010,
	title = {Strong normalization property for second order linear logic},
	volume = {411},
	issn = {03043975},
	doi = {10.1016/j.tcs.2009.07.053},
	language = {en},
	number = {2},
	urldate = {2020-09-30},
	journal = {Theoretical Computer Science},
	author = {Pagani, Michele and Tortora de Falco, Lorenzo},
	month = jan,
	year = {2010},
	pages = {410--444}
}

Another proof of normalization for second-order CLL, which does not require confluence, is given by Beniamino Accattoli (best paper at RTA 2013, slides from the talk).

@InProceedings{accattoli:LIPIcs:2013:4051,
  author =	{Beniamino Accattoli},
  title =	{{Linear Logic and Strong Normalization}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{39--54},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{Femke van Raamsdonk},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4051},
  URN =		{urn:nbn:de:0030-drops-40515},
  doi =		{10.4230/LIPIcs.RTA.2013.39},
  annote =	{Keywords: linear logic, proof nets, strong normalization, explicit substitutions}
}

Proof-irrelevant models of linear logic

Please expand: phase semantics.

Proof-relevant models of linear logic

There are many models of the proof theory of linear logic, most of which are organised through the device of categorical semantics. The categorical semantics of (intuitionistic) linear logic is surveyed in great detail by Melliès 2009.

The models include the following:

• The relational model of Linear Logic
• Coherent spaces
• The vector space models of Linear Logic

Please expand.

See also

• Propositions-as-sessions
• Classical Processes
• Recorded lecture on Linear Logic by Paul Downen at OPLSS

References

• A handy reference for all matters related to LL is Yves Lafont's Linear Logic Pages.

• The first treatment of linear logic took up an entire issue of TCS. It was also not peer-reviewed, due to the novelty of the material:

@article{girard_linear_1987,
	title = {Linear logic},
	volume = {50},
	issn = {03043975},
	doi = {10.1016/0304-3975(87)90045-4},
	abstract = {The familiar connective of negation is broken into two operations: linear negation which is the purely negative part of negation and the modality "of course" which has the meaning of reaffirmation. Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.},
	number = {1},
	journal = {Theoretical Computer Science},
	author = {Girard, Jean-Yves},
	year = {1987},
	pages = {1--101}

• (Self-)reviews include:

@incollection{girard_linear_1995,
	address = {Cambridge},
	title = {Linear {Logic}: its syntax and semantics},
	volume = {50},
	isbn = {0-521-55961-8},
	number = {2},
	booktitle = {Advances in {Linear} {Logic}},
	publisher = {Cambridge University Press},
	author = {Girard, J.-Y.},
	editor = {Girard, Jean-Yves and Lafont, Yves and Regnier, Laurent},
	year = {1995},
	doi = {10.1017/CBO9780511629150.002},
	pages = {1--42}
}

• See the nLab page on Linear Logic, which currently contains much more material, as well as descriptions of its categorical semantics.

• There is a separate wiki on Linear Logic, the LLWiki.

• The categorical semantics of (intuitionistic) Linear Logic is covered in great detail in

@incollection{mellies_2009,
	title = {Categorical {Semantics} of {Linear} {Logic}},
	isbn = {978-2-85629-273-0},
	url = {http://www.pps.univ-paris-diderot.fr/~mellies/papers/panorama.pdf},
	booktitle = {Panoramas et synthèses 27: {Interactive} models of computation and program behaviour},
	publisher = {Société Mathématique de France},
	author = {Melliès, Paul-André},
	editor = {Curien, Pierre-Louis and Herbelin, Hugo and Krivine, Jean-Louis and Melliès, Paul-André},
	year = {2009}
}

@inproceedings{inproceedings,
author = {Caires, Luís and Pfenning, Frank},
year = {2010},
month = {08},
pages = {222-236},
title = {Session Types as Intuitionistic Linear Propositions},
isbn = {978-3-642-15374-7},
doi = {10.1007/978-3-642-15375-4_16}
}

@article{article,
author = {Deyoung, Henry and Caires, Luís and Pfenning, Frank and Toninho, Bernardo},
year = {2012},
month = {05},
pages = {},
title = {Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication},
volume = {16},
journal = {Leibniz International Proceedings in Informatics, LIPIcs},
doi = {10.4230/LIPIcs.CSL.2012.228}
}

@article{WADLER_2014, title={Propositions as sessions}, volume={24}, DOI={10.1017/S095679681400001X}, number={2–3}, journal={Journal of Functional Programming}, author={WADLER, PHILIP}, year={2014}, pages={384–418}}

@article{10.1007/s00236-016-0285-y,
author = {Carbone, Marco and Montesi, Fabrizio and Sch\"{u}rmann, Carsten and Yoshida, Nobuko},
title = {Multiparty session types as coherence proofs},
year = {2017},
issue_date = {May       2017},
publisher = {Springer-Verlag},
address = {Berlin, Heidelberg},
volume = {54},
number = {3},
issn = {0001-5903},
url = {https://doi.org/10.1007/s00236-016-0285-y},
doi = {10.1007/s00236-016-0285-y},
abstract = {We propose a Curry---Howard correspondence between a language for programming multiparty sessions and a generalisation of Classical Linear Logic (CLL). In this framework, propositions correspond to the local behaviour of a participant in a multiparty session type, proofs to processes, and proof normalisation to executing communications. Our key contribution is generalising duality, from CLL, to a new notion of n-ary compatibility, called coherence. Building on coherence as a principle of compositionality, we generalise the cut rule of CLL to a new rule for composing many processes communicating in a multiparty session. We prove the soundness of our model by showing the admissibility of our new rule, which entails deadlock-freedom via our correspondence.},
journal = {Acta Inf.},
month = {may},
pages = {243–269},
numpages = {27}
}