LLWiki - User contributions [en]

http://140-77-166-78.cprapid.com/mediawiki/api.php?action=feedcontributions&feedformat=atom&user=Patrick+Baillot LLWiki - User contributions [en] 2026-04-12T07:32:27Z User contributions MediaWiki 1.19.20+dfsg-0+deb7u3 http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T18:37:56Z

<p>Patrick Baillot: </p> <hr /> <div>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.<br><br /> 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. <br /> <br /> = Elementary linear logic =<br /> We present here the intuitionistic version of ''elementary linear logic'', ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) [[Intuitionistic linear logic|ILL]]:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for [[Intuitionistic linear logic|ILL]], except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br /> <br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,|\pi|)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> A function f on integers is ''elementary recursive'' if there exists an integer h and a Turing machine <br /> which computes f in time bounded by <math>K(h,n)</math>, where n is the size of the input.<br /> <br /> {{Theorem|The functions representable in ELL are exactly the elementary recursive<br /> functions.<br /> }}<br /> <br /> One also often considers the ''affine'' variant of ELL, called ''elementary affine logic'' EAL, which is defined by adding unrestricted weakening:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{ w L}<br /> \UnaRule{\Gamma,A\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> It enjoys the same properties as ELL.<br /> <br /> Elementary linear logic was introduced together with light linear logic in<br /> <ref>{{BibEntry|bibtype=journal|author=Girard, Jean-Yves|title=Light linear logic|journal=Information and Computation|volume=143|pages=175-204|year=1998}}</ref>.<br /> = Light linear logic =<br /> We present the intuitionistic version of ''light linear logic'' LLL, without additive connectives. The language of formulas is:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \pg{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma, \Delta\vdash A}<br /> \LabelRule{\pg }<br /> \UnaRule{\oc{\Gamma}, \pg \Delta\vdash\pg{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> In the <math>(\oc)</math> rule, <math>\Gamma</math> must contain ''at most one'' formula.<br /> <br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> and <math>(\pg)</math> rules in a branch of <math>\pi</math>.<br /> <br /> <br /> {{Theorem|If <math>\pi</math> 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 <br /> <math> O((d+1)|\pi|^{2^{d+1}})</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> The class FP is the class of functions on binary lists which are computable in polynomial time on a Turing machine.<br /> <br /> {{Theorem|The class of functions on binary lists representable in LLL is exactly FP.<br /> }}<br /> <br /> In the literature one also often considers the ''affine'' variant of LLL, called ''light affine logic'', LAL.<br /> <br /> <br /> = Soft linear logic =<br /> We consider the intuitionistic version of ''soft linear logic'', SLL.<br /> <br /> The language of formulas is the same one as that of ILL:<br /> <math><br /> 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 <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,A^{(n)}\vdash C}<br /> \LabelRule{mplex}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The rule mplex is the ''multiplexing'' rule. In its premise, <math>A^{(n)}</math> stands for<br /> n occurrences of formula <math> A </math>. As particular instances of mplex for <math>n=0</math> and 1 respectively, we get weakening and dereliction:<br /> <br /> <math><br /> \AxRule{\Gamma \vdash C}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,A\vdash C}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> <br /> {{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 <br /> <math> O(|\pi|^d)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> <br /> {{Theorem|The class of functions on binary lists representable in SLL is exactly FP.<br /> }}<br /> <br /> Soft linear logic was introduced in<br /> <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>.<br /> = References =<br /> <references /></div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T18:37:26Z

<p>Patrick Baillot: </p> <hr /> <div>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.<br><br /> 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. <br /> <br /> = Elementary linear logic =<br /> We present here the intuitionistic version of ''elementary linear logic'', ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) [[Intuitionistic linear logic|ILL]]:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for [[Intuitionistic linear logic|ILL]], except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br /> <br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,|\pi|)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> A function f on integers is ''elementary recursive'' if there exists an integer h and a Turing machine <br /> which computes f in time bounded by <math>K(h,n)</math>, where n is the size of the input.<br /> <br /> {{Theorem|The functions representable in ELL are exactly the elementary recursive<br /> functions.<br /> }}<br /> <br /> One also often considers the ''affine'' variant of ELL, called ''elementary affine logic'' EAL, which is defined by adding unrestricted weakening:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{ w L}<br /> \UnaRule{\Gamma,A\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> It enjoys the same properties as ELL.<br /> <br /> Elementary linear logic was introduced together with light linear logic in<br /> <ref>{{BibEntry|bibtype=journal|author=Girard, Jean-Yves|title=Light linear logic|journal=Information and Computation|volume=143|pages=175-204|year=1998}}</ref>.<br /> = Light linear logic =<br /> We present the intuitionistic version of ''light linear logic'' LLL, without additive connectives. The language of formulas is:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \pg{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma, \Delta\vdash A}<br /> \LabelRule{\pg }<br /> \UnaRule{\oc{\Gamma}, \pg \Delta\vdash\pg{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> In the <math>(\oc)</math> rule, <math>\Gamma</math> must contain ''at most one'' formula.<br /> <br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> and <math>(\pg)</math> rules in a branch of <math>\pi</math>.<br /> <br /> <br /> {{Theorem|If <math>\pi</math> 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 <br /> <math> O((d+1)|\pi|^{2^{d+1}})</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> The class FP is the class of functions on binary lists which are computable in polynomial time on a Turing machine.<br /> <br /> {{Theorem|The class of functions on binary lists representable in LLL is exactly FP.<br /> }}<br /> <br /> In the literature one also often considers the ''affine'' variant of LLL, called ''light affine logic'', LAL.<br /> <br /> <br /> = Soft linear logic =<br /> We consider the intuitionistic version of ''soft linear logic'', SLL.<br /> <br /> The language of formulas is the same one as that of ILL:<br /> <math><br /> 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 <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,A^{(n)}\vdash C}<br /> \LabelRule{mplex}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The rule mplex is the ''multiplexing'' rule. In its premise, <math>A^{(n)}</math> stands for<br /> n occurrences of formula <math> A </math>. As particular instances of mplex for <math>n=0</math> and 1 respectively, we get weakening and dereliction:<br /> <br /> <math><br /> \AxRule{\Gamma \vdash C}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,A\vdash C}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> <br /> {{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 <br /> <math> O(|\pi|^d)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> <br /> {{Theorem|The class of functions on binary lists representable in SLL is exactly FP.<br /> }}<br /> <br /> Soft linear logic was introduced in<br /> <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>.<br /> = References =<br /> <references /></div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T18:36:38Z

<p>Patrick Baillot: </p> <hr /> <div>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.<br><br /> 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. <br /> <br /> = Elementary linear logic =<br /> We present here the intuitionistic version of ''elementary linear logic'', ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) [[Intuitionistic linear logic|ILL]]:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for [[Intuitionistic linear logic|ILL]], except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br /> <br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,|\pi|)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> A function f on integers is ''elementary recursive'' if there exists an integer h and a Turing machine <br /> which computes f in time bounded by <math>K(h,n)</math>, where n is the size of the input.<br /> <br /> {{Theorem|The functions representable in ELL are exactly the elementary recursive<br /> functions.<br /> }}<br /> <br /> One also often considers the ''affine'' variant of ELL, called ''elementary affine logic'' EAL, which is defined by adding unrestricted weakening:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{ w L}<br /> \UnaRule{\Gamma,A\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> It enjoys the same properties as ELL.<br /> <br /> Elementary linear logic was introduced together with light linear logic in<br /> <ref>{{BibEntry|bibtype=journal|author=Girard, Jean-Yves|title=Light linear logic|journal=Information and Computation|volume=143|pages=175-204|year=1998}}</ref>.<br /> = Light linear logic =<br /> We present the intuitionistic version of ''light linear logic'' LLL, without additive connectives. The language of formulas is:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \pg{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma, \Delta\vdash A}<br /> \LabelRule{\pg }<br /> \UnaRule{\oc{\Gamma}, \pg \Delta\vdash\pg{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> In the <math>(\oc)</math> rule, <math>\Gamma</math> must contain ''at most one'' formula.<br /> <br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> and <math>(\pg)</math> rules in a branch of <math>\pi</math>.<br /> <br /> <br /> {{Theorem|If <math>\pi</math> 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 <br /> <math> O((d+1)|\pi|^{2^{d+1}})</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> The class FP is the class of functions on binary lists which are computable in polynomial time on a Turing machine.<br /> <br /> {{Theorem|The class of functions on binary lists representable in LLL is exactly FP.<br /> }}<br /> <br /> In the literature one also often considers the ''affine'' variant of LLL, called ''light affine logic'', LAL.<br /> <br /> <br /> = Soft linear logic =<br /> We consider the intuitionistic version of ''soft linear logic'', SLL.<br /> <br /> The language of formulas is the same one as that of ILL:<br /> <math><br /> 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 <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,A^{(n)}\vdash C}<br /> \LabelRule{mplex}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The rule mplex is the ''multiplexing'' rule. In its premise, <math>A^{(n)}</math> stands for<br /> n occurrences of formula <math> A </math>. As particular instances of mplex for <math>n=0</math> and 1 respectively, we get weakening and dereliction:<br /> <br /> <math><br /> \AxRule{\Gamma \vdash C}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,A\vdash C}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> <br /> {{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 <br /> <math> O(|\pi|^d)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> <br /> {{Theorem|The class of functions on binary lists representable in SLL is exactly FP.<br /> }}<br /> <br /> Soft linear logic was introduced in<br /> <ref>{{BibEntry|bibtype=journal|author=Lafont, Yves|title=Soft linear logic and polynomial time|journal=Theoretcal Computer Science|volume=318|issue=1-2|pages=163-180|year=2004}}</ref>.<br /> = References =<br /> <references /></div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T18:33:33Z

<p>Patrick Baillot: </p> <hr /> <div>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.<br><br /> 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. <br /> <br /> = Elementary linear logic =<br /> We present here the intuitionistic version of ''elementary linear logic'', ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) [[Intuitionistic linear logic|ILL]]:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for [[Intuitionistic linear logic|ILL]], except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br /> <br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,|\pi|)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> A function f on integers is ''elementary recursive'' if there exists an integer h and a Turing machine <br /> which computes f in time bounded by <math>K(h,n)</math>, where n is the size of the input.<br /> <br /> {{Theorem|The functions representable in ELL are exactly the elementary recursive<br /> functions.<br /> }}<br /> <br /> One also often considers the ''affine'' variant of ELL, called ''elementary affine logic'' EAL, which is defined by adding unrestricted weakening:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{ w L}<br /> \UnaRule{\Gamma,A\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> It enjoys the same properties as ELL.<br /> <br /> Elementary linear logic was introduced together with light linear logic in<br /> <ref>{{BibEntry|bibtype=journal|author=Girard, Jean-Yves|title=Light linear logic.|journal=Information and Computation|volume=143|pages=175-204|year=1998}}</ref>.<br /> = Light linear logic =<br /> We present the intuitionistic version of ''light linear logic'' LLL, without additive connectives. The language of formulas is:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \pg{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma, \Delta\vdash A}<br /> \LabelRule{\pg }<br /> \UnaRule{\oc{\Gamma}, \pg \Delta\vdash\pg{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> In the <math>(\oc)</math> rule, <math>\Gamma</math> must contain ''at most one'' formula.<br /> <br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> and <math>(\pg)</math> rules in a branch of <math>\pi</math>.<br /> <br /> <br /> {{Theorem|If <math>\pi</math> 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 <br /> <math> O((d+1)|\pi|^{2^{d+1}})</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> The class FP is the class of functions on binary lists which are computable in polynomial time on a Turing machine.<br /> <br /> {{Theorem|The class of functions on binary lists representable in LLL is exactly FP.<br /> }}<br /> <br /> In the literature one also often considers the ''affine'' variant of LLL, called ''light affine logic'', LAL.<br /> <br /> <br /> = Soft linear logic =<br /> We consider the intuitionistic version of ''soft linear logic'', SLL.<br /> <br /> The language of formulas is the same one as that of ILL:<br /> <math><br /> 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 <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,A^{(n)}\vdash C}<br /> \LabelRule{mplex}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The rule mplex is the ''multiplexing'' rule. In its premise, <math>A^{(n)}</math> stands for<br /> n occurrences of formula <math> A </math>. As particular instances of mplex for <math>n=0</math> and 1 respectively, we get weakening and dereliction:<br /> <br /> <math><br /> \AxRule{\Gamma \vdash C}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,A\vdash C}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> <br /> {{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 <br /> <math> O(|\pi|^d)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> <br /> {{Theorem|The class of functions on binary lists representable in SLL is exactly FP.<br /> }}<br /> <br /> = References =<br /> <references /></div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T18:32:39Z

<p>Patrick Baillot: </p> <hr /> <div>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.<br><br /> 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. <br /> <br /> = Elementary linear logic =<br /> We present here the intuitionistic version of ''elementary linear logic'', ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) [[Intuitionistic linear logic|ILL]]:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for [[Intuitionistic linear logic|ILL]], except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br /> <br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,|\pi|)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> A function f on integers is ''elementary recursive'' if there exists an integer h and a Turing machine <br /> which computes f in time bounded by <math>K(h,n)</math>, where n is the size of the input.<br /> <br /> {{Theorem|The functions representable in ELL are exactly the elementary recursive<br /> functions.<br /> }}<br /> <br /> One also often considers the ''affine'' variant of ELL, called ''elementary affine logic'' EAL, which is defined by adding unrestricted weakening:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{ w L}<br /> \UnaRule{\Gamma,A\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> It enjoys the same properties as ELL.<br /> <br /> Elementary linear logic was introduced together with light linear logic in<br /> <ref>{{BibEntry|bibtype=journal|author=Girard, Jean-Yves|title=Light linear logic.|journal=Information and Computation|volume=143|pages=175-204|year=1998}}</ref>.<br /> = Light linear logic =<br /> We present the intuitionistic version of ''light linear logic'' LLL, without additive connectives. The language of formulas is:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \pg{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma, \Delta\vdash A}<br /> \LabelRule{\pg }<br /> \UnaRule{\oc{\Gamma}, \pg \Delta\vdash\pg{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> In the <math>(\oc)</math> rule, <math>\Gamma</math> must contain ''at most one'' formula.<br /> <br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> and <math>(\pg)</math> rules in a branch of <math>\pi</math>.<br /> <br /> <br /> {{Theorem|If <math>\pi</math> 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 <br /> <math> O((d+1)|\pi|^{2^{d+1}})</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> The class FP is the class of functions on binary lists which are computable in polynomial time on a Turing machine.<br /> <br /> {{Theorem|The class of functions on binary lists representable in LLL is exactly FP.<br /> }}<br /> <br /> In the literature one also often considers the ''affine'' variant of LLL, called ''light affine logic'', LAL.<br /> <br /> <br /> = Soft linear logic =<br /> We consider the intuitionistic version of ''soft linear logic'', SLL.<br /> <br /> The language of formulas is the same one as that of ILL:<br /> <math><br /> 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 <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,A^{(n)}\vdash C}<br /> \LabelRule{mplex}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The rule mplex is the ''multiplexing'' rule. In its premise, <math>A^{(n)}</math> stands for<br /> n occurrences of formula <math> A </math>. As particular instances of mplex for <math>n=0</math> and 1 respectively, we get weakening and dereliction:<br /> <br /> <math><br /> \AxRule{\Gamma \vdash C}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,A\vdash C}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> <br /> {{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 <br /> <math> O(|\pi|^d)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> <br /> {{Theorem|The class of functions on binary lists representable in SLL is exactly FP.<br /> }}</div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T18:27:13Z

<p>Patrick Baillot: </p> <hr /> <div>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.<br><br /> 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. <br /> <br /> = Elementary linear logic =<br /> We present here the intuitionistic version of ''elementary linear logic'', ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) [[Intuitionistic linear logic|ILL]]:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for [[Intuitionistic linear logic|ILL]], except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br /> <br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,|\pi|)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> A function f on integers is ''elementary recursive'' if there exists an integer h and a Turing machine <br /> which computes f in time bounded by <math>K(h,n)</math>, where n is the size of the input.<br /> <br /> {{Theorem|The functions representable in ELL are exactly the elementary recursive<br /> functions.<br /> }}<br /> <br /> One also often considers the ''affine'' variant of ELL, called ''elementary affine logic'' EAL, which is defined by adding unrestricted weakening:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{ w L}<br /> \UnaRule{\Gamma,A\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> It enjoys the same properties as ELL.<br /> <br /> = Light linear logic =<br /> We present the intuitionistic version of ''light linear logic'' LLL, without additive connectives. The language of formulas is:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \pg{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma, \Delta\vdash A}<br /> \LabelRule{\pg }<br /> \UnaRule{\oc{\Gamma}, \pg \Delta\vdash\pg{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> In the <math>(\oc)</math> rule, <math>\Gamma</math> must contain ''at most one'' formula.<br /> <br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> and <math>(\pg)</math> rules in a branch of <math>\pi</math>.<br /> <br /> <br /> {{Theorem|If <math>\pi</math> 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 <br /> <math> O((d+1)|\pi|^{2^{d+1}})</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> The class FP is the class of functions on binary lists which are computable in polynomial time on a Turing machine.<br /> <br /> {{Theorem|The class of functions on binary lists representable in LLL is exactly FP.<br /> }}<br /> <br /> In the literature one also often considers the ''affine'' variant of LLL, called ''light affine logic'', LAL.<br /> <br /> <br /> = Soft linear logic =<br /> We consider the intuitionistic version of ''soft linear logic'', SLL.<br /> <br /> The language of formulas is the same one as that of ILL:<br /> <math><br /> 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 <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,A^{(n)}\vdash C}<br /> \LabelRule{mplex}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The rule mplex is the ''multiplexing'' rule. In its premise, <math>A^{(n)}</math> stands for<br /> n occurrences of formula <math> A </math>. As particular instances of mplex for <math>n=0</math> and 1 respectively, we get weakening and dereliction:<br /> <br /> <math><br /> \AxRule{\Gamma \vdash C}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,A\vdash C}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> <br /> {{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 <br /> <math> O(|\pi|^d)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> <br /> {{Theorem|The class of functions on binary lists representable in SLL is exactly FP.<br /> }}</div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T18:25:43Z

<p>Patrick Baillot: </p> <hr /> <div>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.<br><br /> 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. <br /> <br /> = Elementary linear logic =<br /> We present here the intuitionistic version of ''elementary linear logic'', ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) [[Intuitionistic linear logic|ILL]]:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for [[Intuitionistic linear logic|ILL]], except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br /> <br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,|\pi|)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> A function f on integers is ''elementary recursive'' if there exists an integer h and a Turing machine <br /> which computes f in time bounded by <math>K(h,n)</math>, where n is the size of the input.<br /> <br /> {{Theorem|The functions representable in ELL are exactly the elementary recursive<br /> functions.<br /> }}<br /> <br /> One also often considers the ''affine'' variant of ELL, called ''elementary affine logic'' EAL, which is defined by adding unrestricted weakening:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{ w L}<br /> \UnaRule{\Gamma,A\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> It enjoys the same properties as ELL.<br /> <br /> = Light linear logic =<br /> We present the intuitionistic version of ''light linear logic'' LLL, without additive connectives. The language of formulas is:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \pg{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma, \Delta\vdash A}<br /> \LabelRule{\pg }<br /> \UnaRule{\oc{\Gamma}, \pg \Delta\vdash\pg{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> In the <math>(\oc)</math> rule, <math>\Gamma</math> must contain ''at most one'' formula.<br /> <br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> and <math>(\pg)</math> rules in a branch of <math>\pi</math>.<br /> <br /> <br /> {{Theorem|If <math>\pi</math> 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 <br /> <math> O((d+1)|\pi|^{2^{d+1}})</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> The class FP is the class of functions on binary lists which are computable in polynomial time on a Turing machine.<br /> <br /> {{Theorem|The class of functions on binary lists representable in LLL is exactly FP.<br /> }}<br /> <br /> In the literature one also often considers the ''affine'' variant of LLL, called ''light affine logic'', LAL.<br /> <br /> <br /> = Soft linear logic =<br /> We consider the intuitionistic version of ''soft linear logic'', SLL.<br /> <br /> The language of formulas is the same one as that of ILL:<br /> <math><br /> 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 <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,A^{(n)}\vdash C}<br /> \LabelRule{mplex}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The rule mplex is the ''multiplexing'' rule. In its premise, <math>A^{(n)}</math> stands for<br /> n occurrences of formula <math> A </math>. As particular instances of mplex for <math>n=0</math> and 1 respectively, we get weakening and dereliction:<br /> <br /> <math><br /> \AxRule{\Gamma \vdash C}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,A\vdash C}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> <br /> {{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 <br /> <math> O(|\pi|^d))</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> <br /> {{Theorem|The class of functions on binary lists representable in SLL is exactly FP.<br /> }}</div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T18:22:29Z

<p>Patrick Baillot: </p> <hr /> <div>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.<br><br /> 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. <br /> <br /> = Elementary linear logic =<br /> We present here the intuitionistic version of ''elementary linear logic'', ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) [[Intuitionistic linear logic|ILL]]:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for [[Intuitionistic linear logic|ILL]], except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br /> <br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,|\pi|)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> A function f on integers is ''elementary recursive'' if there exists an integer h and a Turing machine <br /> which computes f in time bounded by <math>K(h,n)</math>, where n is the size of the input.<br /> <br /> {{Theorem|The functions representable in ELL are exactly the elementary recursive<br /> functions.<br /> }}<br /> <br /> One also often considers the ''affine'' variant of ELL, called ''elementary affine logic'' EAL, which is defined by adding unrestricted weakening:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{ w L}<br /> \UnaRule{\Gamma,A\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> It enjoys the same properties as ELL.<br /> <br /> = Light linear logic =<br /> We present the intuitionistic version of ''light linear logic'' LLL, without additive connectives. The language of formulas is:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \pg{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma, \Delta\vdash A}<br /> \LabelRule{\pg }<br /> \UnaRule{\oc{\Gamma}, \pg \Delta\vdash\pg{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> In the <math>(\oc)</math> rule, <math>\Gamma</math> must contain ''at most one'' formula.<br /> <br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> and <math>(\pg)</math> rules in a branch of <math>\pi</math>.<br /> <br /> <br /> {{Theorem|If <math>\pi</math> 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 <br /> <math> O((d+1)|\pi|^{2^{d+1}})</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> The class FP is the class of functions on binary lists which are computable in polynomial time on a Turing machine.<br /> <br /> {{Theorem|The class of functions on binary lists representable in LLL is exactly FP.<br /> }}<br /> <br /> In the literature one also often considers the ''affine'' variant of LLL, called ''light affine logic'' LAL.<br /> <br /> <br /> = Soft linear logic =<br /> We consider the intuitionistic version of ''soft linear logic'', SLL.<br /> <br /> The language of formulas is the same one as that of ILL:<br /> <math><br /> 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 <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,A^{(n)}\vdash C}<br /> \LabelRule{mplex}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The rule mplex is the ''multiplexing'' rule. In its premise, <math>A^{(n)}</math> stands for<br /> n occurrences of formula <math> A </math>. As particular instances of mplex for <math>n=0</math> and 1 respectively, we get weakening and dereliction:<br /> <br /> <math><br /> \AxRule{\Gamma \vdash C}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,A\vdash C}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> <br /> {{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 <br /> <math> O(|\pi|^d))</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> <br /> {{Theorem|The class of functions on binary lists representable in SLL is exactly FP.<br /> }}</div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T18:21:40Z

<p>Patrick Baillot: </p> <hr /> <div>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.<br><br /> 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. <br /> <br /> = Elementary linear logic =<br /> We present here the intuitionistic version of ''elementary linear logic'', ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) [[Intuitionistic linear logic|ILL]]:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br /> <br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,|\pi|)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> A function f on integers is ''elementary recursive'' if there exists an integer h and a Turing machine <br /> which computes f in time bounded by <math>K(h,n)</math>, where n is the size of the input.<br /> <br /> {{Theorem|The functions representable in ELL are exactly the elementary recursive<br /> functions.<br /> }}<br /> <br /> One also often considers the ''affine'' variant of ELL, called ''elementary affine logic'' EAL, which is defined by adding unrestricted weakening:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{ w L}<br /> \UnaRule{\Gamma,A\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> It enjoys the same properties as ELL.<br /> <br /> = Light linear logic =<br /> We present the intuitionistic version of ''light linear logic'' LLL, without additive connectives. The language of formulas is:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \pg{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma, \Delta\vdash A}<br /> \LabelRule{\pg }<br /> \UnaRule{\oc{\Gamma}, \pg \Delta\vdash\pg{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> In the <math>(\oc)</math> rule, <math>\Gamma</math> must contain ''at most one'' formula.<br /> <br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> and <math>(\pg)</math> rules in a branch of <math>\pi</math>.<br /> <br /> <br /> {{Theorem|If <math>\pi</math> 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 <br /> <math> O((d+1)|\pi|^{2^{d+1}})</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> The class FP is the class of functions on binary lists which are computable in polynomial time on a Turing machine.<br /> <br /> {{Theorem|The class of functions on binary lists representable in LLL is exactly FP.<br /> }}<br /> <br /> In the literature one also often considers the ''affine'' variant of LLL, called ''light affine logic'' LAL.<br /> <br /> <br /> = Soft linear logic =<br /> We consider the intuitionistic version of ''soft linear logic'', SLL.<br /> <br /> The language of formulas is the same one as that of ILL:<br /> <math><br /> 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 <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,A^{(n)}\vdash C}<br /> \LabelRule{mplex}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The rule mplex is the ''multiplexing'' rule. In its premise, <math>A^{(n)}</math> stands for<br /> n occurrences of formula <math> A </math>. As particular instances of mplex for <math>n=0</math> and 1 respectively, we get weakening and dereliction:<br /> <br /> <math><br /> \AxRule{\Gamma \vdash C}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,A\vdash C}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> <br /> {{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 <br /> <math> O(|\pi|^d))</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> <br /> {{Theorem|The class of functions on binary lists representable in SLL is exactly FP.<br /> }}</div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T18:15:45Z

<p>Patrick Baillot: </p> <hr /> <div>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.<br><br /> 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. <br /> <br /> = Elementary linear logic =<br /> We present here the intuitionistic version of ''elementary linear logic'', ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) ILL:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br /> <br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,|\pi|)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> A function f on integers is ''elementary recursive'' if there exists an integer h and a Turing machine <br /> which computes f in time bounded by <math>K(h,n)</math>, where n is the size of the input.<br /> <br /> {{Theorem|The functions representable in ELL are exactly the elementary recursive<br /> functions.<br /> }}<br /> <br /> One also often considers the ''affine'' variant of ELL, called ''elementary affine logic'' EAL, which is defined by adding unrestricted weakening:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{ w L}<br /> \UnaRule{\Gamma,A\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> It enjoys the same properties as ELL.<br /> <br /> = Light linear logic =<br /> We present the intuitionistic version of ''light linear logic'' LLL, without additive connectives. The language of formulas is:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \pg{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma, \Delta\vdash A}<br /> \LabelRule{\pg }<br /> \UnaRule{\oc{\Gamma}, \pg \Delta\vdash\pg{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> In the <math>(\oc)</math> rule, <math>\Gamma</math> must contain ''at most one'' formula.<br /> <br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> and <math>(\pg)</math> rules in a branch of <math>\pi</math>.<br /> <br /> <br /> {{Theorem|If <math>\pi</math> 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 <br /> <math> O((d+1)|\pi|^{2^{d+1}})</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> The class FP is the class of functions on binary lists which are computable in polynomial time on a Turing machine.<br /> <br /> {{Theorem|The class of functions on binary lists representable in LLL is exactly FP.<br /> }}<br /> <br /> In the literature one also often considers the ''affine'' variant of LLL, called ''light affine logic'' LAL.<br /> <br /> <br /> = Soft linear logic =<br /> We consider the intuitionistic version of ''soft linear logic'', SLL.<br /> <br /> The language of formulas is the same one as that of ILL:<br /> <math><br /> 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 <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,A^{(n)}\vdash C}<br /> \LabelRule{mplex}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The rule mplex is the ''multiplexing'' rule. In its premise, <math>A^{(n)}</math> stands for<br /> n occurrences of formula <math> A </math>. As particular instances of mplex for <math>n=0</math> and 1 respectively, we get weakening and dereliction:<br /> <br /> <math><br /> \AxRule{\Gamma \vdash C}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,A\vdash C}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> <br /> {{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 <br /> <math> O(|\pi|^d))</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> <br /> {{Theorem|The class of functions on binary lists representable in SLL is exactly FP.<br /> }}</div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T18:14:31Z

<p>Patrick Baillot: </p> <hr /> <div>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.<br><br /> 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. <br /> <br /> = Elementary linear logic =<br /> We present here the intuitionistic version of ''elementary linear logic'', ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) ILL:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br /> <br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,|\pi|)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> A function f on integers is ''elementary recursive'' if there exists an integer h and a Turing machine <br /> which computes f in time bounded by <math>K(h,n)</math>, where n is the size of the input.<br /> <br /> {{Theorem|The functions representable in ELL are exactly the elementary recursive<br /> functions.<br /> }}<br /> <br /> One also often considers the ''affine'' variant of ELL, called ''elementary affine logic'' EAL, which is defined by adding unrestricted weakening:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{ w L}<br /> \UnaRule{\Gamma,A\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> It enjoys the same properties as ELL.<br /> <br /> = Light linear logic =<br /> We present the intuitionistic version of ''light linear logic'' LLL, without additive connectives. The language of formulas is:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \pg{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma, \Delta\vdash A}<br /> \LabelRule{\pg }<br /> \UnaRule{\oc{\Gamma}, \pg \Delta\vdash\pg{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> In the <math>(\oc)</math> rule, <math>\Gamma</math> must contain ''at most one'' formula.<br /> <br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> and <math>(\pg)</math> rules in a branch of <math>\pi</math>.<br /> <br /> <br /> {{Theorem|If <math>\pi</math> 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 <br /> <math> O((d+1)|\pi|^{2^{d+1}})</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> The class FP is the class of functions on binary lists which are computable in polynomial time on a Turing machine.<br /> <br /> {{Theorem|The class of functions on binary lists representable in LLL is exactly FP.<br /> }}<br /> <br /> In the literature one also often considers the ''affine'' variant of LLL, called ''light affine logic'' LAL.<br /> <br /> <br /> = Soft linear logic =<br /> We consider the intuitionistic version of ''soft linear logic'', SLL.<br /> <br /> The language of formulas is the same one as that of ILL:<br /> <math><br /> 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 <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,A^{(n)}\vdash C}<br /> \LabelRule{mplex}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The rule mplex is the ''multiplexing'' rule. In its premise, <math>A^{(n)}</math> stands for<br /> n occurrences of formula <math> A </math>. As particular instances of mplex for <math>n=0</math> and 1 respectively, we get weakening and dereliction:<br /> <br /> <math><br /> \AxRule{\Gamma \vdash C}<br /> \LabelRule{mplex}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,A\vdash C}<br /> \LabelRule{mplex}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> <br /> {{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 <br /> <math> O(|\pi|^d))</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}</div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T18:09:52Z

<p>Patrick Baillot: </p> <hr /> <div>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.<br><br /> 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. <br /> <br /> = Elementary linear logic =<br /> We present here the intuitionistic version of ''elementary linear logic'', ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) ILL:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br /> <br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,|\pi|)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> A function f on integers is ''elementary recursive'' if there exists an integer h and a Turing machine <br /> which computes f in time bounded by <math>K(h,n)</math>, where n is the size of the input.<br /> <br /> {{Theorem|The functions representable in ELL are exactly the elementary recursive<br /> functions.<br /> }}<br /> <br /> One also often considers the ''affine'' variant of ELL, called ''elementary affine logic'' EAL, which is defined by adding unrestricted weakening:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{ w L}<br /> \UnaRule{\Gamma,A\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> It enjoys the same properties as ELL.<br /> <br /> = Light linear logic =<br /> We present the intuitionistic version of ''light linear logic'' LLL, without additive connectives. The language of formulas is:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \pg{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma, \Delta\vdash A}<br /> \LabelRule{\pg }<br /> \UnaRule{\oc{\Gamma}, \pg \Delta\vdash\pg{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> In the <math>(\oc)</math> rule, <math>\Gamma</math> must contain ''at most one'' formula.<br /> <br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> and <math>(\pg)</math> rules in a branch of <math>\pi</math>.<br /> <br /> <br /> {{Theorem|If <math>\pi</math> 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 <br /> <math> O((d+1)|\pi|^{2^{d+1}})</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> The class FP is the class of functions on binary lists which are computable in polynomial time on a Turing machine.<br /> <br /> {{Theorem|The class of functions on binary lists representable in LLL is exactly FP.<br /> }}<br /> <br /> In the literature one also often considers the ''affine'' variant of LLL, called ''light affine logic'' LAL.<br /> <br /> <br /> = Soft linear logic =<br /> We consider the intuitionistic version of ''soft linear logic'', SLL.<br /> <br /> The language of formulas is the same one as that of ILL:<br /> <math><br /> 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 <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,A^{n}\vdash C}<br /> \LabelRule{mplex}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> <br /> {{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 <br /> <math> O(|\pi|^d))</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}</div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T17:55:52Z

<p>Patrick Baillot: </p> <hr /> <div>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.<br><br /> 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. <br /> <br /> = Elementary linear logic =<br /> We present here the intuitionistic version of ''elementary linear logic'', ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) ILL:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br /> <br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,|\pi|)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> A function f on integers is ''elementary recursive'' if there exists an integer h and a Turing machine <br /> which computes f in time bounded by <math>K(h,n)</math>, where n is the size of the input.<br /> <br /> {{Theorem|The functions representable in ELL are exactly the elementary recursive<br /> functions.<br /> }}<br /> <br /> One also often considers the ''affine'' variant of ELL, called ''elementary affine logic'' EAL, which is defined by adding unrestricted weakening:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{ w L}<br /> \UnaRule{\Gamma,A\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> It enjoys the same properties as ELL.<br /> <br /> = Light linear logic =<br /> We present the intuitionistic version of ''light linear logic'' LLL, without additive connectives. The language of formulas is:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \pg{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma, \Delta\vdash A}<br /> \LabelRule{\pg }<br /> \UnaRule{\oc{\Gamma}, \pg \Delta\vdash\pg{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> In the <math>(\oc)</math> rule, <math>\Gamma</math> must contain ''at most one'' formula.<br /> <br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> and <math>(\pg)</math> rules in a branch of <math>\pi</math>.<br /> <br /> <br /> {{Theorem|If <math>\pi</math> 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 <br /> <math> O((d+1)|\pi|^{2^{d+1}})</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> The class FP is the class of functions on binary lists which are computable in polynomial time on a Turing machine.<br /> <br /> {{Theorem|The class of functions on binary lists representable in LLL is exactly FP.<br /> }}<br /> <br /> In the literature one also often considers the ''affine'' variant of LLL, called ''light affine logic'' LAL.</div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T17:55:24Z

<p>Patrick Baillot: </p> <hr /> <div>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.<br><br /> 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. <br /> <br /> = Elementary linear logic =<br /> We present here the intuitionistic version of ''elementary linear logic'', ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) ILL:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br /> <br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,|\pi|)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> A function f on integers is ''elementary recursive'' if there exists an integer h and a Turing machine <br /> which computes f in time bounded by <math>K(h,n)</math>, where n is the size of the input.<br /> <br /> {{Theorem|The functions representable in ELL are exactly the elementary recursive<br /> functions.<br /> }}<br /> <br /> One also often considers the ''affine'' variant of ELL, called ''elementary affine logic'' EAL, which is defined by adding unrestricted weakening:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{ w L}<br /> \UnaRule{\Gamma,A\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> It enjoys the same properties as ELL.<br /> <br /> = Light linear logic =<br /> We present the intuitionistic version of ''light linear logic'' LLL, without additive connectives. The language of formulas is:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \pg{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma, \Delta\vdash A}<br /> \LabelRule{\pg }<br /> \UnaRule{\oc{\Gamma}, \pg \Delta\vdash\pg{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> In the <math>(\oc)</math> rule, <math>\Gamma</math> must contain ''at most one'' formula.<br /> <br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> and <math>(\pg)</math> rules in a branch of <math>\pi</math>.<br /> <br /> <br /> {{Theorem|If <math>\pi</math> 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 <br /> <math> O((d+1)|\pi|^{2^{d+1}})</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> The class FP is the class of functions on binary lists which are computable in polynomial time on a Turing machine.<br /> <br /> {{Theorem|The class of functions on binary lists representable in LLL is exactly FP.<br /> }}<br /> <br /> In the literature one also often considers the ''affine'' variant of LLL, called ''light affine logic'' LAL.</div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T17:50:45Z

<p>Patrick Baillot: </p> <hr /> <div>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.<br><br /> 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. <br /> <br /> = Elementary linear logic =<br /> We present here the intuitionistic version of ''elementary linear logic'', ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) ILL:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br /> <br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,|\pi|)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> A function f on integers is ''elementary recursive'' if there exists an integer h and a Turing machine <br /> which computes f in time bounded by <math>K(h,n)</math>, where n is the size of the input.<br /> <br /> {{Theorem|The functions representable in ELL are exactly the elementary recursive<br /> functions.<br /> }}<br /> <br /> One also often considers the ''affine'' variant of ELL, called ''elementary affine logic'' EAL, which is defined by adding unrestricted weakening:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{ w L}<br /> \UnaRule{\Gamma,A\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> It enjoys the same properties as ELL.<br /> <br /> = Light linear logic =<br /> We present the intuitionistic version of ''light linear logic'' LLL, without additive connectives. The language of formulas is:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \pg{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma, \Delta\vdash A}<br /> \LabelRule{\pg }<br /> \UnaRule{\oc{\Gamma}, \pg \Delta\vdash\pg{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> In the <math>(\oc)</math> rule, <math>\Gamma</math> must contain ''at most one'' formula.<br /> <br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> and <math>(\pg)</math> rules in a branch of <math>\pi</math>.<br /> <br /> <br /> {{Theorem|If <math>\pi</math> 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 <br /> <math> O((d+1)|\pi|^{2^{d+1}})</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}</div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T17:46:56Z

<p>Patrick Baillot: </p> <hr /> <div>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.<br><br /> 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. <br /> <br /> = Elementary linear logic =<br /> We present here the intuitionistic version of ''elementary linear logic'', ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) ILL:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br /> <br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,|\pi|)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> A function f on integers is ''elementary recursive'' if there exists an integer h and a Turing machine <br /> which computes f in time bounded by <math>K(h,n)</math>, where n is the size of the input.<br /> <br /> {{Theorem|The functions representable in ELL are exactly the elementary recursive<br /> functions.<br /> }}<br /> <br /> One also often considers the ''affine'' variant of ELL, called ''elementary affine logic'' EAL, which is defined by adding unrestricted weakening:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{ w L}<br /> \UnaRule{\Gamma,A\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> It enjoys the same properties as ELL.<br /> <br /> = Light linear logic =<br /> We present the intuitionistic version of ''light linear logic'' LLL, without additive connectives. The language of formulas is:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \pg{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma, \Delta\vdash A}<br /> \LabelRule{\pg }<br /> \UnaRule{\oc{\Gamma}, \pg \Delta\vdash\pg{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> In the <math>(\oc)</math> rule, <math>\Gamma</math> must contain ''at most one'' formula.<br /> <br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> and <math>(\pg)</math> rules in a branch of <math>\pi</math>.</div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T17:44:54Z

<p>Patrick Baillot: /* Light linear logic */</p> <hr /> <div>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.<br><br /> 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. <br /> <br /> = Elementary linear logic =<br /> We present here the intuitionistic version of ''elementary linear logic'', ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) ILL:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br /> <br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,|\pi|)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> A function f on integers is ''elementary recursive'' if there exists an integer h and a Turing machine <br /> which computes f in time bounded by <math>K(h,n)</math>, where n is the size of the input.<br /> <br /> {{Theorem|The functions representable in ELL are exactly the elementary recursive<br /> functions.<br /> }}<br /> <br /> One also often considers the ''affine'' variant of ELL, called ''elementary affine logic'' EAL, which is defined by adding unrestricted weakening:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{ w L}<br /> \UnaRule{\Gamma,A\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> It enjoys the same properties as ELL.<br /> <br /> = Light linear logic =<br /> We present the intuitionistic version of ''light linear logic'' LLL, without additive connectives. The language of formulas is:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \pg{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma, \Delta\vdash A}<br /> \LabelRule{\pg }<br /> \UnaRule{\oc{\Gamma}, \pg \Delta\vdash\pg{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> In the <math>(\oc)</math> rule, <math>\Gamma</math> must contain ''at most one'' formula.</div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T17:44:23Z

<p>Patrick Baillot: /* Light linear logic */</p> <hr /> <div>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.<br><br /> 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. <br /> <br /> = Elementary linear logic =<br /> We present here the intuitionistic version of ''elementary linear logic'', ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) ILL:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br /> <br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,|\pi|)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> A function f on integers is ''elementary recursive'' if there exists an integer h and a Turing machine <br /> which computes f in time bounded by <math>K(h,n)</math>, where n is the size of the input.<br /> <br /> {{Theorem|The functions representable in ELL are exactly the elementary recursive<br /> functions.<br /> }}<br /> <br /> One also often considers the ''affine'' variant of ELL, called ''elementary affine logic'' EAL, which is defined by adding unrestricted weakening:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{ w L}<br /> \UnaRule{\Gamma,A\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> It enjoys the same properties as ELL.<br /> <br /> = Light linear logic =<br /> We present the intuitionistic version of ''light linear logic'' LLL, without additive connectives. The language of formulas is:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \pg{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma, \Delta\vdash A}<br /> \LabelRule{\pg }<br /> \UnaRule{\oc{\Gamma}, \pg \Delta\vdash\pg{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> In the <math>(\oc)</math> rule, <math>\Gamma</math> must contain ''at most one'' formula.</div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T17:43:35Z

<p>Patrick Baillot: /* Elementary linear logic */</p> <hr /> <div>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.<br><br /> 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. <br /> <br /> = Elementary linear logic =<br /> We present here the intuitionistic version of ''elementary linear logic'', ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) ILL:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br /> <br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,|\pi|)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> A function f on integers is ''elementary recursive'' if there exists an integer h and a Turing machine <br /> which computes f in time bounded by <math>K(h,n)</math>, where n is the size of the input.<br /> <br /> {{Theorem|The functions representable in ELL are exactly the elementary recursive<br /> functions.<br /> }}<br /> <br /> One also often considers the ''affine'' variant of ELL, called ''elementary affine logic'' EAL, which is defined by adding unrestricted weakening:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{ w L}<br /> \UnaRule{\Gamma,A\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> It enjoys the same properties as ELL.<br /> <br /> = Light linear logic =<br /> We present the intuitionistic version of ''light linear logic'' LLL, without additive connectives. The language of formulas is:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \pg{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma, \Delta\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}, \pg \Delta\vdash\pg{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> In the <math>(\oc)<\math> rule, <math>\Gamma<\math> must contain ''at most one'' formula.</div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T17:32:48Z

<p>Patrick Baillot: </p> <hr /> <div>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.<br><br /> 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. <br /> <br /> = Elementary linear logic =<br /> We present here the intuitionistic version of ''elementary linear logic'', ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) ILL:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br /> <br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,|\pi|)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> A function f on integers is ''elementary recursive'' if there exists an integer h and a Turing machine <br /> which computes f in time bounded by <math>K(h,n)</math>, where n is the size of the input.<br /> <br /> {{Theorem|The functions representable in ELL are exactly the elementary recursive<br /> functions.<br /> }}<br /> <br /> One also often considers the ''affine'' variant of ELL, called ''elementary affine logic'' EAL, which is defined by adding unrestricted weakening:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{ w L}<br /> \UnaRule{\Gamma,A\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> It enjoys the same properties as ELL.</div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T17:32:19Z

<p>Patrick Baillot: </p> <hr /> <div>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.<br><br /> 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. <br /> <br /> = Elementary linear logic =<br /> We present here the intuitionistic version of ''elementary linear logic'', ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) ILL:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br /> <br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,|\pi|)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> A function f on integers is ''elementary recursive'' if there exists an integer h and a Turing machine <br /> which computes f in time bounded by <math>K(h,n)</math>, where n is the size of the input.<br /> <br /> {{Theorem|The functions representable in ELL are exactly the elementary recursive<br /> functions.<br /> }}<br /> <br /> One also often considers the ''affine'' variant of ELL, called ''elementary affine logic'' EAL, which is defined by adding unrestricted weakening:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{ w L}<br /> \UnaRule{\Gamma,A\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> It enjoys the same properties as ELL.</div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T17:27:17Z

<p>Patrick Baillot: /* Elementary linear logic */</p> <hr /> <div>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.<br><br /> 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. <br /> <br /> == Elementary linear logic ==<br /> We present here the intuitionistic version of elementary linear logic, ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) ILL:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br /> <br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br /> <br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,|\pi|)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> <br /> A function f on integers is ''elementary recursive'' if there exists an integer h and a Turing machine <br /> which computes f in time bounded by <math>K(h,n)</math>, where n is the size of the input.<br /> <br /> {{Theorem|The functions representable in ELL are exactly the elementary recursive<br /> functions.<br /> }}</div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T17:26:24Z

<p>Patrick Baillot: /* Elementary linear logic */</p> <hr /> <div>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.<br><br /> 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. <br /> <br /> == Elementary linear logic ==<br /> We present here the intuitionistic version of elementary linear logic, ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) ILL:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> <br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br><br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br><br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,|\pi|)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br><br /> A function f on integers is ''elementary recursive'' if there exists an integer h and a Turing machine <br /> which computes f in time bounded by <math>K(h,n)</math>, where n is the size of the input.<br><br /> {{Theorem|The functions representable in ELL are exactly the elementary recursive<br /> functions.<br /> }}<br></div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T17:20:25Z

<p>Patrick Baillot: /* Elementary linear logic */</p> <hr /> <div>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.<br><br /> 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. <br /> <br /> == Elementary linear logic ==<br /> We present here the intuitionistic version of elementary linear logic, ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) ILL:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br><br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br><br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br><br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,|\pi|)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br><br /> A function f on integers is ''elementary recursive'' if there exists an integer h and a Turing machine <br /> which computes f in time bounded by <math>K(h,n)</math>, where n is the size of the input.<br><br /> {{Theorem|The functions representable in ELL are exactly the elementary recursive<br /> functions.<br /> }}<br></div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T17:20:03Z

<p>Patrick Baillot: /* Elementary linear logic */</p> <hr /> <div>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.<br><br /> 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. <br /> <br /> == Elementary linear logic ==<br /> We present here the intuitionistic version of elementary linear logic, ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) ILL:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br><br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br><br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br><br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,|\pi|)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br><br /> A function f on integers is ''elementary recursive'' if there exists an integer h and a Turing machine <br /> which computes f in time bounded by <math>K(h,n)</math>, where n is the size of the input.<br /> {{Theorem|The functions representable in ELL are exactly the elementary recursive<br /> functions.<br /> }}<br></div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T17:18:29Z

<p>Patrick Baillot: /* Elementary linear logic */</p> <hr /> <div>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.<br><br /> 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. <br /> <br /> == Elementary linear logic ==<br /> We present here the intuitionistic version of elementary linear logic, ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) ILL:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br><br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br><br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br><br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,|\pi|)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> A function f on integers is ''elementary recursive'' if there exists an integer h and a Turing machine <br /> which computes f in time bounded by <math>K(h,n)</math>, where n is the size of the input.</div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T17:17:57Z

<p>Patrick Baillot: /* Elementary linear logic */</p> <hr /> <div>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.<br><br /> 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. <br /> <br /> == Elementary linear logic ==<br /> We present here the intuitionistic version of elementary linear logic, ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) ILL:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br><br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br><br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br><br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,|\pi|)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> A function f on integers is ''elementary recursive'' if there exists an integer h and a Turing machine <br /> which computes f in time bounded by <math>K(h,n)</math>.</div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T17:17:15Z

<p>Patrick Baillot: /* Elementary linear logic */</p> <hr /> <div>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.<br><br /> 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. <br /> <br /> == Elementary linear logic ==<br /> We present here the intuitionistic version of elementary linear logic, ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) ILL:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br><br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br><br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br><br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,|\pi|)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}<br /> A function f is ''elementary recursive''<br /> if there exists an integer h and a Turing machine <br /> which computes <br /> f in time bounded by <math>K(h,n)</math>.</div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T17:12:41Z

<p>Patrick Baillot: /* Elementary linear logic */</p> <hr /> <div>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.<br><br /> 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. <br /> <br /> == Elementary linear logic ==<br /> We present here the intuitionistic version of elementary linear logic, ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) ILL:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br><br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br><br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br><br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,|\pi|)</math> steps, where <math>|\pi|</math>is the size of <math>\pi</math>.}}</div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T17:09:42Z

<p>Patrick Baillot: /* Elementary linear logic */</p> <hr /> <div>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.<br><br /> 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. <br /> <br /> == Elementary linear logic ==<br /> We present here the intuitionistic version of elementary linear logic, ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) ILL:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br><br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br><br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.<br><br /> {{Theorem|If <math>\pi</math> 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 <math> K(d+1,\pi)</math> steps.}}</div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T17:03:18Z

<p>Patrick Baillot: </p> <hr /> <div>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.<br><br /> 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. <br /> <br /> == Elementary linear logic ==<br /> We present here the intuitionistic version of elementary linear logic, ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) ILL:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br><br /> The ''depth'' of a derivation <math>\pi</math> is the maximum number of<br /> <math>(\oc)</math> rules in a branch of <math>\pi</math>.<br><br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.</div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T16:56:23Z

<p>Patrick Baillot: </p> <hr /> <div>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.<br><br /> 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. <br /> <br /> == Elementary linear logic ==<br /> We present here the intuitionistic version of elementary linear logic, ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) ILL:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br><br /> We consider the function <math>K(.,.)</math> defined by:<br><br /> <math>K(0,n)=n, \quad K(k+1,n)=2^{K(k,n)}</math>.</div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T16:50:38Z

<p>Patrick Baillot: </p> <hr /> <div>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.<br><br /> 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. <br /> <br /> == Elementary linear logic ==<br /> We present here the intuitionistic version of elementary linear logic, ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) ILL:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math><br /> 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>.</div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T16:33:45Z

<p>Patrick Baillot: /* Elementary linear logic */</p> <hr /> <div>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.<br><br /> 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. <br /> <br /> == Elementary linear logic ==<br /> We present here the intuitionistic version of elementary linear logic, ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) ILL:<br /> <br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math><br /> <br><br /> The sequent calculus rules are the same ones as for ILL, except for the rules<br /> dealing with the exponential connectives:<br /> <br /> <math><br /> \AxRule{\Gamma\vdash A}<br /> \LabelRule{\oc }<br /> \UnaRule{\oc{\Gamma}\vdash\oc{A}}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma,\oc{A},\oc{A}\vdash C}<br /> \LabelRule{\oc c L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> \qquad<br /> \AxRule{\Gamma\vdash C}<br /> \LabelRule{\oc w L}<br /> \UnaRule{\Gamma,\oc{A}\vdash C}<br /> \DisplayProof<br /> </math></div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T16:26:15Z

<p>Patrick Baillot: </p> <hr /> <div>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.<br><br /> 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. <br /> <br /> == Elementary linear logic ==<br /> We present here the intuitionistic version of elementary linear logic, ELL. Moreover we restrict to the fragment without additive connectives. <br> The language of formulas is the same one as that of (multiplicative) ILL:<br><br /> <math><br /> A ::= X \mid A\tens A \mid A\limp A \mid \oc{A} \mid \forall X A <br /> </math></div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T16:13:07Z

<p>Patrick Baillot: </p> <hr /> <div>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.<br /> 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. <br /> <br /> \section{Elementary linear logic}<br /> \section{Light linear logic}</div>

Patrick Baillot http://140-77-166-78.cprapid.com/mediawiki/index.php/Light_linear_logics Light linear logics 2009-03-19T16:11:52Z

<p>Patrick Baillot: New page: 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 th...</p> <hr /> <div>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.<br /> <br /> Light linear logics are one of the approaches used in \textit{implicit computational complexity}, the research area studying the computational complexity of programs without referring to external measuring conditions or particular machine models. <br /> <br /> \section{Elementary linear logic}<br /> \section{Light linear logic}</div>

Patrick Baillot