HOME

TheInfoList



OR:

Linear logic is a
substructural logic In logic, a substructural logic is a logic lacking one of the usual structural rules (e.g. of classical and intuitionistic logic), such as weakening, contraction, exchange or associativity. Two of the more significant substructural logics a ...
proposed by French logician
Jean-Yves Girard Jean-Yves Girard (; born 1947) is a French logician working in proof theory. He is a research director (emeritus) at the mathematical institute of University of Aix-Marseille, at Luminy. Biography Jean-Yves Girard is an alumnus of the Éc ...
as a refinement of classical and
intuitionistic logic Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems ...
, joining the dualities of the former with many of the constructive properties of the latter. 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 A programming language is a system of notation for writing computer programs. Programming languages are described in terms of their syntax (form) and semantics (meaning), usually defined by a formal language. Languages usually provide features ...
,
game semantics Game semantics is an approach to Formal semantics (logic), formal semantics that grounds the concepts of truth or Validity (logic), validity on Game theory, game-theoretic concepts, such as the existence of a winning strategy for a player. In this ...
, and
quantum physics Quantum mechanics is the fundamental physical Scientific theory, theory that describes the behavior of matter and of light; its unusual characteristics typically occur at and below the scale of atoms. Reprinted, Addison-Wesley, 1989, It is ...
(because linear logic can be seen as the logic of
quantum information theory Quantum information is the information of the state of a quantum system. It is the basic entity of study in quantum information theory, and can be manipulated using quantum information processing techniques. Quantum information refers to both t ...
), as well as
linguistics Linguistics is the scientific study of language. The areas of linguistic analysis are syntax (rules governing the structure of sentences), semantics (meaning), Morphology (linguistics), morphology (structure of words), phonetics (speech sounds ...
, particularly because of its emphasis on resource-boundedness, duality, and interaction. Linear logic lends itself to many different presentations, explanations, and intuitions. Proof-theoretically, it derives from an analysis of classical
sequent calculus In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology (called a sequent by Gerhard Gentzen) instead of an unconditional tautology. Each conditional tautolog ...
in which uses of (the structural rules) contraction and weakening are carefully controlled. Operationally, this means that logical deduction is no longer merely about an ever-expanding collection of persistent "truths", but also a way of manipulating ''resources'' that cannot always be duplicated or thrown away at will. In terms of simple denotational models, linear logic may be seen as refining the interpretation of intuitionistic logic by replacing cartesian (closed) categories by symmetric monoidal (closed) categories, or the interpretation of classical logic by replacing Boolean algebras by C*-algebras.


Connectives, duality, and polarity


Syntax

The language of ''classical linear logic'' (CLL) is defined inductively by the BNF notation Here and range over logical atoms. For reasons to be explained below, the
connectives In logic, a logical connective (also called a logical operator, sentential connective, or sentential operator) is a logical constant. Connectives can be used to connect logical formulas. For instance in the syntax of propositional logic, th ...
⊗, ⅋, 1, and ⊥ are called ''multiplicatives'', the connectives &, ⊕, ⊤, and 0 are called ''additives'', and the connectives ! and ? are called ''exponentials''. We can further employ the following terminology: Binary connectives ⊗, ⊕, & and ⅋ are associative and commutative; 1 is the unit for ⊗, 0 is the unit for ⊕, ⊥ is the unit for ⅋ and ⊤ is the unit for &. Every proposition in CLL has a dual , defined as follows: Observe that is an
involution Involution may refer to: Mathematics * Involution (mathematics), a function that is its own inverse * Involution algebra, a *-algebra: a type of algebraic structure * Involute, a construction in the differential geometry of curves * Exponentiati ...
, i.e., for all propositions. is also called the ''linear negation'' of . The columns of the table suggest another way of classifying the connectives of linear logic, termed : the connectives negated in the left column (⊗, ⊕, 1, 0, !) are called ''positive'', while their duals on the right (⅋, &, ⊥, ⊤, ?) are called ''negative''; cf. table on the right. is not included in the grammar of connectives, but is definable in CLL using linear negation and multiplicative disjunction, by . The connective ⊸ is sometimes pronounced " lollipop", owing to its shape.


Sequent calculus presentation

One way of defining linear logic is as a
sequent calculus In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology (called a sequent by Gerhard Gentzen) instead of an unconditional tautology. Each conditional tautolog ...
. We use the letters and to range over lists of propositions , also called ''contexts''. A ''sequent'' places a context to the left and the right of the turnstile, written . Intuitively, the sequent asserts that the conjunction of entails the disjunction of (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 inference rules describing how to build proofs of sequents. 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: Note that we do not add the structural rules of weakening and contraction, because we do care about the absence of propositions in a sequent, and the number of copies present. Next we add ''initial sequents'' and ''cuts'': The cut rule can be seen as a way of composing proofs, and initial sequents serve as the
units Unit may refer to: General measurement * Unit of measurement, a definite magnitude of a physical quantity, defined and adopted by convention or by law **International System of Units (SI), modern form of the metric system **English units, histo ...
for composition. In a certain sense these rules are redundant: as we introduce additional rules for building proofs below, we will maintain the property that arbitrary initial sequents can be derived from atomic initial sequents, and that whenever a sequent is provable it can be given a cut-free proof. Ultimately, this
canonical form In mathematics and computer science, a canonical, normal, or standard form of a mathematical object is a standard way of presenting that object as a mathematical expression. Often, it is one which provides the simplest representation of an obje ...
property (which can be divided into the completeness of atomic initial sequents and the
cut-elimination theorem The cut-elimination theorem (or Gentzen's ''Hauptsatz'') is the central result establishing the significance of the sequent calculus. It was originally proved by Gerhard Gentzen in part I of his landmark 1935 paper "Investigations in Logical Ded ...
, inducing a notion of analytic proof) lies behind the applications of linear logic in computer science, since it allows the logic to be used in proof search and as a resource-aware lambda-calculus. Now, we explain the connectives by giving ''logical rules''. Typically in sequent calculus one gives both "right-rules" and "left-rules" for each connective, essentially describing two modes of reasoning about propositions involving that connective (e.g., verification and falsification). In a one-sided presentation, one instead makes use of negation: the right-rules for a connective (say ⅋) effectively play the role of left-rules for its dual (⊗). So, we should expect a certain "harmony" between the rule(s) for a connective and the rule(s) for its dual.


Multiplicatives

The rules for multiplicative conjunction (⊗) and disjunction (⅋): and for their units: Observe that the rules for multiplicative conjunction and disjunction are admissible for plain ''conjunction'' and ''disjunction'' under a classical interpretation (i.e., they are admissible rules in LK).


Additives

The rules for additive conjunction (&) and disjunction (⊕) : and for their units: Observe that the rules for additive conjunction and disjunction are again admissible under a classical interpretation. But now we can explain the basis for the multiplicative/additive distinction in the rules for the two different versions of conjunction: for the multiplicative connective (⊗), the context of the conclusion () is split up between the premises, whereas for the additive case connective (&) the context of the conclusion () is carried whole into both premises.


Exponentials

The exponentials are used to give controlled access to weakening and contraction. Specifically, we add structural rules of weakening and contraction for 'd propositions: and use the following logical rules, in which stands for a list of propositions each prefixed with : 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 In logic, a normal modal logic is a set ''L'' of modal formulas such that ''L'' contains: * All propositional tautology (logic), tautologies; * All instances of the Kripke_semantics, Kripke schema: \Box(A\to B)\to(\Box A\to\Box B) and it is closed ...
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 LU presentation).


Remarkable formulas

In addition to the De Morgan dualities described above, some important equivalences in linear logic include: ; Distributivity : By definition of as , the last two distributivity laws also give: (Here is .) ; Exponential isomorphism : ; Linear distributions : A map that is not an isomorphism yet plays a crucial role in linear logic is: Linear distributions are fundamental in the proof theory of linear logic. The consequences of this map were first investigated in Cockett & Seely (1997) and called a "weak distribution". In subsequent work it was renamed to "linear distribution" to reflect the fundamental connection to linear logic. ; Other implications : The following distributivity formulas are not in general an equivalence, only an implication:


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 , while classical implication can be encoded as or (or a variety of alternative possible translations). 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 First-order logic, also called predicate logic, predicate calculus, or quantificational logic, is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over ...
into linear first-order logic.


The resource interpretation

Lafont (1993) first showed how intuitionistic linear logic can be explained as a logic of resources, so providing the logical language with access to formalisms that can be used for reasoning about resources within the logic itself, rather than, as in classical logic, by means of non-logical predicates and relations.
Tony Hoare Sir Charles Antony Richard Hoare (; born 11 January 1934), also known as C. A. R. Hoare, is a British computer scientist who has made foundational contributions to programming languages, algorithms, operating systems, formal verification, and ...
(1985)'s classic example of the vending machine can be used to illustrate this idea. Suppose we represent having a candy bar by the atomic proposition , and having a dollar by . To state the fact that a dollar will buy you one candy bar, we might write the implication . But in ordinary (classical or intuitionistic) logic, from and one can conclude . So, ordinary logic leads us to believe that we can buy the candy bar and keep our dollar! Of course, we can avoid this problem by using more sophisticated encodings, although typically such encodings suffer from the
frame problem In artificial intelligence, with implications for cognitive science, the frame problem describes an issue with using first-order logic to express facts about a robot in the world. Representing the state of a robot with traditional first-order logi ...
. However, the rejection of weakening and contraction allows linear logic to avoid this kind of spurious reasoning even with the "naive" rule. Rather than , we express the property of the vending machine as a ''linear'' implication . From and this fact, we can conclude , but ''not'' . In general, we can use the linear logic proposition to express the validity of transforming resource into resource . Running with the example of the vending machine, consider the "resource interpretations" of the other multiplicative and additive connectives. (The exponentials provide the means to combine this resource interpretation with the usual notion of persistent
logical truth Logical truth is one of the most fundamental concepts in logic. Broadly speaking, a logical truth is a statement which is true regardless of the truth or falsity of its constituent propositions. In other words, a logical truth is a statement whic ...
.) Multiplicative conjunction denotes simultaneous occurrence of resources, to be used as the consumer directs. For example, if you buy a stick of gum and a bottle of soft drink, then you are requesting . The constant 1 denotes the absence of any resource, and so functions as the unit of ⊗. Additive conjunction represents alternative occurrence of resources, the choice of which the consumer controls. If in the vending machine there is a packet of chips, a candy bar, and a can of soft drink, each costing one dollar, then for that price you can buy exactly one of these products. Thus we write . We do ''not'' write , which would imply that one dollar suffices for buying all three products together. However, from , we can correctly deduce , where . The unit ⊤ of additive conjunction can be seen as a wastebasket for unneeded resources. For example, we can write to express that with three dollars you can get a candy bar and some other stuff, without being more specific (for example, chips and a drink, or $2, or $1 and chips, etc.). Additive disjunction represents alternative occurrence of resources, the choice of which the machine controls. For example, suppose the vending machine permits gambling: insert a dollar and the machine may dispense a candy bar, a packet of chips, or a soft drink. We can express this situation as . The constant 0 represents a product that cannot be made, and thus serves as the unit of ⊕ (a machine that might produce or is as good as a machine that always produces because it will never succeed in producing a 0). So unlike above, we cannot deduce from this.


Other proof systems


Proof nets

Introduced by
Jean-Yves Girard Jean-Yves Girard (; born 1947) is a French logician working in proof theory. He is a research director (emeritus) at the mathematical institute of University of Aix-Marseille, at Luminy. Biography Jean-Yves Girard is an alumnus of the Éc ...
, proof nets have been created to avoid the ''bureaucracy'', that is all the things that make two derivations different in the logical point of view, but not in a "moral" point of view. For instance, these two proofs are "morally" identical: The goal of proof nets is to make them identical by creating a graphical representation of them.


Semantics


Algebraic semantics


Decidability/complexity of entailment

The
entailment Logical consequence (also entailment or logical implication) is a fundamental concept in logic which describes the relationship between statements that hold true when one statement logically ''follows from'' one or more statements. A valid l ...
relation in full CLL is undecidable. When considering fragments of CLL, the decision problem has varying complexity: * Multiplicative linear logic (MLL): only the multiplicative connectives. MLL entailment is
NP-complete In computational complexity theory, NP-complete problems are the hardest of the problems to which ''solutions'' can be verified ''quickly''. Somewhat more precisely, a problem is NP-complete when: # It is a decision problem, meaning that for any ...
, even restricting to Horn clauses in the purely implicative fragment, or to atom-free formulas. * Multiplicative-additive linear logic (MALL): only multiplicatives and additives (i.e., exponential-free). MALL entailment is
PSPACE-complete In computational complexity theory, a decision problem is PSPACE-complete if it can be solved using an amount of memory that is polynomial in the input length (PSPACE, polynomial space) and if every other problem that can be solved in polynomial sp ...
. * Multiplicative-exponential linear logic (MELL): only multiplicatives and exponentials. By reduction from the reachability problem for
Petri nets A Petri net, also known as a place/transition net (PT net), is one of several mathematical modeling languages for the description of distributed systems. It is a class of discrete event dynamic system. A Petri net is a directed bipartite grap ...
, MELL entailment must be at least 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 Theoretical computer science is a subfield of computer science and mathematics that focuses on the Abstraction, abstract and mathematical foundations of computation. It is difficult to circumscribe the theoretical areas precisely. The Associati ...
'', but was later shown to be erroneous. * Affine linear logic (that is linear logic with weakening, an extension rather than a fragment) was shown to be decidable, in 1995.


Variants

Many variations of linear logic arise by further tinkering with the structural rules: *
Affine logic Affine logic is a substructural logic whose proof theory rejects the structural rule of contraction. It can also be characterized as linear logic with weakening. The name "affine logic" is associated with linear logic, to which it differs by ...
, which forbids contraction but allows global weakening (a decidable extension). * Strict logic or relevant logic, which forbids weakening but allows global contraction. * Non-commutative logic or ordered logic, which removes the rule of exchange, in addition to barring weakening and contraction. In ordered logic, linear implication divides further into left-implication and right-implication. Different intuitionistic variants of linear logic have been considered. When based on a single-conclusion sequent calculus presentation, like in ILL (Intuitionistic Linear Logic), the connectives ⅋, ⊥, and ? are absent, and linear implication is treated as a primitive connective. In FILL (Full Intuitionistic Linear Logic) the connectives ⅋, ⊥, and ? are present, linear implication is a primitive connective and, similarly to what happens in intuitionistic logic, all connectives (except linear negation) are independent. There are also first- and higher-order extensions of linear logic, whose formal development is somewhat standard (see
first-order logic First-order logic, also called predicate logic, predicate calculus, or quantificational logic, is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over ...
and
higher-order logic In mathematics and logic, a higher-order logic (abbreviated HOL) is a form of logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics. Higher-order logics with their standard semantics are m ...
).


See also

* Chu spaces * Computability logic *
Game semantics Game semantics is an approach to Formal semantics (logic), formal semantics that grounds the concepts of truth or Validity (logic), validity on Game theory, game-theoretic concepts, such as the existence of a winning strategy for a player. In this ...
* Geometry of interaction *
Intuitionistic logic Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems ...
* Linear logic programming *
Linear type system Substructural type systems are a family of type systems analogous to substructural logics where one or more of the structural rules are absent or only allowed under controlled circumstances. Such systems can constrain access to system resource ...
, a
substructural type system Substructural type systems are a family of type systems analogous to substructural logics where one or more of the structural rules are absent or only allowed under controlled circumstances. Such systems can constrain access to system resourc ...
* Ludics * Proof nets * Uniqueness type


Notes


References

* * * * * * * * * * * *


Further reading

* * * * * * * * * * *


External links

*
A Linear Logic Prover (llprover)
, available for use online, from: Naoyuki Tamura / Dept of CS / Kobe University / Japan
Click And Collect
interactive linear logic prover, available online {{DEFAULTSORT:Linear Logic Non-classical logic Substructural logic Logic