sysl.tex

\chapter{System L}\label{system-l}

\emph{System L}~\cite{dualitycomputationfocus} 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 \(\lambda\)-calculus. In this realm,
\hyperref[polarized-linear-logic]{polarization} and \hyperref[reversibility-and-focusing]{focusing} 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 focused linear
logic. Polarization classifies terms and types between positive and
negative; focusing separates values from non-values.

\section{Definitions}\label{definitions}

\begin{equation*}
\begin{array}{ll@{\,}l@{\,}l}
\text{Positive types:} & P & ::= & 1 \mid P \otimes P \mid 0 \mid P \oplus P \mid \shpos N \mid \oc N \\
\text{Negative types:} & N & ::= & \bot \mid N \parr N \mid \top \mid N \with N \mid \shneg P \mid \wn P \\
\text{Positive values:} & v^+ & ::= & x^+ \mid () \mid (v_1^+, v_2^+) \mid inl(v^+) \mid inr(v^+) \mid \shpos t^- \mid \mu(\wn x^+).c \\
\text{Positive terms:} & t^+ & ::= & v^+ \mid \mu x^-.c \\
\text{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^+ \\
\text{Commands:} & c & ::= & \langle t^+ \mid t^- \rangle
\end{array}
\end{equation*}

\section{Typing}

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

Positive values: sequents are of the form \(\vdash \Gamma :: v^+ : P\).
\begin{gather*}
\LabelRule{\rulename{ax}^+}
\NulRule{\vdash x^+:P\orth :: x^+: P}
\DisplayProof
\\[2ex]
\LabelRule{1}
\NulRule{\vdash \ :: () : 1}
\DisplayProof
\qquad\qquad
\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
\\[2ex]
\AxRule{\vdash \Gamma :: v^+ : P_1}
\LabelRule{\rulename{\oplus_1}}
\UnaRule{\vdash\Gamma :: inl(v^+) : P_1\oplus P_2}
\DisplayProof
\qquad\qquad
\AxRule{\vdash \Gamma :: v^+ : P_2}
\LabelRule{\rulename{\oplus_2}}
\UnaRule{\vdash\Gamma :: inr(v^+) : P_1\oplus P_2}
\DisplayProof
\\[2ex]
\AxRule{\vdash \Gamma \mid t^- : N}
\LabelRule{\shpos}
\UnaRule{\vdash\Gamma :: \shpos t^- : \shpos N}
\DisplayProof
\qquad\qquad
\AxRule{c \vdash \wn\Gamma, x^+ : N}
\LabelRule{\oc}
\UnaRule{\vdash\wn\Gamma :: \mu(\wn x^+).c : \oc N}
\DisplayProof
\end{gather*}

Positive terms: sequents are of the form \(\vdash\Gamma\mid t^+:P\).
\begin{equation*}
\AxRule{\vdash \Gamma :: v^+ : P}
\LabelRule{\rulename{foc}}
\UnaRule{\vdash\Gamma \mid v^+ : P}
\DisplayProof
\qquad\qquad
\AxRule{c \vdash \Gamma, x^- : P}
\LabelRule{\rulename{\mu^-}}
\UnaRule{\vdash\Gamma \mid\mu x^-.c : P}
\DisplayProof
\end{equation*}

Negative terms: sequents are of the form \(\vdash\Gamma\mid t^-:N\).
\begin{gather*}
\LabelRule{\rulename{ax}^-}
\NulRule{\vdash x^-:N\orth \mid x^-: N}
\DisplayProof
\qquad\qquad
\AxRule{c\vdash \Gamma, x^+: N}
\LabelRule{\mu^+}
\UnaRule{\vdash\Gamma \mid \mu x^+.c : N}
\DisplayProof
\\[2ex]
\AxRule{c \vdash \Gamma}
\LabelRule{\bot}
\UnaRule{\vdash \Gamma \mid \mu().c : \bot}
\DisplayProof
\qquad\qquad
\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
\\[2ex]
\LabelRule{\rulename{\top}}
\NulRule{\vdash \Gamma \mid \mu[\cdot] : \top}
\DisplayProof
\qquad\qquad
\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
\\[2ex]
\AxRule{c\vdash \Gamma, x^-: P}
\LabelRule{\shneg}
\UnaRule{\vdash\Gamma \mid \mu(\shpos x^-).c : \shneg P}
\DisplayProof
\qquad\qquad
\AxRule{\vdash \Gamma :: v^+ : P}
\LabelRule{\wn}
\UnaRule{\vdash\Gamma \mid \wn v^+ : \wn P}
\DisplayProof
\end{gather*}

Commands:
\begin{gather*}
\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
\\[2ex]
\AxRule{c \vdash \Gamma}
\LabelRule{\rulename{wkn}}
\UnaRule{c \vdash\Gamma, x^+: \wn P}
\DisplayProof
\qquad\qquad
\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
\end{gather*}

\section{Reduction rules}\label{reduction-rules}

\begin{align*}
\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^+]
\end{align*}


%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End: