Fragment

From LLWiki
(Redirected from MLL)
Jump to: navigation, search

In general, a fragment of a logical system S is a logical system obtained by restricting the language of S, and by restricting the rules of S accordingly. In linear logic, the most well known fragments are obtained by combining/removing in different ways the classes of connectives present in the language of linear logic itself:

  • Multiplicative connectives: the conjunction \tens (tensor) and the disjunction \parr (par), with their respective units \one (one) and \bot (bottom); these connectives are the combinatorial base of linear logic (permutations, circuits, etc.).
  • Additive connectives: the conjunction \with (with) and the disjunction \plus (plus), with their respective units \top (top) and \zero (zero); the computational content of these connectives, which behave more closely to their intuitionistic counterparts (e.g., A\with B\limp A and A\with B\limp B are provable), is strongly related to choice (if...then...else, product and sum types, etc.).
  • Exponential connectives: the modalities \oc (of course) and \wn (why not) handle the structural rules in linear logic, and are necessary to recover the expressive power of intuitionistic or classical logic.
  • Quantifiers: just as in classical logic, quantifiers may be added to propositional linear logic, at any order. The most frequently considered are the second order ones (in analogy with System F).

The additive and exponential connectives, if taken alone, yield fragments of limited interest, so one usually considers only fragments containing at least the multiplicative connectives (perhaps without units). It is important to observe that the cut elimination rules of linear logic do not introduce connectives belonging to a different class than that of the pair of dual formulas whose cut is being reduced. Hence, any fragment defined by combining the above classes will enjoy cut elimination. Since cut elimination implies the subformula property, all of the fundamental equivalences provable in full linear logic remain valid within such fragments, as soon as the formulas concerned belong to the fragment itself.

Conventionally, if LL denotes full linear logic, its fragments are denoted by prefixing LL with letters corresponding to the classes of connectives being considered: M for multiplicative connectives, A for additive connectives, and E for exponential connectives. Additional subscripts may specify whether units and/or quantifiers are present or not, and, for quantifiers, of what order (see the article on notations).

Contents

Motivations

The main interest of studying fragments of linear logic is that these are usually simpler than the whole system, so that certain properties may be first analyzed on fragments, and then extended or adapted to increasingly larger fragments. It may also be interesting to see, given a property that does not hold for full linear logic, whether it holds for a fragment, and where the "breaking point" is situated. Examples of such questions include:

  • logical complexity: proving cut elimination for full linear logic with second order quantification is equivalent to proving the consistency of second order Peano arithmetic (Girard, via translations of System F in linear logic). One may expect that smaller fragments have lower logical complexity.
  • provability: the provability problem for a logical system S is defined as follows: given a formula A in the language of S, is A provable in S? This problem is undecidable in full linear logic with quantifiers, of whatever order (again, because classical logic can be translated in linear logic). On what fragments does it become decidable? And if it does, what is its computational complexity?
  • computational complexity of cut elimination: the cut elimination problem (Mairson-Terui) for a logical system S is defined as follows: given two proofs of A in S, do they reduce to the same cut-free proof? Although decidable (thanks to strong normalization), this problem is not elementary recursive in full propositional linear logic (Statman, again via the above-mentioned translations). Does the problem fall into any interesting complexity class when applied to fragments?
  • proof nets: the definition of proof nets, and in particular the formulation of correctness criteria and the study of their complexity, is a good example of how a methodology can be applied to a small fragment of linear logic and later adapted (more or less successfully) to wider fragments.
  • denotational semantics: several problems related to denotational semantics (formulation of categorical models, full abstraction, full completeness, injectivity, etc.) may be first attacked in the simpler case of fragments, and then extended to wider subsystems.

Multiplicative fragments

