System L

From LLWiki
Revision as of 03:48, 22 April 2012 by Pierre-Marie Pédrot (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

System L is a family of syntax for a variety of variants of linear logic, inspired from classical calculi such as \bar\lambda\mu\tilde\mu-calculus. These, in turn, stem from the study of abstract machines for λ-calculus. In this realm, 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.



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

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

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

Positive terms: t^+ ::= v^+ \mid \mu x^-.c

Negative terms: 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^+

Commands: c ::= \langle t^+ \mid t^- \rangle


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 \vdash \Gamma :: v^+ : P.

\NulRule{\vdash x^+:P\orth :: x^+: P}

\NulRule{\vdash \ :: () : 1}

\AxRule{\vdash \Gamma_1 :: v_1^+ : P_1}
\AxRule{\vdash \Gamma_2 :: v_2^+ : P_2}
\BinRule{\vdash\Gamma_1, \Gamma_2 :: (v_1^+, v_2^+) : P_1\otimes P_2}

\AxRule{\vdash \Gamma :: v^+ : P_1}
\UnaRule{\vdash\Gamma :: inl(v^+) : P_1\oplus P_2}
\AxRule{\vdash \Gamma :: v^+ : P_2}
\UnaRule{\vdash\Gamma :: inr(v^+) : P_1\oplus P_2}

\AxRule{\vdash \Gamma \mid t^- : N}
\UnaRule{\vdash\Gamma :: \shpos t^- : \shpos N}

\AxRule{c \vdash \wn\Gamma, x^+ : N}
\UnaRule{\vdash\wn\Gamma :: \mu(\wn x^+).c : \oc N}

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

\AxRule{\vdash \Gamma :: v^+ : P}
\UnaRule{\vdash\Gamma \mid v^+ : P}

\AxRule{c \vdash \Gamma, x^- : P}
\UnaRule{\vdash\Gamma \mid\mu x^-.c : P}

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

\NulRule{\vdash x^-:N\orth \mid x^-: N}

\AxRule{c\vdash \Gamma, x^+: N}
\UnaRule{\vdash\Gamma \mid \mu x^+.c : N}

\AxRule{c \vdash \Gamma}
\UnaRule{\vdash \Gamma \mid \mu().c : \bot}

\AxRule{c\vdash \Gamma, x^+: N_1, y^+: N_2}
\UnaRule{\vdash\Gamma \mid \mu(x^+, y^+).c : N_1 \parr N_2}

\NulRule{\vdash \Gamma \mid \mu[\cdot] : \top}

\AxRule{c_1\vdash \Gamma, x^+:N_1}
\AxRule{c_2\vdash \Gamma, y^+:N_2}
\BinRule{\vdash\Gamma \mid \mu[inl(x^+).c_1 \mid inr(y^+).c_2] : N_1 \with N_2}

\AxRule{c\vdash \Gamma, x^-: P}
\UnaRule{\vdash\Gamma \mid \mu(\shpos x^-).c : \shneg P}

\AxRule{\vdash \Gamma :: v^+ : P}
\UnaRule{\vdash\Gamma \mid \wn v^+ : \wn P}


\AxRule{\vdash \Gamma \mid t^+ : P}
\AxRule{\vdash \Delta \mid t^- : P\orth}
\BinRule{\langle t^+ \mid t^-\rangle\vdash\Gamma, \Delta}

\AxRule{c \vdash \Gamma}
\UnaRule{c \vdash\Gamma, x^+: \wn P}

\AxRule{c \vdash \Gamma, x_1^+:\wn P, x_2^+:\wn P}
\UnaRule{c[x_1^+ := x^+, x_2^+ := x^+] \vdash\Gamma, x^+: \wn P}

Reduction rules

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

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

\langle () \mid \mu().c \rangle \rightarrow c

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

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

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

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

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


  • Pierre-Louis Curien and Guillaume Munch-Maccagnoni. The duality of computation under focus. 2010.
Personal tools