Light linear logics - Revision history

Olivier Laurent: /* Elementary linear logic */ typo

2013-05-02T09:28:44Z

‎Elementary linear logic: typo

2009-03-19T20:22:00Z

‎Soft linear logic: explicit mention of multi-functoriality

2009-03-19T20:19:26Z

‎Light linear logic: explicit mention of functoriality

2009-03-19T20:16:45Z

‎Elementary linear logic: explicit mention of multi-functoriality

2009-03-19T18:37:56Z

2009-03-19T18:37:26Z

2009-03-19T18:36:38Z

2009-03-19T18:33:33Z

2009-03-19T18:32:39Z

2009-03-19T18:27:13Z

@@ Line 55: / Line 55: @@
 It enjoys the same properties as ELL.
-Elementary linear logic was introduced together with light linear logic in
+Elementary linear logic was introduced together with light linear logic
 <ref>{{BibEntry|bibtype=journal|author=Girard, Jean-Yves|title=Light linear logic|journal=Information and Computation|volume=143|pages=175-204|year=1998}}</ref>.

@@ Line 120: / Line 120: @@
 <math>
 \AxRule{\Gamma\vdash A}
-\LabelRule{\oc }
+\LabelRule{\oc\rulename{mf} }
 \UnaRule{\oc{\Gamma}\vdash\oc{A}}
 \DisplayProof
 \qquad
 \AxRule{\Gamma,A^{(n)}\vdash C}
-\LabelRule{mplex}
+\LabelRule{\rulename{mplex}}
 \UnaRule{\Gamma,\oc{A}\vdash C}
 \DisplayProof
@@ Line 144: / Line 144: @@
 The ''depth'' of a derivation <math>\pi</math> is the maximum number of
-<math>(\oc)</math> rules in a branch of <math>\pi</math>.
+<math>(\oc\rulename{mf})</math> rules in a branch of <math>\pi</math>.
@@ Line 156: / Line 156: @@
 Soft linear logic was introduced  in
 <ref>{{BibEntry|bibtype=journal|author=Lafont, Yves|title=Soft linear logic and polynomial time|journal=Theoretcal Computer Science|volume=318(1-2)|pages=163-180|year=2004}}</ref>.
 = References =
 <references />

@@ Line 70: / Line 70: @@
 <math>
 \AxRule{\Gamma\vdash A}
-\LabelRule{\oc }
+\LabelRule{\oc\rulename{f} }
 \UnaRule{\oc{\Gamma}\vdash\oc{A}}
 \DisplayProof
@@ Line 90: / Line 90: @@
 </math>
-In the <math>(\oc)</math> rule, <math>\Gamma</math> must contain ''at most one'' formula.
+In the <math>(\oc\rulename{f})</math> rule, <math>\Gamma</math> must contain ''at most one'' formula.
 The ''depth'' of a derivation <math>\pi</math> is the maximum number of
-<math>(\oc)</math> and <math>(\pg)</math> rules in a branch of <math>\pi</math>.
+<math>(\oc\rulename{f})</math> and <math>(\pg)</math> rules in a branch of <math>\pi</math>.
@@ Line 106: / Line 106: @@
 In the literature one also often considers the ''affine'' variant of LLL, called ''light affine logic'', LAL.
 = Soft linear logic =

@@ Line 14: / Line 14: @@
 <math>
 \AxRule{\Gamma\vdash A}
-\LabelRule{\oc }
+\LabelRule{\oc\rulename{mf} }
 \UnaRule{\oc{\Gamma}\vdash\oc{A}}
 \DisplayProof
@@ Line 30: / Line 30: @@
 The ''depth'' of a derivation <math>\pi</math> is the maximum number of
-<math>(\oc)</math> rules in a branch of <math>\pi</math>.
+<math>(\oc\rulename{mf})</math> rules in a branch of <math>\pi</math>.
 We consider the function <math>K(.,.)</math> defined by:<br>
@@ Line 57: / Line 57: @@
 Elementary linear logic was introduced together with light linear logic in
 <ref>{{BibEntry|bibtype=journal|author=Girard, Jean-Yves|title=Light linear logic|journal=Information and Computation|volume=143|pages=175-204|year=1998}}</ref>.
 = Light linear logic =
 We present the intuitionistic version of ''light linear logic''  LLL, without additive connectives. The language of formulas is:

@@ Line 155: / Line 155: @@
 Soft linear logic was introduced  in
-<ref>{{BibEntry|bibtype=journal|author=Lafont, Yves|title=Soft linear logic and polynomial time|journal=Theoretcal Computer Science|volume=318(1-2)|issue=1-2|pages=163-180|year=2004}}</ref>.
+<ref>{{BibEntry|bibtype=journal|author=Lafont, Yves|title=Soft linear logic and polynomial time|journal=Theoretcal Computer Science|volume=318(1-2)|pages=163-180|year=2004}}</ref>.
 = References =
 <references />

← Older revision		Revision as of 18:33, 19 March 2009
Line 153:		Line 153:
	{{Theorem\|The class of functions on binary lists representable in SLL is exactly FP.		{{Theorem\|The class of functions on binary lists representable in SLL is exactly FP.
	}}		}}
		+
		+	= References =
		+	<references />

← Older revision		Revision as of 18:27, 19 March 2009
Line 146:		Line 146:

	{{Theorem\|If <math>\pi</math> is an SLL proof of depth d, and R is the corresponding SLL proof-net, then R can be reduced to its normal form by cut elimination in		{{Theorem\|If <math>\pi</math> is an SLL proof of depth d, and R is the corresponding SLL proof-net, then R can be reduced to its normal form by cut elimination in
−	<math> O(\|\pi\|^d))</math> steps, where <math>\|\pi\|</math>is the size of <math>\pi</math>.}}	+	<math> O(\|\pi\|^d)</math> steps, where <math>\|\pi\|</math>is the size of <math>\pi</math>.}}