Laboratoire de l'Informatique et du Parallélisme » Linear Arithmetic

\@writefile{nav}{\headcommand {\beamer@partpages {1}{7}}}

\@writefile{nav}{\headcommand {\beamer@subsectionpages {1}{7}}}

\@writefile{nav}{\headcommand {\beamer@sectionpages {1}{7}}}

\@writefile{nav}{\headcommand {\beamer@documentpages {7}}}

\@writefile{nav}{\headcommand {\def \inserttotalframenumber {7}}}

\item in particular, not so satisfactory for non-deterministic classes

 design an { \ICC{unbounded}} {\BA{arithmetic}} for characterizing FPH

\item enlarge the toolbox  {\ICC{ICC logics}} of , by exploring the power of quantification

\item {\ICC{ramification}}   

\item

\end{document}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%----------

  \frametitle{}

\item   \end{itemize}

  \frametitle{Introduction}

\item  \textit{Implicit computational complexity} (ICC) : 

characterizing complexity classes by programming languages / calculi  without  explicit bounds, 

but instead

 by restricting the constructions %of the language.

 \item either theory-oriented or certification-oriented

 \item often conveniently formulated by:

 (i) a general programming language, (ii)  a criterion on programs

 \end{itemize}

 \end{frame}

 %%%%%%%%%%%%%%%%%%%%%%

 \begin{frame}

  \frametitle{Various approaches to ICC}

 \begin{itemize}

 \item ramified recursion (Leivant, Leivant-Marion) / safe recursion (Bellantoni-Cook)

% \item restrictions on second-order logic (taming comprehension rule) (Leivant)

 \item variants of linear logic (light logics) \textbf{this talk}

 %\item \emph{read-only} functional languages (Jones)

 \item interpretation methods

 \item \dots

  \end{itemize}

  \end{frame}

%%%%%%%%%%%%%%%%%%%%%%

 \begin{frame}

  \frametitle{ICC vs. complexity analysis}

specificities of ICC w.r.t. automatic complexity analysis:

 \begin{itemize}

 \item complexity certificate (e.g. type)

 \item modular

  \end{itemize}

but

\begin{itemize}

\item only rough complexity bounds

\item less general analysis (specific programming discipline)

  \end{frame}

\end{document}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%----------

\begin{frame}\frametitle{The proofs-as-programs viewpoint}

\begin{itemize}

\item our reference language here is $\la$-calculus

 untyped $\la$-calculus is Turing-complete

\item type systems can guarantee termination

ex: system F (polymorphic types)

%\end{itemize}

%

%\end{frame}

%

%----------

%\begin{frame} \frametitle{}

%\begin{itemize}

\item proofs-as-programs correspondence

%Curry-Howard correspondence

\begin{tabular}{ccc}

proof & = & type derivation \\

normalization & = & execution \\

intuitionistic logic & $\leftrightarrow$ & system F

\end{tabular}

\item some characteristics of $\la$-calculus:

    higher-order types

    no distinction between data / program

\end{itemize}

\end{frame}

%----------

\begin{frame} \frametitle{Linear logic}

\begin{itemize}

\item linear logic (LL):

 fine-grained decomposition of intuitionistic logic

 duplication is controlled with a specific connective $\bs$ (\textit{exponential})

\item variants of linear logic with different rules for 

$\bs$ have bounded complexity: \textit{light logics}

 these logics (or subsystems) can be used as type systems for $\la$-calculus

thus:

(i) general language= $\lambda$-calculus, (ii) criterion= typability

\end{itemize}

\end{frame}

%----------

\begin{frame} \frametitle{Outline of the talk}

%\begin{itemize}

%\item Background on $\la$-calculus and system F

%\item The type system DLAL

%\item Relating the Bellantoni-Cook algebra and light linear logic

%\item Conclusion

%\end{itemize}

\begin{enumerate}

\item a recap on $\lambda$-calculus and system F

\item elementary linear logic (ELL): elementary complexity

\item light linear logic (LLL): Ptime complexity

\item other linear logic variants

\item conclusion

\end{enumerate}

\end{frame}

%-----------

\section{A recap on $\lambda$-calculus and system F}

%----------

\begin{frame} \frametitle{$\lambda$-calculus}

\begin{itemize}

\item $\lambda$-terms:

$$t, u::= x \;|\; \la x. t  \; |\; t\; u$$

%$$t, u::= x \;|\; \la x. t  \; |\; (t\; u)$$

\begin{tabular}{cl}

notations: &$\la x_1 x_2. t$ \quad for $\la x_1. \la x_2.t$\\

          & $(t\; u \; v)$ \quad for $((t\; u)\;v)$\\

          &  substitution: $t[u/ x]$

\end{tabular}

\item

$\beta$-reduction:

 $\xrightarrow{1}$ relation obtained by context-closure of:

$$ ((\la x. t) u) \xrightarrow{1} t[u/ x]$$

$\rightarrow$ reflexive and transitive closure of $\xrightarrow{1}$.

\end{itemize}

\end{frame}

%----------

\begin{frame} \frametitle{Typed $\lambda$-terms}

system F types:

$$T, U::= \alpha \; | \; T \rightarrow U \;|\; \forall \al . T$$

simple types: without $\forall$

\medskip

simply typed terms, in Church-style:

$$

x^T

\quad\quad

(\la x^T. M^U)^{T\rightarrow U}

\quad\quad

((M^{T\rightarrow U}) N^T)^U

$$

%$$

%(M^U)^{\forall \alpha.U}

%\quad\quad

%((M^{\forall\alpha. U})T)^{U[T/\alpha]}

%$$

%with: in $\La \alpha. M^U$, 

%$\alpha$ not free in  types of

%free term variables of $M$ %(the {\em eigenvariable condition}).

\end{frame}

%----------

%----------

\begin{frame} \frametitle{Proofs-programs correspondence (Curry-Howard)}

\begin{tabular}{ccc}

 \textbf{typed term} &$\Rightarrow$& \textbf{2nd-order intuitionistic}\\

 &&\quad \textbf{ logic proof}\\

