Light linear logics

From LLWiki
(Difference between revisions)
Jump to: navigation, search
m (→‎Elementary linear logic: typo)
 
(4 intermediate revisions by 2 users not shown)
Line 14: Line 14:
 
<math>
  
<math>
 
\AxRule{\Gamma\vdash A}
  
\AxRule{\Gamma\vdash A}
−
\LabelRule{\oc }
 +
\LabelRule{\oc\rulename{mf} }
 
\UnaRule{\oc{\Gamma}\vdash\oc{A}}
  
\UnaRule{\oc{\Gamma}\vdash\oc{A}}
 
\DisplayProof
  
\DisplayProof
Line 30: Line 30:
   
 
The ''depth'' of a derivation <math>\pi</math> is the maximum number of
  
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>
  
We consider the function <math>K(.,.)</math> defined by:<br>
Line 55: Line 55:
 
It enjoys the same properties as ELL.
  
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>.
  
<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 =
  
= Light linear logic =
 
We present the intuitionistic version of ''light linear logic'' LLL, without additive connectives. The language of formulas is:
  
We present the intuitionistic version of ''light linear logic'' LLL, without additive connectives. The language of formulas is:
Line 69: Line 70:
 
<math>
  
<math>
 
\AxRule{\Gamma\vdash A}
  
\AxRule{\Gamma\vdash A}
−
\LabelRule{\oc }
 +
\LabelRule{\oc\rulename{f} }
 
\UnaRule{\oc{\Gamma}\vdash\oc{A}}
  
\UnaRule{\oc{\Gamma}\vdash\oc{A}}
 
\DisplayProof
  
\DisplayProof
Line 89: Line 90:
 
</math>
  
</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
  
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 105: Line 106:
   
 
In the literature one also often considers the ''affine'' variant of LLL, called ''light affine logic'', LAL.
  
In the literature one also often considers the ''affine'' variant of LLL, called ''light affine logic'', LAL.
−  
   
 
= Soft linear logic =
  
= Soft linear logic =
Line 120: Line 120:
 
<math>
  
<math>
 
\AxRule{\Gamma\vdash A}
  
\AxRule{\Gamma\vdash A}
−
\LabelRule{\oc }
 +
\LabelRule{\oc\rulename{mf} }
 
\UnaRule{\oc{\Gamma}\vdash\oc{A}}
  
\UnaRule{\oc{\Gamma}\vdash\oc{A}}
 
\DisplayProof
  
\DisplayProof
 
\qquad
  
\qquad
 
\AxRule{\Gamma,A^{(n)}\vdash C}
  
\AxRule{\Gamma,A^{(n)}\vdash C}
−
\LabelRule{mplex}
 +
\LabelRule{\rulename{mplex}}
 
\UnaRule{\Gamma,\oc{A}\vdash C}
  
\UnaRule{\Gamma,\oc{A}\vdash C}
 
\DisplayProof
  
\DisplayProof
Line 144: Line 144:
   
 
The ''depth'' of a derivation <math>\pi</math> is the maximum number of
  
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 155: Line 155:
   
 
Soft linear logic was introduced in
  
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 =
 
<references />
  
<references />

Latest revision as of 10:28, 2 May 2013

Light linear logics are variants of linear logic characterizing complexity classes. They are designed by defining alternative exponential connectives, which induce a complexity bound on the cut-elimination procedure.
Light linear logics are one of the approaches used in implicit computational complexity, the area studying the computational complexity of programs without referring to external measuring conditions or particular machine models.

Contents

[edit] Elementary linear logic

We present here the intuitionistic version of elementary linear logic, ELL. Moreover we restrict to the fragment without additive connectives.
The language of formulas is the same one as that of (multiplicative) ILL:

A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A
The sequent calculus rules are the same ones as for ILL, except for the rules dealing with the exponential connectives:

\AxRule{\Gamma\vdash A} \LabelRule{\oc\rulename{mf} } \UnaRule{\oc{\Gamma}\vdash\oc{A}} \DisplayProof \qquad \AxRule{\Gamma,\oc{A},\oc{A}\vdash C} \LabelRule{\oc c L} \UnaRule{\Gamma,\oc{A}\vdash C} \DisplayProof \qquad \AxRule{\Gamma\vdash C} \LabelRule{\oc w L} \UnaRule{\Gamma,\oc{A}\vdash C} \DisplayProof

The depth of a derivation π is the maximum number of (\oc\rulename{mf}) rules in a branch of π.

