Linear logic: Difference between revisions

Revision as of 17:30, 5 January 2025

Revision as of 14:42, 26 March 2025

Line 1:

{{Short description|System of resource-aware logic}}

{{use dmy dates|date=Match 2025}}

{{Redirect|⅋|the EP|& (The Moth & The Flame EP){{!}}''&'' (The Moth & The Flame EP)}}

'''Linear logic''' is a [[substructural logic]] proposed by French [[logician]] [[Jean-Yves Girard]] as a refinement of [[classical logic|classical]] and [[intuitionistic logic]], joining the [[Duality (mathematics)#Duality in logic and set theory|dualities]] of the former with many of the [[Constructivism (mathematics)|constructive]] properties of the latter.<ref>{{cite journalsfn|last1=Girard|first1=Jean-Yves|year=1987|title=Linear logic|url=http://girard.perso.math.cnrs.fr/linear.pdf|journal=[[Theoretical Computer Science (journal)|Theoretical Computer Science]]|volume=50|issue=1|pages=1–102|doi=10.1016/0304-3975(87)90045-4|hdl=10338.dmlcz/120513|author1-link=Jean-Yves Girard|doi-access=free}}</ref> Although the logic has also been studied for its own sake, more broadly, ideas from linear logic have been influential in fields such as [[programming languages]], [[game semantics]], and [[quantum physics]] (because linear logic can be seen as the logic of [[quantum information theory]]),<ref>{{cite journalsfn|first1=John|last1=Baez|author1-link=John Baez|first2=Mike|last2=Stay|year=2008|title=Physics, Topology, Logic and Computation: A Rosetta Stone|editor=Bob Coecke|editor-link=Bob Coecke|journal=New Structures of Physics|url=http://math.ucr.edu/home/baez/rosetta.pdf}}</ref> as well as [[linguistics]],<ref>{{cite journalsfn|title=Dagstuhl Seminar 99341 on Linear Logic and Applications|first1=V.|last1=deDe Paiva|author1-link= Valeria de Paiva |first2=J.|last2=vanVan Genabith|first3=E.|last3=Ritter|journal=Drops-Idn/V2/Document/10.4230/Dagsemrep.248 |year=1999|pages=1–21 |publisher=Schloss Dagstuhl – Leibniz-Zentrum für Informatik |doi=10.4230/DagSemRep.248 |doi-access=free |url=http://www.dagstuhl.de/Reports/99/99341.pdf}}</ref> particularly because of its emphasis on resource-boundedness, duality, and interaction.

Linear logic lends itself to many different presentations, explanations, and intuitions.

Line 117 ⟶ 118:

One way of defining linear logic is as a [[sequent calculus]]. We use the letters {{math| Γ}} and {{math| Δ}} to range over lists of propositions {{math|<VAR>A</VAR>₁, ..., <VAR>A</VAR>_''n''}}, also called ''contexts''. A ''sequent'' places a context to the left and the right of the [[turnstile (symbol)|turnstile]], written {{math|Γ {{tee}} Δ}}. Intuitively, the sequent asserts that the conjunction of {{math| Γ}} [[Logical consequence|entails]] the disjunction of {{math| Δ}} (though we mean the "multiplicative" conjunction and disjunction, as explained below). Girard describes classical linear logic using only ''one-sided'' sequents (where the left-hand context is empty), and we follow here that more economical presentation. This is possible because any premises to the left of a turnstile can always be moved to the other side and dualised.

We now give [[Sequent calculus#Inference rules|inference rules]] describing how to build proofs of sequents.<ref>{{sfn|Girard (|1987), |loc=p.22, Def.1.15</ref>}}

First, to formalize the fact that we do not care about the order of propositions inside a context, we add the structural rule of [[exchange rule|exchange]]:

Line 278 ⟶ 279:

===Exponentials===

The exponentials are used to give controlled access to weakening and contraction. Specifically, we add structural rules of weakening and contraction for {{math|?}}'d propositions:<ref>{{sfn|Girard (|1987), |loc=p.25-26, Def.1.21</ref>}}

{| style="margin:auto"

Line 377 ⟶ 378:

|}

Linear distributions are fundamental in the proof theory of linear logic. The consequences of this map were first investigated in <ref>J. [[Robin {{sfn|Cockett]] and Robert |Seely "Weakly distributive categories" [[Journal of Pure and Applied Algebra]] 114(2) 133-173, |1997</ref>}} and called a "weak distribution". In subsequent work it was renamed to "linear distribution" to reflect the fundamental connection to linear logic.

; Other implications :

Line 413 ⟶ 414:

==Encoding classical/intuitionistic logic in linear logic==

Both intuitionistic and classical implication can be recovered from linear implication by inserting exponentials: intuitionistic implication is encoded as {{math|!<VAR>A</VAR> ⊸ <VAR>B</VAR>}}, while classical implication can be encoded as {{math|!?<VAR>A</VAR> ⊸ ?<VAR>B</VAR>}} or {{math|!<VAR>A</VAR> ⊸ ?!<VAR>B</VAR>}} (or a variety of alternative possible translations).<ref>{{sfn|Di Cosmo, Roberto. ''[http://www.dicosmo.org/CourseNotes/LinLog/ The Linear Logic Primer]''. Course notes; chapter 2.</ref>|1996}} The idea is that exponentials allow us to use a formula as many times as we need, which is always possible in classical and intuitionistic logic.

Formally, there exists a translation of formulas of intuitionistic logic to formulas of linear logic in a way that guarantees that the original formula is provable in intuitionistic logic if and only if the translated formula is provable in linear logic. Using the [[Gödel–Gentzen negative translation]], we can thus embed classical [[first-order logic]] into linear first-order logic.

Line 479 ⟶ 480:

==Decidability/complexity of entailment==

The [[entailment]] relation in full CLL is [[Undecidable problem|undecidable]].<ref {{refn|name="Lincoln+92">|For this result and discussion of some of the fragments below, see: {{cite journalharvtxt|first1=Patrick|last1=Lincoln|first2=John|last2=Mitchell|first3=Andre|last3=Scedrov|first4=Natarajan|last4=Shankar|year=1992|title=Decision Problems for Propositional Linear Logic|journal=[[Annals of Pure and Applied Logic]]|volume=56|issue=1–3|pages=239–311|doi=10.1016/0168-0072(92)90075-B|doi-access=free}}</ref> }} When considering fragments of

CLL, the decision problem has varying complexity:

* Multiplicative linear logic (MLL): only the multiplicative connectives. MLL entailment is [[NP-complete]], even restricting to [[Horn clauses]] in the purely implicative fragment,<ref>{{Cite conferencesfn| doi = 10.1109/LICS.1992.185533| conference = Seventh Annual IEEE [[Symposium on Logic in Computer Science]], 1992. LICS '92. Proceedings| pages = 200–210| last = Kanovich| first = Max I.| title = Horn programming in linear logic is NP-complete| book-title = Seventh Annual IEEE Symposium on Logic in Computer Science, 1992. LICS '92. Proceedings| date = 1992-06-22| isbn = 0-8186-2735-2}}</ref> or to atom-free formulas.<ref>{{cite journal|first1=Patricksfn|last1=Lincoln|first2=Timothy|last2=Winkler|year=1994|title=Constant-only multiplicative linear logic is NP-complete|journal=Theoretical Computer Science|volume=135|pages=155–169|doi=10.1016/0304-3975(94)00108-1|doi-access=free}}</ref>

* Multiplicative-additive linear logic (MALL): only multiplicatives and additives (i.e., exponential-free). MALL entailment is [[PSPACE-complete]].<ref name="Lincoln+92" />

* Multiplicative-exponential linear logic (MELL): only multiplicatives and exponentials. By reduction from the reachability problem for [[Petri nets]],<ref>{{Cite tech reportsfn|last1 = Gunter| first1 = C. A.| last2 = Gehlot| first2 = V.| title=Nets as Tensor Theories|institution=University of Pennsylvania|number=MS-CIS-89-68|year = 1989|url=http://seclab.illinois.edu/wp-content/uploads/2011/04/GunterG89.pdf}}</ref> MELL entailment must be at least [[EXPSPACE|EXPSPACE-hard]], although decidability itself has had the status of a longstanding open problem. In 2015, a proof of decidability was published in the journal ''[[Theoretical Computer Science (journal)|Theoretical Computer Science]]'',<ref>{{Cite journalsfn| doi = 10.1016/j.tcs.2015.06.019| issn = 0304-3975| volume = 597| pages = 1–17| last = Bimbó| first = Katalin|author-link= Katalin Bimbó | title = The decidability of the intensional fragment of classical linear logic| journal = Theoretical Computer Science| date = 2015-09-13| doi-access = free}}</ref> but was later shown to be erroneous.<ref>{{Cite journalsfn| doi = 10.1016/j.tcs.2019.02.022| issn = 0304-3975| volume = 768| pages = 91–98| last = Straßburger| first = Lutz| title = On the decision problem for MELL| journal = Theoretical Computer Science| date = 2019-05-10| doi-access = free}}</ref>

* Affine linear logic (that is linear logic with weakening, an extension rather than a fragment) was shown to be decidable, in 1995.<ref>{{Cite conferencesfn| doi = 10.1109/LICS.1995.523283| citeseerx = 10.1.1.23.9226| conference = Tenth Annual IEEE Symposium on Logic in Computer Science, 1995. LICS '95. Proceedings| pages = 496–504| last = Kopylov| first = A. P.| title = Decidability of linear affine logic| book-title = Tenth Annual IEEE Symposium on Logic in Computer Science, 1995. LICS '95. Proceedings| date = 1995-06-01| isbn = 0-8186-7050-9}}</ref>

==Variants==

Line 511:

* [[Proof net]]s

* [[Uniqueness type]]

==Notes==

{{Reflist|2}}

==References==

*{{cite journal|last1=Baez|first1=John|author1-link=John Baez|last2=Stay|first2=Mike|year=2008|title=Physics, Topology, Logic and Computation: A Rosetta Stone|journal=New Structures of Physics|editor=Bob Coecke|editor-link=Bob Coecke|url=http://math.ucr.edu/home/baez/rosetta.pdf}}

*{{Cite journal|last=Bimbó|first=Katalin|author-link=Katalin Bimbó|date=2015-09-13|title=The decidability of the intensional fragment of classical linear logic|journal=Theoretical Computer Science|volume=597|pages=1–17|doi=10.1016/j.tcs.2015.06.019|issn=0304-3975|doi-access=free}}

{{Reflist}}

*{{cite journal|last1=Cockett|first1=J. Robin|author1-link=Robin Cockett|last2=Seely|first2=Robert|year=1997|title=Weakly distributive categories|journal=Journal of Pure and Applied Algebra|volume=114|issue=2|pages=133–173}}

*{{cite book|last=Di Cosmo|first=Roberto|year=1996|title=The Linear Logic Primer|type=Course notes|chapter=2|url=http://www.dicosmo.org/CourseNotes/LinLog/}}

*{{cite journal|last1=De Paiva|first1=V.|author1-link=Valeria de Paiva|last2=Van Genabith|first2=J.|last3=Ritter|first3=E.|year=1999|title=Dagstuhl Seminar 99341 on Linear Logic and Applications|journal=Drops-Idn/V2/Document/10.4230/Dagsemrep.248|pages=1–21|publisher=Schloss Dagstuhl – Leibniz-Zentrum für Informatik|doi=10.4230/DagSemRep.248|doi-access=free|url=http://www.dagstuhl.de/Reports/99/99341.pdf}}

*{{cite journal|last1=Girard|first1=Jean-Yves|author1-link=Jean-Yves Girard|year=1987|title=Linear logic|journal=Theoretical Computer Science|volume=50|issue=1|pages=1–102|doi=10.1016/0304-3975(87)90045-4|hdl=10338.dmlcz/120513|url=https://girard.perso.math.cnrs.fr/linear.pdf|doi-access=free}}

*{{Cite tech report|last1=Gunter|first1=C. A.|last2=Gehlot|first2=V.|year=1989|title=Nets as Tensor Theories|institution=University of Pennsylvania|number=MS-CIS-89-68|url=http://seclab.illinois.edu/wp-content/uploads/2011/04/GunterG89.pdf}}

*{{Cite conference|last=Kanovich|first=Max I.|date=1992-06-22|title=Horn programming in linear logic is NP-complete|conference=Seventh Annual IEEE Symposium on Logic in Computer Science, 1992. LICS '92. Proceedings|book-title=Seventh Annual IEEE Symposium on Logic in Computer Science, 1992. LICS '92. Proceedings|pages=200–210|doi=10.1109/LICS.1992.185533|isbn=0-8186-2735-2}}

*{{Cite conference|last=Kopylov|first=A. P.|date=1995-06-01|title=Decidability of linear affine logic|conference=Tenth Annual IEEE Symposium on Logic in Computer Science, 1995. LICS '95. Proceedings|book-title=Tenth Annual IEEE Symposium on Logic in Computer Science, 1995. LICS '95. Proceedings|pages=496–504|doi=10.1109/LICS.1995.523283|citeseerx=10.1.1.23.9226|isbn=0-8186-7050-9}}

*{{cite journal|last1=Lincoln|first1=Patrick|last2=Mitchell|first2=John|last3=Scedrov|first3=Andre|last4=Shankar|first4=Natarajan|year=1992|title=Decision Problems for Propositional Linear Logic|journal=Annals of Pure and Applied Logic|volume=56|issue=1–3|pages=239–311|doi=10.1016/0168-0072(92)90075-B|doi-access=free}}

*{{cite journal|last1=Lincoln|first1=Patrick|last2=Winkler|first2=Timothy|year=1994|title=Constant-only multiplicative linear logic is NP-complete|journal=Theoretical Computer Science|volume=135|pages=155–169|doi=10.1016/0304-3975(94)00108-1|doi-access=free}}

*{{Cite journal|last=Straßburger|first=Lutz|date=2019-05-10|title=On the decision problem for MELL|journal=Theoretical Computer Science|volume=768|pages=91–98|doi=10.1016/j.tcs.2019.02.022|issn=0304-3975|doi-access=free}}

==Further reading==

* {{cite web |title=Introduction to Linear Logic |last=Brauner| first=Torben|url=http://www.brics.dk/LS/96/6/BRICS-LS-96-6.pdf }}

* {{cite book |last1=Di Cosmo |first1=Roberto |last2=Danos |first2=Vincent |year=1992|title=The Linear Logic Primer |url=https://www.dicosmo.org/CourseNotes/LinLog/ }}

*{{cite SEP|title=Linear Logic|url-id=logic-linear|date=2023-09-16|edition=Fall 2023|author-last=Di Cosmo|author-first=Roberto|author-last2=Miller|author-first2=Dale |author-link2=Dale Miller (academic)}}

* {{cite book |last1=Girard, |first1=Jean-Yves, |last2=Lafont, |first2=Yves, and |last3=Taylor, |first3=Paul. |year=1989 ''[|title=Proofs and Types |publisher=Cambridge University Press |url=https://web.archive.org/web/20160704202340/http://www.cs.man.ac.uk/~pt/stable/Proofs+Types.html Proofs and Types]''. Cambridge Press, 1989.}}

* {{cite book |last=Hoare, |first=C. A. R., |year=1985. ''|title=Communicating Sequential Processes''. |publisher=Prentice-Hall International. {{|isbn|=0-13-153271-5 }}

*{{cite conference | last = Lafont, | first = Yves, | year = 1993. | title = ''Introduction to Linear Logic''. | Lecturebook-title notes from= TEMPUS Summer School on ''Algebraic and Categorical Methods in Computer Science'', | ___location = Brno, Czech Republic. | type = Lecture notes}}

* {{cite book|last=Miller |first=Dale |year=2004 |chapter=Overview of Linear Logic Programming |title=Linear Logic in Computer Science |editor1-last=Ehrhard |editor2-last=Girard |editor3-last=Ruet |editor4-last=Scott |publisher=Cambridge University Press |series=London Mathematical Society Lecture Notes |volume=316 |url=http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/llp.pdf }}

* {{cite web |title=Introduction to Linear Logic |last=Lincoln |first=Patrick|url=http://www.csl.sri.com/~lincoln/papers/sigact92.ps |format=Postscript }}

* {{cite web |title=Linear Logic Wiki |url=http://llwiki.ens-lyon.fr/ }}

* {{cite book |last=Troelstra |first=A. S. |year=1992 |title=Lectures on Linear Logic |series=CSLI Lecture Notes |volume=29 |publisher=Stanford }}

* [[{{cite book |last1=Troelstra |first1=A. S. Troelstra]],|last2=Schwichtenberg |first2=H. Schwichtenberg (|year=1996). ''|title=Basic Proof Theory''. In |series ''=Cambridge Tracts in Theoretical Computer Science'', |publisher=Cambridge University Press, {{|isbn|=0-521-77911-1 }}.

* {{cite web |title=A Taste of Linear Logic |last=Wadler| first=Philip|url=http://homepages.inf.ed.ac.uk/wadler/topics/linear-logic.html }}

* Girard, Jean-Yves. ''[http://girard.perso.math.cnrs.fr/linear.pdf Linear logic]'', Theoretical Computer Science, Vol 50, no 1, pp.&nbsp;1–102, 1987.

* Girard, Jean-Yves, Lafont, Yves, and Taylor, Paul. ''[https://web.archive.org/web/20160704202340/http://www.cs.man.ac.uk/~pt/stable/Proofs+Types.html Proofs and Types]''. Cambridge Press, 1989.

* Hoare, C. A. R., 1985. ''Communicating Sequential Processes''. Prentice-Hall International. {{isbn|0-13-153271-5}}

* Lafont, Yves, 1993. ''Introduction to Linear Logic''. Lecture notes from TEMPUS Summer School on ''Algebraic and Categorical Methods in Computer Science'', Brno, Czech Republic.

* [[A. S. Troelstra|Troelstra, A.S.]] ''Lectures on Linear Logic''. CSLI (Center for the Study of Language and Information) Lecture Notes No. 29. Stanford, 1992.

* [[A. S. Troelstra]], H. Schwichtenberg (1996). ''Basic Proof Theory''. In series ''Cambridge Tracts in Theoretical Computer Science'', Cambridge University Press, {{isbn|0-521-77911-1}}.

* Di Cosmo, Roberto, and Danos, Vincent. ''[http://www.dicosmo.org/CourseNotes/LinLog/ The linear logic primer]''.

* [http://www.csl.sri.com/~lincoln/papers/sigact92.ps Introduction to Linear Logic] (Postscript) by [http://www.csl.sri.com/users/lincoln/ Patrick Lincoln]

* [http://www.brics.dk/LS/96/6/BRICS-LS-96-6.pdf Introduction to Linear Logic] by Torben Brauner

* [http://homepages.inf.ed.ac.uk/wadler/topics/linear-logic.html A taste of linear logic] by Philip Wadler

* [http://plato.stanford.edu/entries/logic-linear/ Linear Logic] by [https://web.archive.org/web/20060925141642/http://www.pps.jussieu.fr/~dicosmo/index.html.en Roberto Di Cosmo] and [http://www.lix.polytechnique.fr/Labo/Dale.Miller/ Dale Miller]. The Stanford Encyclopedia of Philosophy (Fall 2006 Edition), Edward N. Zalta (ed.).

* [http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/llp.pdf Overview of linear logic programming] by [http://www.lix.polytechnique.fr/Labo/Dale.Miller/ Dale Miller]. In ''Linear Logic in Computer Science'', edited by Ehrhard, Girard, Ruet, and Scott. Cambridge University Press. London Mathematical Society Lecture Notes, Volume 316, 2004.

* [http://llwiki.ens-lyon.fr/ Linear Logic Wiki]

==External links==