Pierre-Marie Pédrot: propaganda for system L

2012-04-22T02:48:02Z

propaganda for system L

New page

'''System L''' is a family of syntax for a variety of variants of linear logic, inspired from classical calculi such as <math>\bar\lambda\mu\tilde\mu</math>-calculus. These, in turn, stem from the study of abstract machines for <math>\lambda</math>-calculus. In this realm, [[Polarized linear logic|polarization]] and [[focalization]] are features that appear naturally. Positives are typically values, and negatives pattern-matches. Contraction and weakening are implicit.

We present here a system for explicitely polarized and focalized linear logic. Polarization classifies terms and types between positive and negative; focalization separates values from non-values.

== Definitions ==

Positive types: <math>P ::= 1 \mid P_1 \otimes P_2 \mid 0 \mid P_1 \oplus P_2 \mid \shpos N \mid \oc N</math>

Negative types: <math>N ::= \bot \mid N_1 \parr N_2 \mid \top \mid N_1 \with N_2 \mid \shneg P \mid \wn P</math>

Positive values: <math>v^+ ::= x^+ \mid () \mid (v_1^+, v_2^+) \mid inl(v^+) \mid inr(v^+) \mid \shpos t^- \mid \mu(\wn x^+).c</math>

Positive terms: <math>t^+ ::= v^+ \mid \mu x^-.c</math>

Negative terms: <math>t^- ::= x^- \mid \mu x^+.c \mid \mu().c \mid \mu(x^+, y^+).c \mid \mu [\cdot] \mid \mu[inl(x^+).c_1 \mid inr(y^+).c_2] \mid \mu(\shpos x^-).c \mid \wn v^+</math>

Commands: <math>c ::= \langle t^+ \mid t^- \rangle</math>

== Typing ==

There are as many typing sequents classes as there are terms classes. Typing of positive values corresponds to focalized sequents, and commands are cuts.

Positive values: sequents are of the form <math>\vdash \Gamma :: v^+ : P</math>.

<math>
\LabelRule{\rulename{ax}^+}
\NulRule{\vdash x^+:P\orth :: x^+: P}
\DisplayProof
</math>

<math>
\LabelRule{1}
\NulRule{\vdash \ :: () : 1}
\DisplayProof
</math>

<math>
\AxRule{\vdash \Gamma_1 :: v_1^+ : P_1}
\AxRule{\vdash \Gamma_2 :: v_2^+ : P_2}
\LabelRule{\rulename{\otimes}}
\BinRule{\vdash\Gamma_1, \Gamma_2 :: (v_1^+, v_2^+) : P_1\otimes P_2}
\DisplayProof
</math>

<math>
\AxRule{\vdash \Gamma :: v^+ : P_1}
\LabelRule{\rulename{\oplus_1}}
\UnaRule{\vdash\Gamma :: inl(v^+) : P_1\oplus P_2}
\DisplayProof
\qquad
\AxRule{\vdash \Gamma :: v^+ : P_2}
\LabelRule{\rulename{\oplus_2}}
\UnaRule{\vdash\Gamma :: inr(v^+) : P_1\oplus P_2}
\DisplayProof
</math>

<math>
\AxRule{\vdash \Gamma \mid t^- : N}
\LabelRule{\shpos}
\UnaRule{\vdash\Gamma :: \shpos t^- : \shpos N}
\DisplayProof
</math>

<math>
\AxRule{c \vdash \wn\Gamma, x^+ : N}
\LabelRule{\oc}
\UnaRule{\vdash\wn\Gamma :: \mu(\wn x^+).c : \oc N}
\DisplayProof
</math>

Positive terms: sequents are of the form <math>\vdash\Gamma\mid t^+:P</math>.

<math>
\AxRule{\vdash \Gamma :: v^+ : P}
\LabelRule{\rulename{foc}}
\UnaRule{\vdash\Gamma \mid v^+ : P}
\DisplayProof
</math>

<math>
\AxRule{c \vdash \Gamma, x^- : P}
\LabelRule{\rulename{\mu^-}}
\UnaRule{\vdash\Gamma \mid\mu x^-.c : P}
\DisplayProof
</math>