We consider the function K(.,.) defined by:
K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}.

Theorem

If π is an ELL proof of depth d, and R is the corresponding ELL proof-net, then R can be reduced to its normal form by cut elimination in at most K(d + 1, | π | ) steps, where | π | is the size of π.

A function f on integers is elementary recursive if there exists an integer h and a Turing machine which computes f in time bounded by K(h,n), where n is the size of the input.

Theorem

The functions representable in ELL are exactly the elementary recursive functions.

One also often considers the affine variant of ELL, called elementary affine logic EAL, which is defined by adding unrestricted weakening:

\AxRule{\Gamma\vdash C} \LabelRule{ w L} \UnaRule{\Gamma,A\vdash C} \DisplayProof

It enjoys the same properties as ELL.

Elementary linear logic was introduced together with light linear logic [1].

[edit] Light linear logic

We present the intuitionistic version of light linear logic LLL, without additive connectives. The language of formulas is:

A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \pg{A} \mid \forall X A
The sequent calculus rules are the same ones as for ILL, except for the rules dealing with the exponential connectives:

\AxRule{\Gamma\vdash A} \LabelRule{\oc\rulename{f} } \UnaRule{\oc{\Gamma}\vdash\oc{A}} \DisplayProof \qquad \AxRule{\Gamma, \Delta\vdash A} \LabelRule{\pg } \UnaRule{\oc{\Gamma}, \pg \Delta\vdash\pg{A}} \DisplayProof \qquad \AxRule{\Gamma,\oc{A},\oc{A}\vdash C} \LabelRule{\oc c L} \UnaRule{\Gamma,\oc{A}\vdash C} \DisplayProof \qquad \AxRule{\Gamma\vdash C} \LabelRule{\oc w L} \UnaRule{\Gamma,\oc{A}\vdash C} \DisplayProof

In the (\oc\rulename{f}) rule, Γ must contain at most one formula.


The depth of a derivation π is the maximum number of (\oc\rulename{f}) and (\pg) rules in a branch of π.


Theorem

If π is an LLL proof of depth d, and R is the corresponding LLL proof-net, then R can be reduced to its normal form by cut elimination in O((d+1)|\pi|^{2^{d+1}}) steps, where | π | is the size of π.

The class FP is the class of functions on binary lists which are computable in polynomial time on a Turing machine.

Theorem

The class of functions on binary lists representable in LLL is exactly FP.

In the literature one also often considers the affine variant of LLL, called light affine logic, LAL.

[edit] Soft linear logic

We consider the intuitionistic version of soft linear logic, SLL.

The language of formulas is the same one as that of ILL: A ::= X \mid A\tens A \mid A\limp A \mid A\with A \mid A\plus A \mid \oc{A} \mid \forall X A
The sequent calculus rules are the same ones as for ILL, except for the rules dealing with the exponential connectives:

\AxRule{\Gamma\vdash A} \LabelRule{\oc\rulename{mf} } \UnaRule{\oc{\Gamma}\vdash\oc{A}} \DisplayProof \qquad \AxRule{\Gamma,A^{(n)}\vdash C} \LabelRule{\rulename{mplex}} \UnaRule{\Gamma,\oc{A}\vdash C} \DisplayProof

The rule mplex is the multiplexing rule. In its premise, A(n) stands for n occurrences of formula A. As particular instances of mplex for n = 0 and 1 respectively, we get weakening and dereliction:

\AxRule{\Gamma \vdash C} \UnaRule{\Gamma,\oc{A}\vdash C} \DisplayProof \qquad \AxRule{\Gamma,A\vdash C} \UnaRule{\Gamma,\oc{A}\vdash C} \DisplayProof

The depth of a derivation π is the maximum number of (\oc\rulename{mf}) rules in a branch of π.


Theorem

If π 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 O( | π | d) steps, where | π | is the size of π.


Theorem

The class of functions on binary lists representable in SLL is exactly FP.

Soft linear logic was introduced in [2].

[edit] References

  1. ↑ Girard, Jean-Yves. Light linear logic. Information and Computation. Volume 143, pp. 175-204, 1998.
  2. ↑ Lafont, Yves. Soft linear logic and polynomial time. Theoretcal Computer Science. Volume 318(1-2), pp. 163-180, 2004.
Retrieved from "http://140.77.166.78/mediawiki/index.php?title=Light_linear_logics&oldid=586"
Personal tools