Light linear logics

From LLWiki
(Difference between revisions)
Jump to: navigation, search
Line 27: Line 27:
 
\UnaRule{\Gamma,\oc{A}\vdash C}
 
\UnaRule{\Gamma,\oc{A}\vdash C}
 
\DisplayProof
 
\DisplayProof
</math>
+
</math><br>
We consider the function <math>K(.,.)</math> defined by:
+
We consider the function <math>K(.,.)</math> defined by:<br>
<math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)</math>.
+
<math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.

Revision as of 18:56, 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 research 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:


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 }
\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
We consider the function K(.,.) defined by:
K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}.

Personal tools