&&\\

type && formula\\

&&\\

$M^B$, with  & &proof of $A_1, \dots, A_n \vdash B$\\

free variables $x_i:A_i$, $1\leq i \leq n$&&\\

&&\\

$\beta$-reduction of term && normalization of proof\\

&& (cut elimination) 

\end{tabular}

\end{frame}

%----------

\begin{frame} \frametitle{Some types and data types}

$$\begin{array}{lcl}

\mbox{Polymorphic identity:}&&\\

 %{\blue \La \al. \la x^{\al}. x }&:& \forall \al. (\al \fl \al)\\

 {\blue  \la x^{\al}. x }&:& \forall \al. (\al \fl \al)\\

 &&\\

\mbox{Church unary integers:}&&\\

 N^F & =& \forall \al.  (\al \fl \al) \fl (\al \fl \al) \\

\mbox{example}&&\\

 % {\blue \underline{2}}&{\blue =}& {\blue \La \al. \la f^{\al\fl \al}.\la x^{\al}. (f\; (f \; x))^{\al}: N }\\

%{\blue  \underline{2} }&{\blue =}& {\blue \la f^{\al\fl \al}.\la x^{\al}. (f)\; (f) \; x: N }\\

 \underline{2} &{\blue =}& {\blue \la f^{\al\fl \al}.\la x^{\al}. (f\; (f \; x)): N^F }\\

\mbox{Church binary words:} &&\\

W^F & =&  \forall \al.  (\al \fl \al) \fl (\al \fl \al) \fl (\al \fl \al)\\

 \mbox{example}&&\\

 % {\blue \underline{<1,1,0>}}&{\blue =}& {\blue \La \al. \la o^{\al\fl \al}.\la z^{\al\fl \al}.\la x^{\al}. (o\; (o \; (z\; x)))^{\al}: W }\\

% {\blue \underline{<1,1,0>} }&{\blue =}& {\blue \la o^{\al\fl \al}.\la z^{\al\fl \al}.\la x^{\al}. (o)\; (o) \; (z)\; x : W }\\

 \underline{<1,1,0>}  &{\blue =}& {\blue \la s_0^{\al\fl \al}.\la s_1^{\al\fl \al}.\la x^{\al}. (s_1\; (s_1  \; (s_0\; x))) : W^F }\\

%\end{eqnarray*}

\end{array}

$$

\end{frame}

%----------

\begin{frame} \frametitle{Iteration }

For each inductive data type an associated iteration principle.

For instance,  for $N= \forall \al.  (\al \fl \al) \fl (\al \fl \al)$, 

we can define  an iterator $\ite$:

$$ \ite= \la f x n. \; (n \; f \; x) \; : (A \fl A) \fl A \fl N \fl  A, \quad \mbox{for any $A$}$$

then

 $(\ite  \; t \; u \; \un{n}) \rightarrow (t\; (t \dots (t\; u)\dots)$  \quad ($n$ times)

\bigskip

\textbf{example:}

$double: N \fl N$

$exp= \la n.  (\ite \; double \; \un{1} \; n)\; : N \fl  N$

$tower= \la n.  (\ite \; exp \; \un{1} \; n)\; : N \fl  N$

\end{frame}

%----------

\begin{frame} \frametitle{Examples of terms}

$$\begin{array}{lll}

\mbox{concatenation}&&\\

%conc &=& \la u^{W}. \la v^{W} .\La \al. \la o. \la z. \la x . (u \; o \; z \;(v \; o\; z \; x))\\

conc &=& \la u^{W}. \la v^{W} . \la s_0. \la s_1. \la x . (u \; s_0 \; s_1) \;(v \; s_0\; s_1 \; x)\\

   &:~ &W\fl W \fl W\\

&&\\

\mbox{length}&&\\

%length&=& \la u^{W}. \La \al. \la f^{\al\fl \al }.( u\; f \; f)^{\al\fl \al}\\

length&=& \la u^{W}.  \la f^{\al\fl \al }.(u\; f \; f)^{\al\fl \al}\\ 

 &:~ &W \fl N\\

% \end{array}$$

% 

% $$\begin{array}{lll}

\mbox{\textit{repeated concatenation}}&&\\

%mult&=& \la n. \la m. (m \; \la k.\la f.\la x. (n \; f\; (k\; f\; x))) \; \underline{0}&:& ~N \fli N \fm \pa N\\

%mult&=& \la n^{N}. \la v^{W}. (n \; (conc \; v)^{W\fl W} ) \; \underline{nil}^W\\

rep&=& \la n^{N}. \la v^{W}. [n \; (conc \; v)  \; \underline{nil}]^W\\

&:& ~N \fl W \fl W\\

%&&&&\\

%square&& &:&N \fm \pa^{4}N

\end{array}

$$

\end{frame}

%----------

\begin{frame} \frametitle{System F and termination}

\bigskip

\begin{theo}[Girard] %[Girard 1972]

 If a term is well typed in $F$, then it is strongly normalizable.

\end{theo}

\bigskip

Thus a type derivation can be seen as a termination witness.

In particular, a term $t: W \fl W$ represents a function on words which terminates 

on all inputs.

\bigskip

%\textbf {Problem:}

 Can we refine this system in order to guarantee \textit{feasible} termination, that is to 

say in polynomial time?

\end{frame}

%---------------

%-----------

%%\begin{frame} \frametitle{Exponential blow up}

%\begin{frame} \frametitle{How can exponential blow up occur?}

%

%\vspace{-5mm}

%

%(thanks to K.~Terui)

%

%2 easy ways to cause exponential blow-up:

%\begin{itemize}

%\item 

% basic functions: $0: \NN$, \quad $s: \NN \rightarrow \NN$, \quad $+:\NN \rightarrow \NN \rightarrow \NN$.

%\item exponential blow-up can be caused by:

%\begin{enumerate}

% \item iteration-iteration

%$$\begin{array}{cccccc}

%\mbox{dbl}(0) &=&0 \qquad \qquad &                \mbox{exp}(0)&=&1  \\

%\mbox{dbl}(s(x))&=&\mbox{dbl}(x)+2 \qquad & \mbox{exp}(s(x))&=&\mbox{dbl}(\mbox{exp}(x))  

%\end{array}

%$$

%\item contraction-iteration

%$$\begin{array}{cccccc}

%\mbox{dbl}(x) &=&x+x \qquad \qquad &                \mbox{exp}(0)&=&1  \\

% &&& \mbox{exp}(s(x))&=&\mbox{dbl}(\mbox{exp}(x))  

%\end{array}

%$$

%\end{enumerate}

%\vspace{-4mm}

%\item to keep contraction and iteration, we need to forbid bad combinations of these.

%\end{itemize}

%

%\end{frame} 

%-----------

\begin{frame} \frametitle{Linear logic}

\item  Linear logic (LL) arises from the decomposition 

 $$A \fli B \equiv  \bs A \fm B$$

\item the $\bs$ modality accounts for duplication (contraction)

\item $!$ satisfies the following principles:

$$

\begin{array}{ccc}

 \bs A \fm \bs A \otimes \bs A \qquad & \infer{ \bs A\vdash  \bs B}{A \vdash B} \qquad           & \bs A \fm A \\

                               & \bs A \otimes \bs B \fm \bs (A \otimes B) & \bs A \fm \bs \bs A

\end{array}

$$

\end{frame} 

\section{Elementary linear logic}

%-----------

\begin{frame} \frametitle{Elementary linear logic (ELL) \qquad [Girard95]}  

\begin{itemize}

\item Language of formulas:

$$ A, B := \alpha \;|\; A \multimap B \;|\; !A \;|\; \forall \alpha. A $$

Denote $!^k A$ for $k$ occurrences of $!$.

\item  The system is designed in such a way that the following principles are \textbf{not} provable

 $$ !A \multimap A, \quad  !A \multimap !!A$$

 \item Defined to characterize \textit{elementary time complexity}, that is to say in time bounded by $2_k^{n}$, for arbitrary $k$.

\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame} \frametitle{Elementary linear logic rules}

