Fragment - Revision history

Olivier Laurent: /* Additive fragments */ ALL added

2013-10-28T21:17:37Z

‎Additive fragments: ALL added

Damiano Mazza: /* Exponential fragments */

2009-07-16T13:46:48Z

‎Exponential fragments

Damiano Mazza: /* Motivations */

2009-07-16T13:39:13Z

‎Motivations

Emmanuel Beffara: Updated links to 'sequent calculus'

2009-03-12T16:01:23Z

Updated links to 'sequent calculus'

Damiano Mazza at 14:51, 3 March 2009

2009-03-03T14:51:47Z

Show changes

Damiano Mazza at 18:29, 1 March 2009

2009-03-01T18:29:10Z

Damiano Mazza: Removing all content from page

2009-03-01T14:57:07Z

Removing all content from page

Damiano Mazza: New page: A '''fragment''' is

2009-03-01T14:56:30Z

New page: A '''fragment''' is

New page

A '''fragment''' is

@@ Line 40: / Line 40: @@
 * <math>MALL_n</math>: <math>MALL</math> with quantifiers of order <math>n</math>;
 * <math>MALL_{0n}</math>: <math>MALL_0</math> with quantifiers of order <math>n</math>.
 As for the multiplicative connectives, the additive connectives are also defined by their rules: adding a pair of dual connectives <math>\with',\plus'</math> to <math>MALL</math>, and giving them the same rules as <math>\with,\plus</math>, makes the new connectives provably equivalent to the old ones.

@@ Line 67: / Line 67: @@
 In <math>LL_{02}</math> the formulas <math>A\with B</math> and <math>A\plus B</math> are provably equivalent to <math>\exists X.(\oc{(X\orth\parr A)}\tens\oc{(X\orth\parr B)}\tens X)</math> and <math>\forall X.(\wn{(X\orth\tens A)}\parr\wn{(X\orth \tens B)}\parr X)</math>, respectively, for all <math>A,B</math>. Thanks to the second-order definability of units discussed above, we obtain that <math>MELL_2</math> is as expressive as <math>LL_{02}</math>, ''i.e.'', full propositional second order linear logic embeds in its second order multiplicative exponential fragment without units.
