Linear logic 579675 223201914 2008-07-03T01:00:04Z Jamelan 3529454 /* External links */ +ja [[fr:Logique linéaire]] In [[mathematical logic]], '''linear logic''' is a type of [[substructural logic]] that denies the [[structural rule]]s of ''weakening'' and ''contraction''. The interpretation is of ''hypotheses as resources'': every hypothesis must be consumed ''exactly once'' in a [[Mathematical proof|proof]]. This differs from usual logics such as [[classical logic|classical]] or [[intuitionistic logic]] where the governing judgement is of ''truth'', which may be freely used as many times as necessary. To give an example, from [[proposition]]s ''A'' and ''A'' ⇒ ''B'' one may conclude ''A'' ∧ ''B'' as follows: # [[Modus ponens]] (or implication [[elimination rule|elimination]]) on the assumptions ''A'' and ''A'' ⇒ ''B'' to conclude ''B''. # Conjunction of the assumption ''A'' and (1) to conclude ''A'' ∧ ''B''. This is often symbolically represented as a [[sequent]]: ''A'', ''A'' ⇒ ''B'' {{Unicode|⊢}} ''A'' ∧ ''B''. Both lines in the above proof "consume" the fact that ''A'' is true; this "''freeness''" of truth is usually what is desired in formal mathematics. However, truth is often too abstract or unwieldy when applied to statements about the world. For example, suppose one has a quart of [[cream]] from which one can make a pound of [[butter]]. If the cream is used to make butter, then it cannot be concluded that one has both cream and butter. Yet, the logical schema outlined above leads one to conclude that <tt>cream</tt>, <tt>cream</tt> ⇒ <tt>butter</tt> {{Unicode|⊢}} <tt>cream</tt> ∧ <tt>butter</tt> (here, <tt>cream</tt> stands for the proposition "I have a quart of cream", and <tt>butter</tt> stands for "I have a pound of butter"). The failure of ordinary logic to accurately model this activity is due to the nature of cream, butter, and ''resources'' in general: the quantity of resources is not a free fact to be used or disposed at will, like truth, but rather must be carefully accounted in every "''state change''". The accurate statement about making butter is: : From a quart of cream and a process to convert a quart of cream into a pound of butter, one may obtain a pound of butter. In linear logic this is written: <tt>cream</tt>, <tt>cream</tt> {{Unicode|⊸}} <tt>butter</tt> {{Unicode|⊩}} <tt>butter</tt>, using different connectives ({{Unicode|⊸}} instead of ⇒) and a different notion of logical entailment ({{Unicode|⊩}} instead of {{Unicode|⊢}}). Linear logic was proposed by the French [[logician]] [[Jean-Yves Girard]] in 1987. == Linear connectives == The [[logical connective]]s are re-examined in this resource-interpretation; each connective splits into ''multiplicative'' and ''additive'' versions, which correspond to ''simultaneous'' and ''alternative'' presence, respectively. To motivate the connectives, let us use the example of a [[vending machine]]. '''Multiplicative conjunction''', also called ''tensor'' or ''times'' (written {{Unicode|⊗}}), denotes simultaneous occurrence of resources, to be used as you (the consumer) direct. For example, if you buy a stick of gum and a bottle of soft drink, then you are requesting <tt>gum</tt> {{Unicode|⊗}} <tt>drink</tt>. It is up to you in which order they appear; in fact, in principle you even have the option to mix them up. That doesn't really amount to anything when the conjuncts are atomic; but in, for example, (<tt>gum</tt> {{Unicode|⊗}} <tt>drink</tt>) {{Unicode|⊗}} <tt>candy</tt>, you have the power to choose the gum first, then the candy bar, and finally the drink. Indeed, {{Unicode|⊗}} is an [[associative]] and [[commutative]] operation, so this is equivalent to <tt>gum</tt> {{Unicode|⊗}} (<tt>candy</tt> {{Unicode|⊗}} <tt>drink</tt>). The constant 1 is used to denote the absence of any resource; it functions as a [[identity element|unit]] of tensor: ''A'' {{Unicode|⊗}} 1 ≡ 1 {{Unicode|⊗}} ''A'' ≡ ''A''. '''Additive conjunction''', also called ''with'' (written &amp;) represents alternative occurrence of resources, the choice of which you control. If in the vending machine there is a packet of chips, a candy bar, and a can of soft drink, all worth the same price, then for that price you can get exactly one of these products. After the purchase, you will have <tt>candy</tt> & <tt>chips</tt> & <tt>drink</tt>, ''i.e.'', exactly one of the conjuncts. You cannot use {{Unicode|⊗}} for this outcome, because you cannot get all of these items ''simultaneously'' for the price of one. This operation is also both associative and commutative. Additive conjunction has a unit ''top'' (written {{Unicode|⊤}}, with ''A'' & {{Unicode|⊤}} ≡ {{Unicode|⊤}} & ''A'' ≡ ''A''); it represents a lack of alternative or an inability to choose. It is often used when the exact accounting of resources is burdensome or impossible. For example, if you don't actually care what you get from the machine, or indeed whether you get anything at all, then the outcome may be expressed as {{Unicode|⊤}}. This unit can be used together with {{Unicode|⊗}} to define a ''minimal'' composition of resources: if you want a candy bar at least, but possibly something else also, then the desired outcome is <tt>candy</tt> {{Unicode|⊗}} {{Unicode|⊤}}. '''Multiplicative disjunction''', also called ''par'' or ''parallelisation'' (written {{Unicode|⅋}}, an upside-down [[ampersand]]) represents simultaneous occurrence of resources, to be used as the machine (the producer) directs. If there is a single button which, when pushed, will dispense both a stick of gum and a bottle of soft drink, then this may be represented as <tt>gum</tt> {{Unicode|⅋}} <tt>drink</tt>. The difference between this and the multiplicative conjunction <tt>gum</tt> {{Unicode|⊗}} <tt>drink</tt> is that now the machine chooses in what order they will be dispensed. For gum and a drink, this probably does not matter. However, for a coffee vending machine that dispenses both the coffee and the coffee cup, <tt>cup</tt> {{Unicode|⅋}} <tt>coffee</tt> and <tt>cup</tt> {{Unicode|⊗}} <tt>coffee</tt> are very different machines. As with the conjunctions, par is associative and commutative. Its unit is ''bottom'' (written ⊥), which stands for the empty goal: imagine pushing the "coin return" lever without inserting any money. '''Additive disjunction''', also called ''plus'' (written ⊕) represents alternative occurrence of resources, the choice of which the machine controls. For example, suppose the vending machine permits gambling (''i.e.'', "insert a dollar and win a candy bar, a soft drink, or an all-expenses-paid vacation"). Then the outcome of the purchase is <tt>candy</tt> ⊕ <tt>drink</tt> ⊕ <tt>vacation</tt>. You know that one of the choices will be produced, but you have no control over the result; indeed, it's consistent with this description that the machine might ''never'' produce a vacation. Note the difference from additive conjunction: if you have <tt>candy</tt> & <tt>drink</tt> & <tt>vacation</tt>, then you have the power to choose the vacation if you wish. Once again, this operation is associative and commutative. Its unit is the constant 0, which represents a lack of outcome, catastrophic failure, or inability of the machine to comply with its programming. '''Linear implication'''. The conjunctions and disjunctions above define the state of the world, but the description is static. For state change, linear logic defines the connective of ''linear implication'' (written {{Unicode|⊸}}), sometimes also known as ''entails'', ''multimap'', or ''lolli'' because of its lollipop-like shape. As a resource, ''A'' {{Unicode|⊸}} ''B'' means a method to consume resource ''A'' to achieve resource ''B''. If the machine is a [[penny smasher]], then its ability to smash a coin can be described as <tt>penny</tt> {{Unicode|⊸}} <tt>smashed penny</tt>. Note that the implication itself is a resource that must obey the principle of single consumption. '''Exponential connectives'''. The collection of connectives so far are excellent for describing states and transitions, but they are too weak if one needs the usual notion of ''truth''. This is obviously very desirable because a discussion about the actual world should not preclude standard mathematical reasoning. Linear logic uses an idea from [[modal logic]] to embed the usual logic by means of a pair of exponential operators. * Re-use or copying is allowed for propositions using the "''of course''" exponential operator (written !). Logically, two occurrences of !''A'' as hypotheses may be contracted into a single occurrence. This is related to the conjunctions in that the consumer or user has the power to decide how often ''A'' will appear. * The collection of goals is allowed to be extended with propositions using the "''why not''" operator (written ?). Logically, any fact can be weakened by including an additional conclusion ?''A''. This is related to the disjunctions in that the producer or machine has the power to decide how often ''A'' will appear. Under the resource interpretation, ! encodes ''arbitrary production'' and ? encodes ''arbitrary consumption''. An actual vending machine could be specified as a complicated combination of the above connectives, describing all the allowed behaviours of the machine. == Flavours of linear logic == Linear logic has many restrictions and variants. The primary axis of variation is along the [[classical logic|classical]]/[[intuitionistic logic|intuitionistic]] divide. ''Classical linear logic'' (CLL) is the original linear logic as proposed by Girard. In CLL every connective has a [[dual]]. The following is a two-sided presentation of CLL as a [[sequent calculus]]: <center>[[Image:Sequent_calculus_for_classical_linear_logic.png]]</center> Any proof can be transformed into one that [[Cut-elimination theorem|doesn't use the cut rule]]. ''Linear implication'' is not included in this table, but it is definable in CLL using linear negation and multiplicative disjunction: ''A'' {{Unicode|⊸}} ''B'' ≡ ''A''<sup>⊥</sup> {{Unicode|⅋}} ''B''. This is familiar from other classical logics: for example, the usual implication ⇒ is similarly definable: ''A'' ⇒ ''B'' ≡ ?''A''<sup>⊥</sup> {{Unicode|⅋}} ''B''. Such definitions of course require a notion of ''linear negation'', but in classical logic one can use [[dual (math)|dual]]s: the dual of ''A'', written ''A''<sup>⊥</sup> is defined as follows. {| style="margin-left: 2em" | (''A'' {{Unicode|⊗}} ''B'')<sup>⊥</sup> || = || ''A''<sup>⊥</sup> {{Unicode|⅋}} ''B''<sup>⊥</sup> |- | (''A'' & ''B'')<sup>⊥</sup> || = || ''A''<sup>⊥</sup> ⊕ ''B''<sup>⊥</sup> |- | (''A'' ⊕ ''B'')<sup>⊥</sup> || = || ''A''<sup>⊥</sup> & ''B''<sup>⊥</sup> |- | (''A'' {{Unicode|⅋}} ''B'')<sup>⊥</sup> || = || ''A''<sup>⊥</sup> {{Unicode|⊗}} ''B''<sup>⊥</sup> |} The logical units have similar duals; for example: {{Unicode|⊤}}<sup>⊥</sup> = 0. Similarly, ! is dual to ?. The rule for duals is that an item may be moved from one side to the other by transforming it into its dual. Intuitionistic linear logic (ILL) allows only a single conclusion. Unlike CLL, connectives in ILL do not have perfect duals. Indeed, the connectives ''par'' and ''why not'' (?), and the propositional constant ''bottom'' (⊥), are absent in ILL because their [[introduction rule|introduction]] requires multiple conclusions. As a result, linear implication is a basic connective in ILL. Other variants of linear logic variously allow or disallow certain connectives, giving rise to logics with varying complexity. The following are the most common variants. * Multiplicative linear logic or MLL. This variant allows only the multiplicative connectives ''tensor'' and ''par'' (and their units). It is [[decidability (logic)|decidable]], but the decision problem is [[NP-complete]]. * Multiplicative additive linear logic or MALL, which adds the additive connectives to MLL. This variant is also decidable with a [[PSPACE-complete]] decision problem. * Multiplicative exponential linear logic or MELL, which is MLL plus the exponential operators. The decision problem for MELL is currently open. * Multiplicative additive exponential linear logic or MAELL, which has all the above connectives. This variant is [[undecidable]]. * Full Intuitionistic Linear Logic or FILL. This variant allows independent multiplicative connectives ''tensor'', ''par'' and ''linear implication''. This is just like [[Intuitionistic logic]], where one has independent connectives of conjunction, disjunction and implication. There are also first- and higher-order extensions of linear logic, but their development is standard (See [[first-order logic]] and [[higher-order logic]].) The closest sub-structural cousins of linear logic are: * [[Affine logic]], which extends linear logic with the [[structural rule]] of [[monotonicity of entailment|weakening]]. The connectives ''one'' and ''top'' are indistinguishable in affine logic. * [[Strict logic]] or [[relevant logic]], which extends linear logic with the structural rule of [[idempotency of entailment|contraction]]. * [[Non-commutative logic]] or [[ordered logic]] which '''removes''' the structural rule of [[exchange rule|exchange]] from linear logic. Multiplicative conjunction divides further into a pair of ''fuse''s (''left fuse'' and ''right fuse''). ==See also== * [[Logic of unity]] (LU) * [[Proof net]]s * [[Game semantics]] * [[Intuitionistic logic]] * [[Computability logic]] * [[Ludics]] * [[Chu space]]s * [[Uniqueness type]] ==References== * Girard, Jean-Yves. ''[http://iml.univ-mrs.fr/~girard/linear.pdf Linear logic]'', Theoretical Computer Science, London Mathematical 50:1, pp. 1-102, 1987. * Girard, Jean-Yves, Lafont, Yves, and Taylor, Paul. ''Proofs and Types''. Cambridge Press, 1989. (An electronic version is online at [http://www.cs.man.ac.uk/~pt/stable/Proofs+Types.html].) * [[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. ==External links== * [http://www.csl.sri.com/users/lincoln/ Patrick Lincoln]'s excellent [http://www.csl.sri.com/~lincoln/papers/sigact92.ps Introduction to Linear Logic] (Postscript) * Introduction to Linear Logic by Torben Brauner [http://www.brics.dk/LS/96/6/BRICS-LS-96-6/BRICS-LS-96-6.html] * A taste of linear logic by Philip Wadler [http://homepages.inf.ed.ac.uk/wadler/topics/linear-logic.html] * [http://plato.stanford.edu/archives/fall2006/entries/logic-linear/ Linear Logic] by [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 Note, Volume 316, 2004. {{portalpar|Logic}} {{Logic}} [[Category:Substructural logic]] [[ja:線形論理]] [[zh:线性逻辑]]