%{\tiny

\vspace{-5mm}

\begin{center}

\begin{tabular}{ll}

  {\infer[\mbox{(Id)}]{ x:A \vdash x:A}{}} & \\[1ex]

 &\\

 {\infer[\mbox{($\fm$ i)}]{\Gamma  \vdash \la x. t: A \fm B }

 {\Gamma, x:A \vdash t:B}}

  &

 {\infer[\mbox{($\fm$ e)}]{\Gamma_1,\Gamma_2 \vdash (t\; u) :B }

  {\Gamma_1 \vdash t:A \fm B & \Gamma_2 \vdash u:A}}

\\[1ex]

&\\

{\infer[\mbox{(Cntr)}]{x:!A, \Gamma \vdash t[x \slash x_1, x \slash x_2] :B }{x_1:!A,x_2:!A, \Gamma \vdash t:B }}

&

{\infer[\mbox{(Weak)}]{\Gamma, x:B\vdash t: A }

 {\Gamma \vdash t:A}}

\\[1ex]

&\\

{\infer[\mbox{($!$ i)}]{x_1:! B_1, \dots, x_n:! B_n  \vdash t: ! A }

 {   x_1:B_1, \dots, x_n:B_n \vdash t:A}}

  &

{\infer[\mbox{($!$ e)}]{\Gamma_1,\Gamma_2  \vdash t[u \slash x] :B }

  {\Gamma_1  \vdash u: ! A  & \Gamma_2, x:! A \vdash t:B}}

\\[1ex]

%{\infer[\mbox{($\forall$ i) (*)}]{{ \Gamma  \vdash  t:\forall \alpha. A}}{{ \Gamma  \vdash t:A}}}

% &

% {\infer[\mbox{($\forall$ e)}]{\Gamma  \vdash t:A[B \slash \al] }

%{\Gamma \vdash t:\forall \al. A}} 

 \end{tabular}

%}

\end{center}

\end{frame}

%----------

\begin{frame} \frametitle{Forgetful map from ELL to  F}

Consider $\eras{(.)}: ELL  \rightarrow F$ defined by:

$$\eras{(\bs A)}= \eras{A},\ \ \ 

\eras{(A\fm B)}=\eras{A} \rightarrow \eras{B}, \quad \eras{(\forall \al. A)}= \forall \al. \eras{A}, \quad \eras{\al}=\al.$$

\begin{prop}

 If $\Gamma \vdash_{ELL} t:A$ then $t$ is typable in F with type $\eras{A}$. 

 \end{prop}

\medskip

If $\eras{A}=T$, say  $A$ is a {\emph decoration} of  $T$  in ELL.

\end{frame} 

%----------

\begin{frame} \frametitle{Data types in ELL}

\begin{itemize}

\item

 Church unary integers

\end{itemize}

%\begin{center}

%{\tiny

%\hspace{-4mm}

\begin{tabular}{ccc}

 system F: &  & ELL: \\

$N^F$ &\qquad  & $N^{ELL}$ \\

$\forall \al.  (\al \rightarrow \al) \rightarrow (\al \rightarrow \al)$

& & $\forall \al.  \bs (\al \fm \al) \fm \bs (\al \fm \al)$

\end{tabular}

%\begin{tabular}{ccc}

% system F: &  & ELL: \\

%$N^F$ &\qquad \qquad \qquad \qquad & $N^{ELL}$ \\

%$\forall \al.  (\al \rightarrow \al) \rightarrow (\al \rightarrow \al)$

%& & $\forall \al.  \bs (\al \fm \al) \fm \bs (\al \fm \al)$

%\end{tabular}

%}

%\end{center}

\smallskip

{\tiny Example: integer $2$, in F:

$$ \un{2}=\lambda f^{\blue (\al \rightarrow \al)}. \lambda x^{\blue \al}. (f\;(f\; x))~.$$

}

\begin{itemize}

