User:Kaustuv/ip/Linear logic

From Wikipedia, the free encyclopedia

 This page is a user's work in progress page, not an article, and may be incomplete and/or unreliable. The current version of this article is, or will be located at linear logic.

In mathematical logic, linear logic is a variety of substructural logic that denies the structural rules of weakening and contraction, which causes the hypotheses to be interpreted as resources that are consumed exactly once in a proof. Linear logic was proposed in 1987 by the French mathematician Jean-Yves Girard.[1]

Contents

[edit] Resources or truth?

In the usual classical or intuitionistic logics, the governing logical judgement is of mathematical truth, which may be freely used as necessary; the truth of a proposition does not change with its use. For example, from propositions A and A ⊃ B one may conclude A ∧ B as follows:

  1. Modus ponens (or implication elimination) on the assumptions A and A ⊃ B to conclude B.
  2. Conjunction of the assumption A and (1) to conclude A ∧ B.

This is often symbolically represented as a hypothetical judgement:

A, A ⊃ B ⊢ A ∧ B

where the turnstyle (⊢) separates the hypotheses on the left from the conclusion on the right. Both steps in the above proof consume the fact that A is true.

However, when describing a state or a world, mathematical truth does not model its objects. For example, suppose one has a quart of milk from which one can make a pound of butter. After using the milk to make butter, one cannot then conclude that one has both milk and butter. Yet, if one uses the schema above, one sees that the following hypothetical judgement should be provable:

milk, milk ⊃ butter ⊢ milk ∧ butter.

Ordinary logic fails to model this activity because resources cannot be reused. 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 change in the state. Thus, to make the logic resource-aware, one replaces the notion of logical entailment (⊢) with that of state change (⊩). That is, the interpretation of

A1, …, Aj ⊩ B1, …, Bj

is that the resources A1, …, Aj (written Γ) are used to construct the resources B1, …, Bj (written Δ).

[edit] Linear connectives

The logical connectives are re-examined in this resource-interpretation. Each connective splits into multiplicative and additive versions, which correspond to simultaneous and alternative presence, respectively. Linear logic is usually presented in a single-sided format, ⊩ A1, …, An, with the understanding that Γ ⊩ Δ stands for ⊩ (Γ)⊥, Δ, where A⊥ is the de Morgan dual of A.

Simultaneous conjunction, written ⊗ ("tensor"), denotes simultaneous occurrence of resources. To construct A ⊗ B, one must collate the resources used to construct A and those used to construct B. Simultaneous conjunction is not the same as the usual conjunction ∧, because A ⊗ A is not equivalent to A whereas A ∧ A is. The logical constant 1 is the unit of ⊗: A ⊗ 1 ≡ 1 ⊗ A ≡ A. The inference ruless for these connectives are as follows:

⊩ Γ, A     ⊩ Δ, B  ⊗
⊩ Γ, Δ, A ⊗ B
   1.
⊩ 1

Simultaneous disjunction, written ⅋ ("par"), is the de Morgan dual of ⊗ and denotes a group of resources that are simultaneously achievable in the same state. Its unit is ⊥, and their inference rules are as follows:

⊩ Γ, A, B  ⅋
⊩ Γ, A ⅋ B
⊩ Γ  ⊥.
⊩ Γ, ⊥

The butter-making example from before can be expressed using these connectives easily. The process of converting milk into butter is expressed as the simultaneous consumption of the milk and the production of the butter, i.e., milk⊥ ⅋ butter. The original problem consumes both the milk and this process to produce butter, which is the judgement ⊩ milk⊥, (milk⊥ ⅋ butter)⊥, butter, i.e., using de Morgan's laws, ⊩ milk⊥, milk ⊗ butter⊥, butter. Its proof is:

⊩ milk⊥, milk     ⊩ butter⊥, butter  ⊗.
⊩ milk⊥, milk ⊗ butter⊥, butter

Alternative conjunction, written &, denotes a group of resources that are alternatively achievable, that is, each of its operands can be achieved independently of the others. It has a unit ⊤ ("top"), and their inference rules are as follows:

⊩ Γ, A     ⊩ Γ, B  &
⊩ Γ, A & B
   ⊤.
⊩ Γ, ⊤

The key difference between simultaneous and alternative conjunction is that the resources are divided among the premisses in the former but not in the latter. The two connectives are incomparable: A ⊗ B neither implies, nor is implied by, A & B.

Alternative disjunction, written ⊕, is the de Morgan dual of & and denotes a group of resources of which only one is achievable. It has a unit written 0, which does not have any inference rule as it represents the impossibility. The rules for ⊕ are:

⊩ Γ, A  ⊕L
⊩ Γ, A ⊕ B
⊩ Γ, B  ⊕R
⊩ Γ, A ⊕ B

Linear implication, written ⊸, denotes a state change. The proposition A ⊸ B means: consume resource A to achieve resource B. It is definable using the previous connectives as:

A ⊸ B = A⊥ ⅋ B.

This definition is reminiscent of A ⊃ B as ¬ A ∨ B in ordinary classical logic.

[edit] Exponential connectives

The linear connectives of the previous section can describe state and transitions, but they are too weak to define the ordinary notion of mathematical truth. Mathematical truth is desirable, however, because a discussion about the actual world should not preclude standard mathematical reasoning. Linear logic uses modal logic to embed the usual logic by means of a pair of dual modal exponential connectives.

  • Re-use or copying is allowed for propositions using the "of course" modal (written !). Logically, two occurrences of resource !A may be contracted into a single occurrence.
  • The modal why not operator (written ?) allows adding resources of the form ?A ("why not A") arbitrarily. This corresponds to the structural rule of weakening.

These structural properties are written in the form of two structural rules of contraction (C) and weakening (W).

⊩ Γ, !A, !A  C
⊩ Γ, !A
⊩ Γ  W
⊩ Γ, ?A

The inference rules for the modal exponential connectives are as follows:

⊩ ?Γ, A  !
⊩ ?Γ, !A
⊩ Γ, A  ?
⊩ Γ, ?A

In the rule for !, the form ?Γ stands for a collection of resources of the form ?C.

[edit] Flavours of linear logic

Linear logic has many restrictions and variants. The primary axis of variation is along the classical/intuitionistic divide. The previous sections present classical linear logic (CLL), as originally proposed by Girard.

Intuitionistic linear logic (ILL) differs from classical linear logic allowing only a single goal resource that may be constructed from the resource hypotheses. 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 requires either zero or multiple goals. The entailment ⊩ is then internalised as a new connective ⊸, not definable in terms of the other connectives.

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 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.

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 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 contraction.
  • Non-commutative logic or ordered logic which removes the structural rule of exchange from linear logic. Multiplicative conjunction divides further into a pair of fuses (left fuse and right fuse).

[edit] See also

[edit] References

  • Girard, Jean-Yves. 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 [1].)
  • Troelstra, A.S. Lectures on Linear Logic. CSLI (Center for the Study of Language and Information) Lecture Notes No. 29. Stanford, 1992.

[edit] Footnotes

  1. ^ (Girard 87)

[edit] External links

Category:Substructural logic