Negative terms: sequents are of the form <math>\vdash\Gamma\mid t^-:N</math>.

<math>
\LabelRule{\rulename{ax}^-}
\NulRule{\vdash x^-:N\orth \mid x^-: N}
\DisplayProof
</math>

<math>
\AxRule{c\vdash \Gamma, x^+: N}
\LabelRule{\mu^+}
\UnaRule{\vdash\Gamma \mid \mu x^+.c : N}
\DisplayProof
</math>

<math>
\AxRule{c \vdash \Gamma}
\LabelRule{\bot}
\UnaRule{\vdash \Gamma \mid \mu().c : \bot}
\DisplayProof
</math>

<math>
\AxRule{c\vdash \Gamma, x^+: N_1, y^+: N_2}
\LabelRule{\rulename{\parr}}
\UnaRule{\vdash\Gamma \mid \mu(x^+, y^+).c : N_1 \parr N_2}
\DisplayProof
</math>

<math>
\LabelRule{\rulename{\top}}
\NulRule{\vdash \Gamma \mid \mu[\cdot] : \top}
\DisplayProof
</math>

<math>
\AxRule{c_1\vdash \Gamma, x^+:N_1}
\AxRule{c_2\vdash \Gamma, y^+:N_2}
\LabelRule{\rulename{\with}}
\BinRule{\vdash\Gamma \mid \mu[inl(x^+).c_1 \mid inr(y^+).c_2] : N_1 \with N_2}
\DisplayProof
</math>

<math>
\AxRule{c\vdash \Gamma, x^-: P}
\LabelRule{\shneg}
\UnaRule{\vdash\Gamma \mid \mu(\shpos x^-).c : \shneg P}
\DisplayProof
</math>

<math>
\AxRule{\vdash \Gamma :: v^+ : P}
\LabelRule{\wn}
\UnaRule{\vdash\Gamma \mid \wn v^+ : \wn P}
\DisplayProof
</math>

Commands:

<math>
\AxRule{\vdash \Gamma \mid t^+ : P}
\AxRule{\vdash \Delta \mid t^- : P\orth}
\LabelRule{\rulename{cut}}
\BinRule{\langle t^+ \mid t^-\rangle\vdash\Gamma, \Delta}
\DisplayProof
</math>

<math>
\AxRule{c \vdash \Gamma}
\LabelRule{\rulename{wkn}}
\UnaRule{c \vdash\Gamma, x^+: \wn P}
\DisplayProof
</math>

<math>
\AxRule{c \vdash \Gamma, x_1^+:\wn P, x_2^+:\wn P}
\LabelRule{\rulename{ctr}}
\UnaRule{c[x_1^+ := x^+, x_2^+ := x^+] \vdash\Gamma, x^+: \wn P}
\DisplayProof
</math>

== Reduction rules ==

<math>\langle v^+ \mid \mu x^+.c \rangle \rightarrow c[ x^+ := v^+] </math>

<math>\langle \mu x^-.c \mid t^- \rangle \rightarrow c[x^- := t^-] </math>

<math>\langle () \mid \mu().c \rangle \rightarrow c </math>

<math>\langle (v_1^+, v_2^+) \mid \mu(x^+, y^+).c \rangle \rightarrow c[x^+ := v_1^+, y^+ := v_2^+] </math>

<math>\langle inl(v^+) \mid \mu[inl(x^+).c_1 \mid inr(y^+).c_2] \rangle \rightarrow c_1[x^+ := v^+] </math>

<math>\langle inr(v^+) \mid \mu[inl(x^+).c_1 \mid inr(y^+).c_2] \rangle \rightarrow c_2[y^+ := v^+] </math>

<math>\langle \shpos t^- \mid \mu(\shpos x^-).c \rangle \rightarrow c[x^- := t^-] </math>

<math>\langle \mu(\wn x^+).c \mid \wn v^+ \rangle \rightarrow c[x^+ := v^+] </math>

== References ==

* {{BibEntry|bibtype=proceedings|author=Pierre-Louis Curien and Guillaume Munch-Maccagnoni|title=The duality of computation under focus|booktitle=IFIP TCS|year=2010}}

System L - Revision history

Pierre-Marie Pédrot: propaganda for system L