\item

 Church binary words

\end{itemize}

%{\tiny

\begin{tabular}{cc}

 system F: & ELL: \\

$W^F$ & $W^{ELL}$\\

{\tiny $\forall \al.  (\al \rightarrow \al) \rightarrow (\al \rightarrow \al) \rightarrow (\al \rightarrow \al)$}

& 

{\tiny $\forall \al.  \bs (\al \fm \al) \fm \bs (\al \fm \al) \fm \bs(\al \fm \al)$}

\end{tabular}

%}

\smallskip

{\tiny

Example: $w=\langle 1, 0, 0 \rangle$, in  F:

$$ \un{w}=\lambda s_0^{\blue (\al \rightarrow \al)}. \lambda s_1^{\blue (\al \rightarrow \al)}.

\lambda x^{\blue \al}. (s_1\;(s_0\; (s_0\; x)))~.$$

}

\end{frame} 

%----------

\begin{frame} \frametitle{Representation of functions}

\begin{itemize}

\item  a term $t$ of type $!^k N \fm !^l N$, for some $k$, $l$,  represents a function over unary integers

\item some examples of terms

$$\begin{array}{lll}

\mbox{addition}&&\\

add &=& \la n m f x. (n\; f) \; (m \; f \; x) \; \\

   &:~ &N\fm N \fm N\\

&&\\

\mbox{multiplication}&&\\

%mult &=& \la n m f . (n\; (m\; f))  \\

mult &=& \la n m f . (n\; (m\; f))  \\

   &:~ &N\fm N \fm N\\

\mbox{squaring}&&\\

square &=& \la n f . (n\; (n\; f))  \\

   &:~ &\bs N \fm \bs N\\

$$ 

\end{itemize}

%$$\begin{array}{cclcc}

% N & =& \forall \al.  (\al \fm \al) \fli \pa (\al \fm \al)&&\\

%&&&&\\

%add &=& \la n. \la m .\la f .\la x . (n \; f \;(m \; f \; x))&:~ &N\fm N \fm N\\

%&&&&\\

%mult&=& \la n. \la m. (m \; \la k.\la f.\la x. (n \; f\; (k\; f\; x))) \; \underline{0}&:& ~N \fli N \fm \pa N\\

%mult&=& \la n. \la m. (m \; (add \; n) ) \; \underline{0}&:& ~N \fli N \fm \pa N\\

%&&&&\\

%square&& &:&N \fm \pa^{4}N

%\end{array}

%$$

\end{frame} 

%----------

\begin{frame} \frametitle{Iteration in ELL}

 recall the iterator $\ite$:

$$ \ite= \la f {\red x} {\blue n}. \; (n \; f \; x) \; : \bs (A \fm A) \fm  {\red \bs A} \fm {\blue N} \fm \bs A$$

with $(\ite  \; t \; u \; \un{n}) \rightarrow (t\; (t \; \dots (t\; u)\dots))$  \quad ($n$ times)

\smallskip

\textbf{examples:}

$double: N \fm N$

$exp=  (\ite \; double \; \un{1}) : N \fm \bs N$

remark: $exp$ cannot be iterated; $tower= (\ite \exp \; \un{1})$ non ELL typable.

%$(add \underline{2}): N \fm N$

%

%$double'= \la n. (\ite  \; (add \underline{2}) \; \un{0}) \; n\; : N \fm \pa N$

%

%but $double'$ cannot be iterated.

%

%\medskip

\end{frame} 

%----------

\begin{frame} \frametitle{From derivations to proof-nets }

\begin{figure} %[ht]

%\begin{center}

\includegraphics[angle=90,width=9cm]{SCANS/ELLtranslation.jpg}

%\end{center}

\end{figure}

\end{frame} 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame} \frametitle{Elementary linear logic rules, again}

%{\tiny

\vspace{-5mm}

\begin{center}

\begin{tabular}{ll}

  {\infer[\mbox{(Id)}]{ x:A \vdash x:A}{}} & \\[1ex]

 &\\

 {\infer[\mbox{($\fm$ i)}]{\Gamma  \vdash \la x. t: A \fm B }

 {\Gamma, x:A \vdash t:B}}

  &

 {\infer[\mbox{($\fm$ e)}]{\Gamma_1,\Gamma_2 \vdash (t\; u) :B }

  {\Gamma_1 \vdash t:A \fm B & \Gamma_2 \vdash u:A}}

\\[1ex]

&\\

{\infer[\mbox{(Cntr)}]{x:!A, \Gamma \vdash t[x \slash x_1, x \slash x_2] :B }{x_1:!A,x_2:!A, \Gamma \vdash t:B }}

&

{\infer[\mbox{(Weak)}]{\Gamma, x:B\vdash t: A }

 {\Gamma \vdash t:A}}

\\[1ex]

&\\

{\infer[\mbox{($!$ i)}]{x_1:! B_1, \dots, x_n:! B_n  \vdash t: ! A }

 {   x_1:B_1, \dots, x_n:B_n \vdash t:A}}

  &

{\infer[\mbox{($!$ e)}]{\Gamma_1,\Gamma_2  \vdash t[u \slash x] :B }

  {\Gamma_1  \vdash u: ! A  & \Gamma_2, x:! A \vdash t:B}}

\\[1ex]

%{\infer[\mbox{($\forall$ i) (*)}]{{ \Gamma  \vdash  t:\forall \alpha. A}}{{ \Gamma  \vdash t:A}}}

% &

% {\infer[\mbox{($\forall$ e)}]{\Gamma  \vdash t:A[B \slash \al] }

%{\Gamma \vdash t:\forall \al. A}} 

 \end{tabular}

%}

\end{center}

\end{frame}

%----------

\begin{frame} \frametitle{ELL Proof-Nets }

\vspace{-8mm}

\begin{figure} %[ht]

%\begin{center}

\includegraphics[angle=90,width=10.8cm]{SCANS/ELLproofnets6.jpg}

%\end{center}

%\caption{Lambda terms and Light proof-nets.}\label{schema1}