Multiplicative linear logic (MLL) is the simplest of the well known fragments of linear logic. Its formulas are obtained by combining propositional atoms with the connectives tensor and par only. As a consequence, the sequent calculus of MLL is limited to the rules \rulename{axiom}, \rulename{cut}, \tens, and \parr. These rules actually determine the multiplicative connectives: if a dual pair of connectives \tens' and \parr' is introduced, with the same rules as \tens and \parr, respectively, then one can show A\tens' B to be provably equivalent to A\tens B (and, dually, A\parr'B to be provably equivalent to A\parr B).

The cut elimination problem for MLL is \mathbf P-complete (Mairson-Terui), even though there exists a deterministic algorithm solving the problem in logarithmic space if one considers only eta-expanded proofs (Mairson-Terui). On the other hand, provability for MLL is \mathbf{NP}-complete, and it remains so even in presence of first order quantifiers.

Another multiplicative fragment, less considered in the literature, can be defined by using the units \one and \bot instead of the propositional atoms. In this fragment, denoted by MLLu, one can also eliminate the \rulename{axiom} rule from sequent calculus, since it is redundant. MLLu is even simpler than MLL: its provability problem is in \mathbf P, and, since all proofs are eta-expandend, its cut elimination problem is in \mathbf L.

The union of MLL and MLLu is the full propositional multiplicative fragment of linear logic, and is denoted by MLL0. It has the same properties as MLL, which shows that the presence/absence of propositional atoms (and of the \rulename{axiom} rule) has a non-trivial effect on the complexity of provability and cut elimination, i.e., the complexity is not altered iff \mathbf P\subsetneq\mathbf{NP} and \mathbf L\subsetneq\mathbf P, respectively.

If we add second order quantifiers to MLL (resp. MLLu), we obtain a system denoted by MLL2 (resp. MLL02). In MLL02 one can show that \one and \bot are provably equivalent to \forall X.(X\orth\parr X) and \exists X.(X\orth\tens X), respectively. Hence, MLL2 is as expressive as MLL02. In these second order fragments, provability is undecidable, while cut elimination is still \mathbf P-complete.

Additive fragments

The most studied additive fragments of linear logic are defined by taking MLL or MLL0 and by enriching their language with the additive connectives, with or without units. The same can be done in presence of quantifiers. We thus obtain:

  • MALL: formulas built from propositional atoms using \tens,\parr,\with,\plus;
  • MALL0: formulas built from propositional atoms and \one,\bot,\top,\zero, using \tens,\parr,\with,\plus;
  • MALLn: MALL with quantifiers of order n;
  • MALL0n: MALL0 with quantifiers of order n.

The purely additive framents are less common:

  • ALL: formulas built from propositional atoms using \with,\plus;
  • ALL0: formulas built from propositional atoms and \top,\zero, using \with,\plus;
  • ALLn: ALL with quantifiers of order n;
  • ALL0n: ALL0 with quantifiers of order n.

As for the multiplicative connectives, the additive connectives are also defined by their rules: adding a pair of dual connectives \with',\plus' to MALL, and giving them the same rules as \with,\plus, makes the new connectives provably equivalent to the old ones.

In MALL02, the additive units \top and \zero are provably equivalent to \exists X.X\orth and \forall X.X, respectively. Since multiplicative units are also definable in terms of second order quantification, we obtain that MALL2 is as expressive as MALL02.

The cut elimination problem is \mathbf{coNP}-complete for all of the fragments defined above (Mairson-Terui).

Provability is undecidable in any additive fragment as soon as second order quantification is considered. It is decidable, although quite complex, in the propositional and first order case: it is \mathbf{PSPACE}-complete in MALL0, and \mathbf{NEXP}-complete in MALL01. This latter result is indicative of the fact that the undecidability of predicate calculus is not ascribable to existential quantification alone, but rather to the simultaneous presence of existential quantification and contraction.

Exponential fragments

The most common proper fragments of linear logic containing the exponential connectives are defined as in the case of the additive fragments, i.e., by adding the modalities on top of MLL and its variants:

  • MELL: formulas built from propositional atoms using \tens,\parr,\oc,\wn;
  • MELL0: formulas built from propositional atoms and \one,\bot, using \tens,\parr,\oc,\wn;
  • MELLn: MELL with quantifiers of order n;
  • MELL0n: MELL0 with quantifiers of order n.

If, instead of taking MLL, we add the modalities to MALL, we obtain of course various versions of full linear logic:

  • LL: full linear logic, without units;
  • LL0: full linear logic, with units;
  • LLn: LL with quantifiers of order n;
  • LL0n: LL0 with quantifiers of order n.

In LL02 the formulas A\with B and A\plus B are provably equivalent to \exists X.(\oc{(X\orth\parr A)}\tens\oc{(X\orth\parr B)}\tens X) and \forall X.(\wn{(X\orth\tens A)}\parr\wn{(X\orth \tens B)}\parr X), respectively, for all A,B. Thanks to the second-order definability of units discussed above, we obtain that MELL2 is as expressive as LL02, i.e., full propositional second order linear logic embeds in its second order multiplicative exponential fragment without units.

Girard showed how cut elimination for LL02 without the contraction rule can be proved by a simple induction up to ω, i.e., in first order Peano arithmetic. This gives a huge gap between the logical complexity of full linear logic and its contraction-free subsystem: in fact, still by Girard's results, we know that cut elimination in MELL2 is equivalent to the consistency of second order Peano arithmetic, for which no ordinal analysis is known. There are nevertheless subsystems of MELL2, the so-called light subsystems of linear logic, in which the exponential connectives are weakened, whose cut elimination can be proved in seconder order Peano arithmetic even in presence of contraction.

The cut elimination problem is never elementary recursive in presence of exponential connectives: the simply typed λ-calculus with arrow types only can be encoded in MELL, and this is enough for Statman's lower bound to apply. However, it becomes elementary recursive in the above mentioned light logics.

Albeit perhaps surprisingly, provability in LL is already undecidable. This result, obtained by coding Minsky machines with linear logic formulas, contrasts with the situation in classical logic, whose propositional fragment is notoriously decidable. It is indicative of the fact that modalities are themselves a form of quantification, although this claim is far from being clear: as a matter of fact, the decidability of propositional provability in the absence of additives, i.e., in MELL alone, is still an open problem. It is known that adding first order quantification to MELL makes it undecidable.

About exponential rules

In this section, provability is assumed to be in LL02, i.e., full propositional second order linear logic.

In contrast with multiplicative and additive connectives, the modalities of linear logic are not defined by their rules: one may introduce a pair of dual modalities \oc',\wn', each with the same rules as \oc,\wn, without \oc'A (resp. \wn'A) being in general provably equivalent to \oc A (resp. \wn A).

The promotion rule is derivable from the following two rules, called functorial promotion and digging, respectively:


\AxRule{\vdash\Gamma,A}
\LabelRule{f\oc}
\UnaRule{\vdash\wn\Gamma,\oc A}
\DisplayProof
\qquad\qquad\qquad
\AxRule{\vdash\Gamma,\wn{\wn A}}
\LabelRule{dig}
\UnaRule{\vdash\Gamma,\wn A}
\DisplayProof

Functorial promotion is itself derivable from dereliction and promotion; the digging rule is also derivable, but only using the \rulename{cut} rule (in fact, digging does not enjoy the subformula property). It may be convenient to consider this pair of rules instead of the standard promotion rule in the context of categorical semantics of linear logic.

In presence of the digging rule, dereliction, weakening, and contraction can be derived from the following rule, called multiplexing, in which A(n) stands for the sequence A,\ldots,A containing n occurrences of A:


\AxRule{\vdash\Gamma,A^{(n)}}
\LabelRule{mux}
\UnaRule{\vdash\Gamma,\wn A}
\DisplayProof

Of course, multiplexing is itself derivable from dereliction, weakening, and contraction. Hence, there are several alternative but equivalent presentations of the exponential fragment of linear logic, such as

  1. remove promotion, and replace it with functorial promotion and digging;
  2. remove promotion, dereliction, weakening, and contraction, and replace them with functorial promotion, digging, and multiplexing.

