Content deleted Content added
No edit summary |
No edit summary |
||
Line 1:
{{Short description|System of resource-aware logic}}
{{Redirect|⅋|the EP|& (The Moth & The Flame EP){{!}}''&'' (The Moth & The Flame EP)}}
'''Linear logic''' is a [[substructural logic]] proposed by [[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 journal|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 journal|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 book|title=Dagstuhl Seminar 99341 on Linear Logic and Applications|first1=V.|last1=de Paiva|author1-link= Valeria de Paiva |first2=J.|last2=van Genabith|first3=E.|last3=Ritter|year=1999|pages=1–21 |doi=10.4230/DagSemRep.248 |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 115:
==Sequent calculus presentation==
One way of defining linear logic is as a [[sequent calculus]]. We use the letters {{math| Γ}} and {{math| Δ}} to range over
We now give [[Sequent calculus#Inference rules|inference rules]] describing how to build proofs of sequents.<ref>Girard (1987), p.22, Def.1.15</ref>
Line 328:
|}
One might observe that the rules for the exponentials follow a different pattern from the rules for the other connectives, resembling the inference rules governing modalities in sequent calculus formalisations of the [[normal modal logic]] [[S4 (modal logic)|S4]], and that there is no longer such a clear symmetry between the duals ! and ?.
This situation is remedied in alternative presentations of CLL (e.g., the [[Logic of unity|LU]] presentation).
Line 377:
|}
Linear distributions are fundamental in the proof theory of linear logic. The consequences of this map were first investigated in <ref>J. [[Robin 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 415:
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>Di Cosmo, Roberto. ''[http://www.dicosmo.org/CourseNotes/LinLog/ The Linear Logic Primer]''. Course notes; chapter 2.</ref> 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.
==The resource interpretation==
Line 479:
==Decidability/complexity of entailment==
The [[entailment]] relation in full CLL is [[Undecidable problem|undecidable]].<ref name="Lincoln+92">For this result and discussion of some of the fragments below, see: {{cite journal|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 conference| 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=Patrick|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 conference| conference = Tenth International Conference on Application and Theory of Petri Nets. Proceedings| pages = 174–191| last1 = Gunter| first1 = C. A.| last2 = Gehlot| first2 = V.| year = 1989}}</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)|
* Affine linear logic (that is linear logic with weakening, an extension rather than a fragment) was shown to be decidable, in 1995.<ref>{{Cite conference| 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>
| |||