\end{figure}

\textit{depth} of an edge: number of boxes it is contained in.

%\vspace{-1mm}

\textit{depth} of proof-net: maximal depth of its edges.

\end{frame} 

%%%%%%%%%

\begin{frame} \frametitle{ELL proof-net : example  }

%\vspace{-5mm}

Church integer $\un{3}$:

\vspace{-4mm}

\begin{figure} %[ht]

%\begin{center}

\includegraphics[angle=90,width=5cm]{SCANS/examplePNthree.jpg}

%\end{center}

\end{figure}

\end{frame} 

%%%%%%%%%

\begin{frame} \frametitle{ELL proof-net reduction  }

\vspace{-6mm}

\begin{figure} %[ht]

%\begin{center}

\includegraphics[angle=90,width=10cm]{SCANS/ELLreduction.jpg}

%\end{center}

\end{figure}

\end{frame} 

%----------

\begin{frame} \frametitle{Methodology}

\begin{itemize}

\item write programs with ELL typed $\lambda$-terms

\item evaluate them by: 

compiling them into proof-nets, and then performing proof-net reduction

\item beware:

 \begin{itemize}

 \item proof-net reduction does not exactly match $\beta$-reduction

 \item ELL does not satisfy subject reduction

 but that's all right for our present goal \dots

 More about that in tomorrow's talk, without proof-nets.

\end{itemize}

\end{frame}

%%%%%%%%%

\begin{frame} \frametitle{ELL proof-net reduction  properties}

\begin{itemize}

 \item We have

  \begin{prop}[Stratification]

 The depth of an edge does not change during reduction.

\end{prop}

Consequence: the depth $d$ of a proof-net does not increase during reduction.

\item \textbf{Level-by-level reduction strategy}:

$R$ proof-net of depth $d$

perform reduction successively at depth 0, 1 \dots,  $d$.

\end{itemize}

\end{frame}

%%%%%%%%%

\begin{frame} \frametitle{Level-by-level reduction of ELL proof-nets}

\begin{itemize}

\item let $R$ be an ELL proof-net of depth $d$

$|R|_i$ = size at depth $i$

$|R|$ = total size

round $i$: reduction at depth $i$

there are $d+1$ rounds for the reduction of $R$

\item \textbf{what happens during round $i$?}

\begin{itemize}

 \item $|R|_i$  decreases at each step

  thus there are at most  $|R|_i$ steps  \quad {\blue (size bounds time)}

 \item but  $|R|_{i+1}$ can increase at each step, in fact it can double 

 \item hence  round $i$ can cause an exponential size increase

\item on the whole we have a $2_d^{|R|}$ size increase

\item this yields a  $O(2_d^{|R|})$ bound on the number of steps

\end{itemize}

\end{frame}

%%%%%%%%%

\begin{frame} \frametitle{ELL complexity results}

%\begin{itemize}

 %\item We get

  \begin{theorem}[Proof-net complexity]

  If $R$ is an ELL proof-net of depth $d$, then it can be reduced to its normal form in 

  $O(2_d^{|R|})$ steps.

\end{theorem}

\medskip

  \begin{theorem}[Representable functions]

  The functions representable by a term of type $N \fm !^k N$, where $k\geq 0$ , are exactly the elementary time functions.

\end{theorem}

%\end{itemize}

\end{frame}

%%%%%%%%%

\begin{frame} \frametitle{Proof of the representability theorem}

\begin{itemize}

 \item $\subseteq$ (soundness):

 if $t: N \fm !^k N$ for some $k$, then $t$ represents an elementary function $f$.

 \smallskip

 \textbf{proof}: compute $(t \underline{n})$ by proof-net reduction.

 \item $\supseteq$ (completeness):

  if $f: \mathbb{N} \rightarrow \mathbb{N}$ is an elementary function, then there exists $k$ and $t: N \fm !^k N$ such that $t$ represents $f$.

 \smallskip

   \textbf{proof}: simulation of $O(2_i^n)$-time bounded Turing machine, for any $i$.

\end{frame}

%%%%%%%%%

\section{Light linear logic}

\begin{frame} \frametitle{Taming the exponential blow-up?}

%\begin{frame} \frametitle{Motivation: exponential blow-up}

\vspace{-4mm}

\begin{figure} %[ht]

%\begin{center}

\includegraphics[width=2.7cm]{SCANS/example_exponent.jpg}

%\end{center}

\end{figure}

\end{frame} 

%-----------

\begin{frame} \frametitle{Light linear logic (LLL)  \qquad [Girard95]}

\begin{itemize}

\item Language of formulas:

$$ A, B := \alpha \;|\; A \multimap B  \;|\; \forall \alpha. A  \;|\;  !A \;|\; {\red \pa A}$$

intuition: $\pa$ a new modality for non-duplicable boxes

\item  The   following principles are still \textbf{not} provable

 $$ !A \multimap A, \quad  !A \multimap !!A$$

\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame} \frametitle{Light linear logic rules}

\begin{itemize}

\item rules (Id), ($\fm$ i), ($\fm$ e), (Cntr), (Weak): as in ELL.

 \item new rules ($!$ i), ($!$ e), ($\pa$ i), ($\pa$ e):

\bigskip

\begin{center}

\begin{tabular}{ll}

%  {\infer[\mbox{(Id)}]{ x:A \vdash x:A}{}} & \\[1ex]

% &\\

% {\infer[\mbox{($\fm$ i)}]{\Gamma  \vdash \la x. t: A \fm B }

% {\Gamma, x:A \vdash t:B}}

%

%  &

% {\infer[\mbox{($\fm$ e)}]{\Gamma_1,\Gamma_2 \vdash (t\; u) :B }

%  {\Gamma_1 \vdash t:A \fm B & \Gamma_2 \vdash u:A}}

%\\[1ex]

%&\\

%{\infer[\mbox{(Cntr)}]{x:A, \Gamma \vdash t[x \slash x_1, x \slash x_2] :B }{x_1:!A,x_2:!A, \Gamma \vdash t:B }}

