Light linear logics
(→Elementary linear logic) |
|||
| Line 54: | Line 54: | ||
It enjoys the same properties as ELL. |
It enjoys the same properties as ELL. |
||
| + | |||
| + | = Light linear logic = |
||
| + | We present the intuitionistic version of ''light linear logic'' LLL, without additive connectives. The language of formulas is: |
||
| + | |||
| + | <math> |
||
| + | A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \pg{A} \mid \forall X A |
||
| + | </math> |
||
| + | <br> |
||
| + | The sequent calculus rules are the same ones as for ILL, except for the rules |
||
| + | dealing with the exponential connectives: |
||
| + | |||
| + | <math> |
||
| + | \AxRule{\Gamma\vdash A} |
||
| + | \LabelRule{\oc } |
||
| + | \UnaRule{\oc{\Gamma}\vdash\oc{A}} |
||
| + | \DisplayProof |
||
| + | \qquad |
||
| + | \AxRule{\Gamma, \Delta\vdash A} |
||
| + | \LabelRule{\oc } |
||
| + | \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 |
||
| + | </math> |
||
| + | In the <math>(\oc)<\math> rule, <math>\Gamma<\math> must contain ''at most one'' formula. |
||
Revision as of 18:43, 19 March 2009
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.
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:
The sequent calculus rules are the same ones as for ILL, except for the rules
dealing with the exponential connectives:
The depth of a derivation π is the maximum number of
rules in a branch of π.
We consider the function K(.,.) defined by:
.
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:
It enjoys the same properties as ELL.
Light linear logic
We present the intuitionistic version of light linear logic LLL, without additive connectives. The language of formulas is:
The sequent calculus rules are the same ones as for ILL, except for the rules
dealing with the exponential connectives:
In the Failed to parse (unknown function\math): (\oc)<\math> rule, <math>\Gamma<\math> must contain ''at most one'' formula.
