lll.tex

\chapter{Light linear logics}\label{light-linear-logics}

Light linear logics are variants of linear logic characterizing
complexity classes. They are designed by defining alternative
exponential connectives, which induce a complexity bound on the
cut-elimination procedure.

Light linear logics are one of the approaches used in \emph{implicit
computational complexity}, the area studying the computational
complexity of programs without referring to external measuring
conditions or particular machine models.

\section{Elementary linear logic}\label{elementary-linear-logic}

We present here the intuitionistic version of \emph{elementary linear
logic}, ELL. Moreover we restrict to the fragment without additive
connectives.

The language of formulas is the same one as that of (multiplicative)
\hyperref[intuitionistic-linear-logic]{ILL}:
\begin{equation*}
A ::= X \mid A\tens A \mid A\limp A  \mid \oc{A} \mid \forall X A
\end{equation*}
The sequent calculus rules are the same ones as for
\hyperref[intuitionistic-linear-logic]{ILL}, except for the rules dealing
with the exponential connectives:
\begin{equation*}
\AxRule{\Gamma\vdash A}
\LabelRule{\oc\rulename{mf}}
\UnaRule{\oc{\Gamma}\vdash\oc{A}}
\DisplayProof
\qquad
\AxRule{\Gamma,\oc{A},\oc{A}\vdash C}
\LabelRule{\oc c L}
\UnaRule{\Gamma,\oc{A}\vdash C}
\DisplayProof
\qquad
\AxRule{\Gamma\vdash C}
\LabelRule{\oc w L}
\UnaRule{\Gamma,\oc{A}\vdash C}
\DisplayProof
\end{equation*}

The \emph{depth} of a derivation \(\pi\) is the maximum number of
\((\oc\rulename{mf})\) rules in a branch of \(\pi\).

We consider the function \(K(.,.)\) defined by:
\begin{equation*}
\begin{cases}
K(0,n) &=n,\\
K(k+1,n) &=2^{K(k,n)}.
\end{cases}
\end{equation*}

\begin{theorem}
If $\pi$ 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 $ K(d+1,|\pi|)$ steps, where $|\pi|$ is the size of $\pi$.
\end{theorem}

A function $f$ on integers is \emph{elementary recursive} if there exists
an integer $h$ and a Turing machine which computes $f$ in time bounded by
\(K(h,n)\), where $n$ is the size of the input.

\begin{theorem}
The functions representable in  ELL are exactly the elementary recursive functions.
\end{theorem}

One also often considers the \emph{affine} variant of ELL, called
\emph{elementary affine logic} EAL, which is defined by adding
unrestricted weakening:
\begin{prooftree}
\AxRule{\Gamma\vdash C}
\LabelRule{w L}
\UnaRule{\Gamma,A\vdash C}
\end{prooftree}
It enjoys the same properties as ELL.

Elementary linear logic was introduced together with light linear logic~\cite{lightlinearlogic}.

\section{Light linear logic}\label{light-linear-logic}

We present the intuitionistic version of \emph{light linear logic} LLL,
without additive connectives. The language of formulas is:
\begin{equation*}
A ::= X \mid A\tens A \mid A\limp A  \mid \oc{A} \mid \pg{A} \mid \forall X A
\end{equation*}
The sequent calculus rules are the same ones as for ILL, except for the
rules dealing with the exponential connectives:
\begin{equation*}
\AxRule{\Gamma\vdash A}
\LabelRule{\oc\rulename{f} }
\UnaRule{\oc{\Gamma}\vdash\oc{A}}
\DisplayProof
\qquad
\AxRule{\Gamma, \Delta\vdash A}
\LabelRule{\pg }
\UnaRule{\oc{\Gamma}, \pg \Delta\vdash\pg{A}}
\DisplayProof
\qquad
\AxRule{\Gamma,\oc{A},\oc{A}\vdash C}
\LabelRule{\oc c L}
\UnaRule{\Gamma,\oc{A}\vdash C}
\DisplayProof
\qquad
\AxRule{\Gamma\vdash C}
\LabelRule{\oc w L}
\UnaRule{\Gamma,\oc{A}\vdash C}
\DisplayProof
\end{equation*}
In the \((\oc\rulename{f})\) rule, \(\Gamma\) must contain \emph{at most one} formula.

The \emph{depth} of a derivation \(\pi\) is the maximum number of
\((\oc\rulename{f})\) and \((\pg)\) rules in a branch of \(\pi\).

\begin{theorem}
If $\pi$ 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  $ O((d+1)|\pi|^{2^{d+1}})$ steps, where $|\pi|$ is the size of $\pi$.
\end{theorem}

The class FP is the class of functions on binary lists which are
computable in polynomial time on a Turing machine.

\begin{theorem}
The class of functions on binary lists representable in LLL is exactly FP.
\end{theorem}

In the literature one also often considers the \emph{affine} variant of
LLL, called \emph{light affine logic}, LAL.

\section{Soft linear logic}\label{soft-linear-logic}

We consider the intuitionistic version of \emph{soft linear logic}, SLL.
The language of formulas is the same one as that of ILL:
\begin{equation*}
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
\end{equation*}
The sequent calculus rules are the same ones as for ILL, except for the
rules dealing with the exponential connectives:
\begin{equation*}
\AxRule{\Gamma\vdash A}
\LabelRule{\oc\rulename{mf}}
\UnaRule{\oc{\Gamma}\vdash\oc{A}}
\DisplayProof
\qquad
\AxRule{\Gamma,A^{(n)}\vdash C}
\LabelRule{\rulename{mux}}
\UnaRule{\Gamma,\oc{A}\vdash C}
\DisplayProof
\end{equation*}
The rule $\rulename{mux}$ is the \emph{multiplexing} rule. In its premiss,
\(A^{(n)}\) stands for $n$ occurrences of formula \(A\). As particular
instances of multiplexing for \(n=0\) and 1 respectively, we get weakening and
dereliction:
\begin{equation*}
\AxRule{\Gamma \vdash C}
\UnaRule{\Gamma,\oc{A}\vdash C}
\DisplayProof
\qquad
\AxRule{\Gamma,A\vdash C}
\UnaRule{\Gamma,\oc{A}\vdash C}
\DisplayProof
\end{equation*}

The \emph{depth} of a derivation \(\pi\) is the maximum number of
\((\oc\rulename{mf})\) rules in a branch of \(\pi\).

\begin{theorem}
If $\pi$ 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 $O(|\pi|^d)$ steps, where $|\pi|$ is the size of $\pi$.
\end{theorem}

\begin{theorem}
The class of functions on binary lists representable in SLL is exactly FP.
\end{theorem}

Soft linear logic was introduced in~\cite{softlinearlogic}.


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