%&

%{\infer[\mbox{(Weak)}]{\Gamma, x:B\vdash t: A }

% {\Gamma \vdash t:A}}

% 

%\\[1ex]

%&\\

{\infer[\mbox{($!$ i)}]{x:! B  \vdash t: ! A }

 {   x :B \vdash t:A}}

  &

{\infer[\mbox{($!$ e)}]{\Gamma_1,\Gamma_2  \vdash t[u \slash x] :B }

  {\Gamma_1  \vdash u: ! A  & \Gamma_2, x:! A \vdash t:B}}

\\[1ex]

&\\

{\infer[\mbox{($\pa$ i)}]{! \Gamma, \pa \Delta  \vdash t: \pa  A }

 {   \Gamma, \Delta  \vdash t:A}}

  &

{\infer[\mbox{($!$ e)}]{\Gamma_1,\Gamma_2  \vdash t[u \slash x] :B }

  {\Gamma_1  \vdash u: \pa A  & \Gamma_2, x: \pa  A \vdash t:B}}

%{\infer[\mbox{($\pa$ i)}]{x_1:! B_1, \dots, x_i: \pa B_i , \dots,  x_n:\pa  B_n  \vdash t: \pa  A }

% {   x_1:B_1, \dots, x_i: B_i, \dots , x_n:B_n \vdash t:A}}

%  &

%{\infer[\mbox{($!$ e)}]{\Gamma_1,\Gamma_2  \vdash t[u \slash x] :B }

%  {\Gamma_1  \vdash u: \pa A  & \Gamma_2, x: \pa  A \vdash t:B}}

%\\[1ex]

%{\infer[\mbox{($\forall$ i) (*)}]{{ \Gamma  \vdash  t:\forall \alpha. A}}{{ \Gamma  \vdash t:A}}}

% &

% {\infer[\mbox{($\forall$ e)}]{\Gamma  \vdash t:A[B \slash \al] }

%{\Gamma \vdash t:\forall \al. A}} 

 \end{tabular}

%}

\end{center}

\bigskip

 where if $\Gamma= x_1:B_1, \dots, x_k:B_k$, 

$\dagger \Gamma= x_1: \dagger B_1, \dots, x_k: :\dagger B_k$, for $\dagger= !, \pa$.

%----------

\begin{frame} \frametitle{Forgetful map from LLL to  ELL}

Consider $\lte{(.)}: LLL  \rightarrow ELL$ defined by:

$$\lte{(\pa A)}= ! \lte{A},   \quad \lte{(! A)}= ! \lte{A}$$

and other connectives unchanged.

%\eras{(A\fm B)}=\eras{A} \rightarrow \eras{B}, \quad \eras{(\forall \al. A)}= \forall \al. \eras{A}, \quad \eras{\al}=\al.$$

\begin{prop}

 If $\Gamma \vdash_{LLL} t:A$ then  $\lte{\Gamma} \vdash_{ELL} t:\lte{A}$.  

 \end{prop}

\end{frame} 

%----------

\begin{frame} \frametitle{Data types in LLL}

\begin{itemize}

\item

 Church unary integers

\end{itemize}

%\begin{center}

%{\tiny

%\hspace{-4mm}

\begin{tabular}{ccc}

 system F: &  & LLL: \\

$N^F$ &\qquad  & $N^{LLL}$ \\

$\forall \al.  (\al \rightarrow \al) \rightarrow (\al \rightarrow \al)$

& & $\forall \al.  \bs (\al \fm \al) \fm {\red \pa}  (\al \fm \al)$

\end{tabular}

%\begin{tabular}{ccc}

% system F: &  & ELL: \\

%$N^F$ &\qquad \qquad \qquad \qquad & $N^{ELL}$ \\

%$\forall \al.  (\al \rightarrow \al) \rightarrow (\al \rightarrow \al)$

%& & $\forall \al.  \bs (\al \fm \al) \fm \bs (\al \fm \al)$

%\end{tabular}

%}

%\end{center}

\smallskip

{\tiny Example: integer $2$, in F:

$$ \un{2}=\lambda f^{\blue (\al \rightarrow \al)}. \lambda x^{\blue \al}. (f\;(f\; x))~.$$

}

\begin{itemize}

\item

 Church binary words

\end{itemize}

%{\tiny

\begin{tabular}{cc}

 system F: & LLL: \\

$W^F$ & $W^{LLL}$\\

{\tiny $\forall \al.  (\al \rightarrow \al) \rightarrow (\al \rightarrow \al) \rightarrow (\al \rightarrow \al)$}

& 

{\tiny $\forall \al.  \bs (\al \fm \al) \fm \bs (\al \fm \al) \fm {\red \pa} (\al \fm \al)$}

\end{tabular}

%}

\smallskip

{\tiny

Example: $w=\langle 1, 0, 0 \rangle$, in  F:

$$ \un{w}=\lambda s_0^{\blue (\al \rightarrow \al)}. \lambda s_1^{\blue (\al \rightarrow \al)}.

\lambda x^{\blue \al}. (s_1\;(s_0\; (s_0\; x)))~.$$

}

\end{frame} 

%----------

\begin{frame} \frametitle{Representation of functions}

\begin{itemize}

\item  a term $t$ of type $!^k N \fm \pa^l N$, for some $k$, $l$,  represents a function over unary integers

 $!^k W \fm \pa^l W$: function over binary words.

\item some examples of terms

$$\begin{array}{lll}

\mbox{addition}&&\\

add &=& \la n m f x. (n\; f) \; (m \; f \; x) \; \\

   &:~ &N\fm N \fm N\\

&&\\

\mbox{double}&&\\

double &=& \la n  f x. (n\; f) \; (n \; f \; x) \; \\

   &:~ &! N \fm \pa N\\

   \mbox{concatenation}&&\\

%conc &=& \la u^{W}. \la v^{W} .\La \al. \la o. \la z. \la x . (u \; o \; z \;(v \; o\; z \; x))\\