Apart from their usefulness in categorical semantics, these alternative formulations are of interest in the context of the so-called light linear logics mentioned above. For example, elementary linear logic is obtained by removing dereliction and digging from formulation 1, and soft linear logic is obtained by removing digging from formulation 2.

Multiplexing is invertible in certain circumstances. A sequent \vdash\Gamma,\wn A containing no occurrence of \with, \oc, or second order \exists is provable iff \vdash\Gamma,A^{(n)} is provable for some n (this is easily checked by induction on cut-free proofs). To see that this does not hold in general, take for instance A=X\orth and \Gamma=X\with\one, or \Gamma=\oc X. The restriction on the presence of additive conjunction can be removed by slightly changing the statement: a sequent \vdash\Gamma,\wn A containing no occurrence of \oc or second order \exists is provable iff \vdash\Gamma,(A\plus\bot)^{(n)} is provable for some n.

The latter result can be generalized as follows. If A is a formula, \oc_nA stands for the formula (A\with\one)\tens\cdots\tens(A\with\one) (n times) and \wn_nA for the formula (A\plus\bot)\parr\cdots\parr(A\plus\bot) (n times). Then, we have

Theorem (Approximation Theorem)

Let \vdash\Gamma be a provable sequent containing p occurrences of \oc, q occurrences of \wn, and no occurrence of second order \exists. Then, for all m_1,\ldots,m_p\in\mathbb N, there are n_1,\ldots,n_q\in\mathbb N such that the sequent obtained from \vdash\Gamma by replacing the p occurrences of \oc with \oc_{m_1},\ldots,\oc_{m_p} and the q occurrences of \wn with \wn_{n_1},\ldots,\wn_{n_q} is provable.

A structural formula is a formula C such that C\limp C\tens C and C\limp\one are provable. Obviously, any formula of the form \wn B is structural. However, the promotion rule cannot be extended to arbitrary structural formulas, i.e., the following rule is not admissible:


\AxRule{C\vdash A}
\AxRule{C\vdash C\tens C}
\AxRule{C\vdash\one}
\TriRule{C\vdash\oc A}
\DisplayProof

For instance, if A=C=\alpha\tens\oc{(\alpha\limp\alpha\tens\alpha)}\tens\oc{(\alpha\limp\one)}, the three premises are provable but not the conclusion.

The following rule, called absorption, is derivable in the standard sequent calculus:


\AxRule{\vdash\Gamma,\wn A,A}
\UnaRule{\vdash\Gamma,\wn A}
\DisplayProof

The absorption rule is useful in the context of proof search in linear logic.

The provability problem

It is well known that the decidability of the provability problem is connected to the finite model property: if a fragment of a logic with a truth semantics enjoys the finite model property, then the provability in that fragment is decidable. Note of course that the converse may fail.

In this section, we summarize the known results about the validity of the final model property and the decidability of provability, with its complexity, for the various fragments of linear logic introduced above. Question marks in the tables below denote open problems. For brevity, all fragments are assumed to have units and propositional atoms, e.g., MLL actually denotes what we called MLL0 above.

The finite model property

MLL MALL MELL LL
yes yes no no

Provability

MLL MALL MELL LL
propositional case \mathbf{NP}-complete \mathbf{PSPACE}-complete  ? undecidable
first order case \mathbf{NP}-complete \mathbf{NEXP}-complete undecidable undecidable
second order case undecidable undecidable undecidable undecidable

The cut elimination problem

In this section, we summarize the known results about the complexity of the cut elimination problem for the various fragments of linear logic introduced above, plus some light linear logics. All fragments are assumed to be propositional; the results do not change in presence of quantification of any order.

MLLu MLL MALL MSLL MLLL MELL
\mathbf L \mathbf{P}-complete \mathbf{coNP}-complete \mathbf{EXP}-complete \mathbf{2EXP}-complete not elementary recursive

Notations used in the above table:

  • MSLL: multiplicative soft linear logic;
  • MLLL: multiplicative light linear logic.
Personal tools