-Girard showed how cut elimination for <math>LL_{02}</math> ''without the contraction rule'' can be proved by a simple induction up to <math>\omega</math>, ''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 <math>MELL_2</math> is equivalent to the consistency of second order Peano arithmetic, for which no ordinal analysis exists. There are nevertheless subsystems of <math>MELL_2</math>, the so-called [[Light linear logics|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.
+Girard showed how cut elimination for <math>LL_{02}</math> ''without the contraction rule'' can be proved by a simple induction up to <math>\omega</math>, ''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 <math>MELL_2</math> is equivalent to the consistency of second order Peano arithmetic, for which no ordinal analysis is known. There are nevertheless subsystems of <math>MELL_2</math>, the so-called [[Light linear logics|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 <math>\lambda</math>-calculus with arrow types only can be encoded in <math>MELL</math>, and this is enough for Statman's lower bound to apply. However, it becomes elementary recursive in the above mentioned [[Light linear logics|light logics]].

@@ Line 18: / Line 18: @@
 * '''computational complexity of cut elimination:''' the ''cut elimination problem'' (Mairson-Terui) for a logical system ''S'' is defined as follows: given two proofs of <math>A</math> 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.
 == Multiplicative fragments ==

@@ Line 6: / Line 6: @@
 * '''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 [[Sequent calculus#Cut elimination and consequences|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 [[Sequent calculus#Equivalences and definability|fundamental equivalences]] provable in full linear logic remain valid within such fragments, as soon as the formulas concerned belong to the fragment itself.
+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 [[Sequent calculus#Cut elimination and consequences|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 [[Sequent calculus#Equivalences|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 <math>LL</math> denotes full linear logic, its fragments are denoted by prefixing <math>LL</math> with letters corresponding to the classes of connectives being considered: <math>M</math> for multiplicative connectives, <math>A</math> for additive connectives, and <math>E</math> 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]]).
@@ Line 23: / Line 23: @@
 Multiplicative linear logic (<math>MLL</math>) 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#Sequents and proofs|sequent calculus]] of <math>MLL</math> is limited to the rules <math>\rulename{axiom}</math>, <math>\rulename{cut}</math>, <math>\tens</math>, and <math>\parr</math>. These rules actually determine the multiplicative connectives: if a dual pair of connectives <math>\tens'</math> and <math>\parr'</math> is introduced, with the same rules as <math>\tens</math> and <math>\parr</math>, respectively, then one can show <math>A\tens' B</math> to be provably equivalent to <math>A\tens B</math> (and, dually, <math>A\parr'B</math> to be provably equivalent to <math>A\parr B</math>).
-The cut elimination problem for <math>MLL</math> is <math>\mathbf P</math>-complete (Mairson-Terui), even though there exists a deterministic algorithm solving the problem in logarithmic space if one considers only [[Sequent calculus#Properties of proofs|eta-expanded]] proofs (Mairson-Terui). On the other hand, provability for <math>MLL</math> is <math>\mathbf{NP}</math>-complete, and it remains so even in presence of first order quantifiers.
+The cut elimination problem for <math>MLL</math> is <math>\mathbf P</math>-complete (Mairson-Terui), even though there exists a deterministic algorithm solving the problem in logarithmic space if one considers only [[Sequent calculus#Expansion of identities|eta-expanded]] proofs (Mairson-Terui). On the other hand, provability for <math>MLL</math> is <math>\mathbf{NP}</math>-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 <math>\one</math> and <math>\bot</math> instead of the propositional atoms. In this fragment, denoted by <math>MLL_u</math>, one can also eliminate the <math>\rulename{axiom}</math> rule from sequent calculus, since it is redundant. <math>MLL_u</math> is even simpler than <math>MLL</math>: its provability problem is in <math>\mathbf P</math>, and, since all proofs are eta-expandend, its cut elimination problem is in <math>\mathbf L</math>.

← Older revision	Revision as of 18:29, 1 March 2009
Line 1:	Line 1:
	+	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 [[Sequent calculus\|language of linear logic]] itself:
	+
	+	* '''Multiplicative connectives:''' the conjunction <math>\tens</math> (''tensor'') and the disjunction <math>\parr</math> (''par''), with their respective units <math>\one</math> (''one'') and <math>\bot</math> (''bottom''); these connectives are the combinatorial base of linear logic (permutations, circuits, etc.).
	+	* '''Additive connectives:''' the conjunction <math>\with</math> (''with'') and the disjunction <math>\plus</math> (''plus''), with their respective units <math>\top</math> (''top'') and <math>\zero</math> (''zero''); the computational content of these connectives, which behave more closely to their intuitionistic counterparts (e.g., <math>A\with B\limp A</math> and <math>A\with B\limp B</math> are provable), is strongly related to choice (''if...then...else'', product and sum types, etc.).
	+	* '''Exponential connectives:''' the modalities <math>\oc</math> (''of course'') and <math>\wn</math> (''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 [[Sequent calculus#Properties of proofs\|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.
	+
	+	Conventionally, if <math>LL</math> denotes full linear logic, its fragments are denoted by prefixing <math>LL</math> with letters corresponding to the classes of connectives being considered: <math>M</math> for multiplicative connectives, <math>A</math> for additive connectives, and <math>E</math> for exponential connectives. Additional subscripts may specify whether units and/or quantifiers are present or not, and, for quantifiers, at what order (see the article on [[notations]]).
	+
	+	== 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 intuitionistic logic\|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 <math>A</math> in the language of ''S'', is <math>A</math> provable in ''S''? This problem is undecidable in full linear logic with first order quantifiers (again, because [[Translations of classical logic\|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 <math>A</math> 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 linear logic with first order quantification (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.
	+
	+	== Multiplicative linear logic ==
	+
	+	Multiplicative linear logic (<math>MLL</math>) 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#Sequents and proofs\|sequent calculus]] of <math>MLL</math> is limited to the rules <math>\rulename{axiom}</math>, <math>\rulename{cut}</math>, <math>\tens</math>, and <math>\parr</math>. These rules actually determine the multiplicative connectives: if a dual pair of connectives <math>\tens'</math> and <math>\parr'</math> is introduced, with the same rules as <math>\tens</math> and <math>\parr</math>, respectively, then one can show <math>A\tens' B</math> to be provably equivalent to <math>A\tens B</math> (and, dually, <math>A\parr'B</math> to be provably equivalent to <math>A\parr B</math>).
	+
	+	The cut-elimination problem for <math>MLL</math> is <math>\mathbf P</math>-complete (Mairson-Terui), even though there exists a deterministic algorithm solving the problem in logarithmic space if one considers only [[Sequent calculus#Properties of proofs\|eta-expanded]] proofs (Mairson-Terui). On the other hand, provability for <math>MLL</math> is <math>\mathbf{NP}</math>-complete.
	+
	+	Another multiplicative fragment, less considered in the literarure, can be defined by using the units <math>\one</math> and <math>\bot</math> instead of the propositional atoms. In this fragment, denoted by <math>MLL_u</math>, one can also eliminate the <math>\rulename{axiom}</math> rule from sequent calculus, since it is redundant. <math>MLL_u</math> is even simpler than <math>MLL</math>: its provability problem is in <math>\mathbf P</math>, and, since all proofs are eta-expandend, its cut-elimination problem is in <math>\mathbf L</math>.
	+
	+	The union of <math>MLL</math> and <math>MLL_u</math> is the full propositional multiplicative fragment of linear logic, and is denoted by <math>MLL_0</math>. It has the same properties as <math>MLL</math>, which shows that the presence/absence of propositional atoms (and of the <math>\rulename{axiom}</math> rule) has a non-trivial effect on the complexity of provability and cut-elimination, i.e., the complexity is not altered iff <math>\mathbf P\subsetneq\mathbf{NP}</math> and <math>\mathbf L\subsetneq\mathbf P</math>, respectively.
	+
	+	If we add second order quantifiers to <math>MLL</math> (resp. <math>MLL_u</math>), we obtain a system denoted by <math>MLL_2</math> (resp. <math>MLL_{02}</math>). In <math>MLL_{02}</math> one can show that <math>\one</math> and <math>\bot</math> are provably equivalent to <math>\forall X.(X\orth\parr X)</math> and <math>\exists X.(X\orth\tens X)</math>, respectively. Hence, <math>MLL_2</math> is as expressive as <math>MLL_{02}</math>.
	+
	+	== Multiplicative additive linear logic ==
	+
	+	== Multiplicative exponential linear logic ==
	+
	+	== Quantifiers ==
	+
	+	== Intuitionistic linear logic ==
	+
	+	== The provability problem ==
	+
	+	== The cut-elimination problem ==

← Older revision		Revision as of 14:57, 1 March 2009
Line 1:		Line 1:
−	A '''fragment''' is