%conc &=& \la u^{W}. \la v^{W} . \la o. \la z. \la x . ((u) \; o \; z) \;(v) \; o\; z \; x\\

%   &:~ &W\fl W \fl W\\

   conc &:~ &W\fm W \fm W\\

  \end{array}

   $$

%\mbox{multiplication}&&\\

%%mult &=& \la n m f . (n\; (m\; f))  \\

%mult' &=& \la n m f . (n\; (m\; f))  \\

%

%   &:~ &N\fm N \fm N\\

%

%\mbox{squaring}&&\\

%square &=& \la n f . (n\; (n\; f))  \\

%

%   &:~ &\bs N \fm \bs N\\

%\end{array}

%$$ 

\end{itemize}

\end{frame} 

%----------

\begin{frame} \frametitle{Iteration in LLL}

 we can type the iterator $\ite$:

$$ \ite= \la f {x} {n}. \; (n \; f \; x) \; : \bs (A \fm A) \fm  {\red \bs A} \fm {N} \fm {\red \pa A}$$

%with $(\ite _A \; F \; t) \; \un{n} \rightarrow (F\; (F \; \dots (F\; t)\dots))$  \quad ($n$ times)

\textbf{examples:}

$(add \underline{3}): N \fm N$ can be iterated

\smallskip

$double: !N \fm \pa N$ cannot be iterated

\smallskip

thus some exponentially growing terms are not typable

%$double'= \la n. (\ite  \; (add \underline{2}) \; \un{0}) \; n\; : N \fm \pa N$

%

%but $double'$ cannot be iterated.

 \end{frame} 

%%%%%%%%%

\begin{frame} \frametitle{LLL proof-nets}

\vspace{-3mm}

\begin{figure} %[ht]

%\begin{center}

\includegraphics[angle=90,width=6.3cm]{SCANS/LLLboxes.jpg}

%\end{center}

\end{figure}

\end{frame} 

%%%%%%%%%

\begin{frame} \frametitle{LLL proof-net reduction}

\vspace{-4mm}

\begin{figure} %[ht]

%\begin{center}

\includegraphics[angle=90,width=6cm]{SCANS/LLLreduction.jpg}

%\end{center}

\end{figure}

\end{frame} 

%%%%%%%%%

\begin{frame} \frametitle{Level-by-level reduction of LLL proof-nets}

\begin{itemize}

\item as in ELL we use a level-by-level strategy

\item let $R$ be an LLL proof-net of depth $d$

round $i$: reduction at depth $i$

there are $d+1$ rounds for the reduction of $R$

\item \textbf{what happens during round $i$?}

\begin{itemize}

 \item $|R|_i$  decreases at each step

  thus there are at most  $|R|_i$ steps  \quad {\blue (size bounds time)}

 \item yet $|R|_{i+1}$ can increase:

 during round $i$ we can have a quadratic increase:

 $$|R'|_{i+1} \leq |R|_{i+1}^2$$

 \end{itemize}

\item this repeats $d$ times, so on the whole we have a $|R|^{2^d}$ size increase

\item this yields a  $O(|R|^{2^d})$ bound on the number of steps

\end{itemize}

\end{frame}

%%%%%%%%%

\begin{frame} \frametitle{LLL complexity results}

%\begin{itemize}

 %\item We get

  \begin{theorem}[Proof-net complexity]

  If $R$ is an LLL proof-net of depth $d$, then it can be reduced to its normal form in 

  $O(|R|^{2^d})$ steps.

\end{theorem}

Thus at fixed depth $d$ we have a polynomial bound.

\medskip

  \begin{theorem}[Representable functions]

  The functions representable by a term of type $W \fm \pa^k W$, for $k\geq 0$, are exactly the functions of FP (polynomial time functions).

\end{theorem}

%\end{itemize}

%%%%%%%%%

\begin{frame} \frametitle{Further comments about LLL}

\begin{itemize}

\item \textbf{LLL and $\lambda$-calculus}: 

 a proper type system for $\lambda$-calculus can be designed out of LLL, which ensures a strong polynomial time bound on $\beta$-reduction (and not only on proof-net reduction)

\item \textbf{about expressivity}:

the completeness result is an extensional one

but the intensional expressivity of LLL is quite limited

\smallskip

indeed:  rich features (higher-order, polymorphism) but "pessimistic" account of iteration \dots

\end{itemize}

\end{frame}

\section{Other linear logic variants}

%%%%%%%%%

\begin{frame} \frametitle{A glimpse of a linear logics zoo}

\begin{itemize}

\item for P

\begin{itemize}

  \item soft linear logic:   {\tiny  [Lafont04]}

     a simple system, but with more constrained programming

     \item bounded linear logic: {\tiny [GSS92]}

     $!_{P(\vec{x})} A$ : more explicit, but more flexible

\end{itemize}

\item for EXPTIME and $k$-EXPTIME

\begin{itemize}

  \item ELL again: see tomorrow's talk

\end{itemize}

\item for PSPACE

   \begin{itemize}

  \item  $STA_B$ {\tiny [GMRdR08]} : extends soft linear logic with a craftly typed conditional

  \end{itemize}

\item for LOGSPACE

 \begin{itemize}

  \item $IntML$ {\tiny[DLS10]}: evaluation by computation by interaction

  \end{itemize}

\end{itemize}

\end{frame}

%\section{Conclusion}

%%%%%%%%%%%%%%%%

\begin{frame}{Conclusions and perspectives}

\begin{itemize}

\item while ramified recursion is based on a stratification of data,

ELL / LLL are based on a stratification of programs

\item they yield type systems for $\lambda$-calculus

\item w.r.t. other ICC approaches:

\begin{itemize}

   \item handle higher-order computation

   \item but limited intensional expressivity

\end{itemize}

relations with other ICC systems are still to explore

%\item still to explore: how they relate to other more expressive ICC approaches (interpretations, NSI types)

\item light logics are languages for higher-order computation, but we only characterize first-order complexity classes \dots

 what about   higher-order complexity?

\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%% GARBAGE %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%-----------

\begin{frame} \frametitle{Light linear logic, LLL (Girard 98)}

%\vspace{-8mm}

$$

\begin{array}{ccc}

 \bs A \fm \bs A \otimes \bs A \qquad & \infer{ \bs A\vdash  \bs B}{A \vdash B} \qquad           & \\

 & \bs A \otimes \bs B \fm \pa (A \otimes B) & 

\end{array}

$$

\begin{tabular}{ll}

new modality $\pa$, with: & $\bs A \fm \pa A$\\

$\pa$ is a functor and &$\pa A \otimes \pa B \fm \pa(A\otimes B)$

\end{tabular}

$\longrightarrow$ manages to avoid both exponentiation schemes

\smallskip

 Light affine logic (LAL) is the variant with full weakening.

\end{frame}

%%%%%%%%%%%

\begin{frame} \frametitle{Light linear logic: properties}

Proofs can be represented as \textit{proof-nets} (graphs). Normalization of proof-nets

corresponds to program execution.

\smallskip

\begin{theo}[Girard] %[Girard 95]

Light linear logic \textit{proof-nets} admit a polynomial time normalization (at fixed \textit{depth}). 

\end{theo}

%\smallskip

\begin{theo}[Completeness. Girard/Asperti-Roversi]

%All polynomial time functions on binary lists

  All polynomial time functions $f: \{0,1\}^{\star} \rightarrow  \{0,1\}^{\star}$

can be represented in Light Linear Logic (resp. Light \textit{Affine} Logic).

\end{theo}

\end{frame} 

%-----------

\begin{frame} \frametitle{ Light linear logic and typing}

%\vspace{-3mm}

Can we use LLL or LAL directly as type systems for lambda calculus~?

\smallskip 

There are two pitfalls:

\begin{itemize}

\item they do not give subject-reduction,

\item no polynomial bound on the number of $\beta$-reduction steps for typed terms (even if there is one on proof-net normalization).

\end{itemize}

\end{frame} 

%-----------

\begin{frame} \frametitle{Type system DLAL}

%\vspace{-3mm}

%

%Can we use LLL or LAL directly as type systems for lambda calculus~?

% There are two pitfalls:

%\begin{itemize}

%\item they do not give subject-reduction,

%\item no polynomial bound on the number of $\beta$-reduction steps for typed terms (even if there is one on proof-net normalization).

%\end{itemize}

%\medskip

%$\rightarrow$ To overcome these problems:

To overcome the problems with typing in LAL:

we can restrict in Light affine logic the use of $\bs$ to $\bs A \fm B$, denoted $A \fli B$

the DLAL (\textit{Dual Light Affine Logic}) type system [Baillot-Terui04]:

$$ A, B ::= \alpha \; |\; A \fm B \; |\; A \fli B \; |\; \pa A \; |\; \forall \alpha. A$$

\vspace{-4mm}

typing judgements of the form: $ {\blue \Gamma} ; {\red \Delta} \vdash t: A$, 

where

\begin{tabular}{l}

$ {\blue \Gamma}$ contains duplicable variables,\\

${\red \Delta}$ contains linear variables.

\end{tabular}

\end{frame} 

%

%%\overlays{8}{

%\begin{frame} \frametitle{DLAL typing rules}

%%\DefaultTransition{Dissolve}

%{\tiny

%%\onlySlide*{1}{

%% \begin{center}

%%\hspace{-12mm}

%%\fbox{

%\begin{tabular}{l@{\hspace{-2mm}}l}

%  {\infer[\mbox{(Id)}]{; x:A \vdash x:A}{}} & \\

%% &\\

% 

%\untilSlide*{2}{

%{\infer[\mbox{($\fm$ i)}]{\Gamma_1; \Delta_1 \vdash \la x. t: A \fm B }

% {\Gamma_1; \Delta_1, x:A \vdash t:B}}

%}

%\onlySlide*{3}{

%{\red \infer[\mbox{($\fm$ i)}]{\Gamma_1; \Delta_1 \vdash \la x. t: A \fm B }

% {\Gamma_1{\blue ;} \Delta_1, x:A \vdash t:B}}

%}

%\fromSlide*{4}{

%{\infer[\mbox{($\fm$ i)}]{\Gamma_1; \Delta_1 \vdash \la x. t: A \fm B }

% {\Gamma_1; \Delta_1, x:A \vdash t:B}}

%}

%  &

% {\infer[\mbox{($\fm$ e)}]{\Gamma_1,\Gamma_2; \Delta_1, \Delta_2 \vdash (t\; u) :B }

%  {\Gamma_1; \Delta_1 \vdash t:A \fm B & \Gamma_2; \Delta_2 \vdash u:A}}

%\\[1ex]

%

%\untilSlide*{2}{

%{\infer[\mbox{($\fli$ i)}]{\Gamma_1; \Delta_1 \vdash \la x. t: A \fli B }

% {\Gamma_1, x:A ; \Delta_1\vdash t:B}}

%}

%\onlySlide*{3}{\red

%{\infer[\mbox{($\fli$ i)}]{\Gamma_1; \Delta_1 \vdash \la x. t: A \fli B }

% {\Gamma_1, x:A {\blue ;} \Delta_1\vdash t:B}}

%}

%\fromSlide*{4}{

%{\infer[\mbox{($\fli$ i)}]{\Gamma_1; \Delta_1 \vdash \la x. t: A \fli B }

% {\Gamma_1, x:A ; \Delta_1\vdash t:B}}

%}

%  & 

%\untilSlide*{3}{

%{\infer[\mbox{($\fli$ e)}]{\Gamma_1, z:C ; \Delta_1 \vdash (t\; u) :B }

%  {\Gamma_1; \Delta_1 \vdash t:A \fli B & ; z:C \vdash u:A}}

%}

%\onlySlide*{4}{\red

%{\infer[\mbox{($\fli$ e)}]{\Gamma_1, z:C  ; \Delta_1 \vdash (t\; u) :B }