
%\documentclass[pdf, pleasingblue,slideColor,colorBG]{prosper}
\documentclass{beamer}
\usepackage{amsfonts,latexsym,amssymb, amsmath}
\usepackage{stmaryrd}
\usepackage{graphicx} 
\usepackage{eepic}
\usepackage[dvips]{epsfig}
%\usepackage{psfig}
%\input head.tex
\usepackage{proof,bussproofs}
%\usepackage{ desseins_s}


%\usepackage{microtype}%if unwanted, comment out or use option "draft"
%\usepackage[dvipsnames]{xcolor}

%\graphicspath{{./graphics/}}%helpful if your graphic files are in another directory

%\bibliographystyle{plainurl}% the recommended bibstyle

%\usepackage[lutzsyntax]{virginialake}
\input{ph-macros}



\setbeamercolor{block title}{bg=blue!10}
\setbeamercolor{block body}{bg=blue!10}
\definecolor{monred}{HTML}{9D0909}
%\definecolor{monbleu}{RVB}{0,0,1}
 \def\red#1{\color{red}{#1}}
 \def\blue#1{\color{blue}{#1}}
 \def\green#1{\color{green}{#1}}
\def\black{}
\def\BA#1{\color{red}{#1}}
 \def\ICC#1{\color{blue}{#1}}


%%%%%%%%%%%%%ENVIRONMENTS AND THEOREM-STYLES %%%%%%%%%%%%%%%%%%
%\def\un#1{\underline{#1}}
%\def\point#1{{\bf #1.}}
%%\newcommand{\etq}[1]{\mbox{\scriptsize\bf #1}}
%\newcommand{\etq}[1]{\mbox{{\bf #1}}}
%\newcommand{\Rulone}[1]{%
%          \begin{center}
%           \makebox[12cm]{\hspace*{\fill}
%                 \begin{minipage}[c]{6cm} #1 \end{minipage} \hspace*{\fill}
%                }
%          \end{center}
%  }
%
%\newcommand{\centra}[1]{\begin{center} #1 \end{center}}
%
%\newcommand{\Rultwo}[2]{%
%          \begin{center}
%           \makebox[12cm]{
%         \makebox[6cm]{\begin{minipage}[c]{6cm} #1 \end{minipage}} \hspace{20pt}
%         \makebox[6cm]{\begin{minipage}[c]{6cm} #2 \end{minipage}}
%                }
%          \end{center}
%  }
%\newcounter{ex}
%%\newtheorem{example}[ex]{Example}
%
%
%\def\para#1{\paragraph{#1}}
%\newtheorem{theo}{Theorem}
%\newtheorem{de}{Definition}
%\newtheorem{prop}[theo]{Proposition}
%\newtheorem{lem}[theo]{Lemma}
%\newtheorem{Cor}[theo]{Corollary}
%\newtheorem{remark}[theo]{Remark}
%\newcounter{pb}
%\newtheorem{problem}[pb]{Problem}
%\newenvironment{proof}{\noindent{\bfseries Proof :}}{\hbox{}\hfill$\Box$}

%---------------------
%% Definition of new colors
%\newrgbcolor{LemonChiffon}{1. 0.98 0.8}
%
%\newrgbcolor{LightBlue}{0.68 0.85 0.9}
%\newrgbcolor{Dgreen}{0  0.6 0.4}
%%\newrgbcolor{DBlue}{0  0 0.5}
%\newrgbcolor{DBlue}{0  0 0.6}
%\newrgbcolor{Dblue}{0  0 0.6}
%%----------------------
%%% MORE Color definitions
%\newrgbcolor{DarkGray}{.284 .210 .410}
%\newrgbcolor{Violet}{.2 .2  .9}

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

\mode<presentation>
{
  \usetheme{Warsaw}
  % or ...

  \setbeamercovered{transparent}
  % or whatever (possibly just delete it)
}


\title{Towards an Unbounded Implicit Arithmetic for\\
the Polynomial Hierarchy
}

\author{Patrick Baillot and Anupam Das}
\institute{CNRS / ENS Lyon}


\begin{document}
\maketitle


\begin{frame}
  \frametitle{Introduction}
 
 2 cousin approaches to logical characterization of complexity classes:
 
\bigskip 

 \begin{tabular}{l|l}
 \BA{Bounded arithmetic (86 -- )} & \ICC{Implicit computational complexity  (91 --)}\\
      & \ICC{(ICC)}\\
 \hline
 &\\
 & function algebras\\
 & types/proofs-as-programs\\
 & arithmetics / logics\\
 & \\
 large variety of & resource-free characterizations of\\
 complexity classes & complexity classes (e.g. ramification)\\
 &\\
 corresp. with & extensions to programming languages\\
 \textit{proof-complexity} &
 \end{tabular}
  \end{frame}

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

\begin{frame}
  \frametitle{Introduction}
 
$$  \mbox{"\textit{$f$ is provably total in system} XXX"} \Leftrightarrow \quad f \in \mbox{ complexity class YYY }$$
 
\bigskip 

 \begin{tabular}{l|l}
 \BA{Bounded arithmetic}  \qquad \qquad & \ICC{Implicit computational complexity}\\
 \hline
 &\\
  Buss ($S_1$): & Leivant (intrinsic theories): \\
  $\forall x, {\BA{\exists y \leq t}} . \; A_f(x,y)$ & $\forall x. N_1(x) \rightarrow N_0(f(x))$\\
  &\\
  FP, FPH & FP
  \end{tabular}
  \end{frame}
  
  %%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
  \frametitle{{A current limitation of ICC logics}}
 
 \begin{itemize}
\item fewer complexity classes characterized by {\ICC{ICC logics}} than by {\BA{bounded arithmetic}}
\item in particular, not so satisfactory for non-deterministic classes

e.g. NP, PH (polynomial hierarchy) \dots

 \end{itemize}
 \end{frame}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
  \frametitle{Recap : the polynomial hierarchy}
 
 \begin{itemize}
\item  to be done: definition \dots
 \end{itemize}
 \end{frame}

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

\begin{frame}
  \frametitle{Our goal}
 
 design an { \ICC{unbounded}} {\BA{arithmetic}} for characterizing FPH
 
 \medskip 
 
 expected benefits:
 \begin{itemize}
\item   bridge  {\BA{bounded arithmetic}}  and {\ICC{ICC logics}}
\item enlarge the toolbox  {\ICC{ICC logics}} of , by exploring the power of quantification
\end{itemize}
 \end{frame}

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

\begin{frame}
  \frametitle{Methodology}
 
 We want to use:
 \begin{itemize}
\item {\ICC{ramification}}   
\item
\end{itemize}
 \end{frame}


\end{document}

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

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

\begin{frame}
  \frametitle{}
 
 \begin{itemize}
\item   \end{itemize}
 \end{frame}

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

\begin{frame}
  \frametitle{Introduction}
 
 \begin{itemize}
\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{itemize}
  \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}

\begin{itemize}
\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{itemize}
\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 $$

\smallskip
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{array}
$$ 
\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
 \end{itemize}
 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
 \end{itemize}
\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{itemize}
\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$.
\end{itemize}

\end{frame}

%----------
\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}
\end{frame}

%%%%%%%%%
\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}

\end{document}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%% 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 }
%  {\Gamma_1; \Delta_1 \vdash t:A \fli B & {\blue ; z:C \vdash u:A }}}
%}
%\onlySlide*{5}{
%{\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*{6}{
%{\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}}
%}
%\fromSlide*{7}{
%{\infer[\mbox{($\fli$ e)}]{\Gamma_1, z:C ; \Delta_1 \vdash (t\; u) :B }
%  {\Gamma_1; \Delta_1 \vdash t:A \fli B & {\blue ; z:C \vdash u:A}}}
%}
%
%\\[1ex]
%{\infer[\mbox{(Weak)}]{\Gamma_1, \Gamma_2; \Delta_1, \Delta_2 \vdash t: A }
% {\Gamma_1; \Delta_1 \vdash t:A}}
%  &
%\onlySlide*{1}{
%{\infer[\mbox{(Cntr)}]{x:A, \Gamma_1; \Delta_1 \vdash t[x \slash x_1, x \slash x_2] :B }{x_1:A,x_2:A, \Gamma_1; \Delta_1 \vdash t:B }}
%} 
%\onlySlide*{2}{\red
%{\infer[\mbox{(Cntr)}]{x:A, \Gamma_1{\blue ;} \Delta_1 \vdash t[x \slash x_1, x \slash x_2] :B }{x_1:A,x_2:A, \Gamma_1{\blue ;} \Delta_1 \vdash t:B }} 
%}
%\fromSlide*{3}{
%{\infer[\mbox{(Cntr)}]{x:A, \Gamma_1; \Delta_1 \vdash t[x \slash x_1, x \slash x_2] :B }{x_1:A,x_2:A, \Gamma_1; \Delta_1 \vdash t:B }} 
%}
%\\[1ex]
%
%\untilSlide*{4}{
%{\infer[\mbox{($\pa$ i)}]{\Gamma ; x_1:\pa B_1, \dots, x_n:\pa B_n  \vdash t: \pa A }
% {  ; \Gamma, x_1:B_1, \dots, x_n:B_n \vdash t:A}}
%}
%\onlySlide*{5}{\red
%{\infer[\mbox{($\pa$ i)}]{\Gamma {\blue ;} x_1:\pa B_1, \dots, x_n:\pa B_n  \vdash t: \pa A }
% { {\blue ;} \Gamma, x_1:B_1, \dots, x_n:B_n \vdash t:A}}
%}
%\onlySlide*{6}{
%{\infer[\mbox{($\pa$ i)}]{\Gamma  ; x_1:\pa B_1, \dots, x_n:\pa B_n  \vdash t: \pa A }
% {  ; \Gamma, x_1:B_1, \dots, x_n:B_n \vdash t:A}}
%}
%\fromSlide*{7}{
%{\infer[\mbox{($\pa$ i)}]{ \Gamma  ; x_1:\pa B_1, \dots, x_n:\pa B_n  \vdash t: \pa A }
% {  {\blue ; \Gamma, x_1:B_1, \dots, x_n:B_n \vdash t:A}}}
%}
%
%  &
%%\hspace{-10mm}
%
% \untilSlide*{5}{
% {\infer[\mbox{\hspace{-1mm}($\pa$ e)}]{\Gamma_1,\Gamma_2; \Delta_1, \Delta_2 \vdash t[u \slash x] :B }
%  {\Gamma_1; \Delta_1 \vdash u: \pa A  & \Gamma_2; x:\pa A, \Delta_2 \vdash t:B}}
%}
%\onlySlide*{6}{\red
% {\infer[\mbox{\hspace{-1mm}($\pa$ e)}]{\Gamma_1,\Gamma_2; \Delta_1, \Delta_2 \vdash t[u \slash x] :B }
%  {\Gamma_1; \Delta_1 \vdash u: \pa A  & \Gamma_2; x:\pa A, \Delta_2 \vdash t:B}}
%}
%\fromSlide*{7}{
% {\infer[\mbox{\hspace{-1mm}($\pa$ e)}]{\Gamma_1,\Gamma_2; \Delta_1, \Delta_2 \vdash t[u \slash x] :B }
%  {\Gamma_1; \Delta_1 \vdash u: \pa A  & \Gamma_2; x:\pa A, \Delta_2 \vdash t:B}}
%}
%
%\\[1ex]
%\fromSlide*{8}{      %% ajouté 26/6
%{\infer[\mbox{($\forall$ i) (*)}]{{ \Gamma_1; \Delta_1 \vdash  t:\forall \alpha. A}}{{ \Gamma_1; \Delta_1 \vdash t:A}}}}
% &
%\fromSlide*{8}{  
% {\infer[\mbox{($\forall$ e)}]{\Gamma_1; \Delta_1 \vdash t:A[B \slash \al] }
%{\Gamma_1; \Delta_1 \vdash t:\forall \al. A}} 
%}
%
% \end{tabular}
%
%%}
%%\end{center}
%%}
%}
%
%
%\medskip
%
%\onlySlide*{2}
%{
%\begin{lem}\label{linearitylemma}
%  If $\Gamma ; \Delta \vdash_{DLAL} t:A$ and  $x \in
%  \Delta$ then $x$ has at most one occurrence in $t$.
%\end{lem}
%}
%
%
%\onlySlide*{3}
%{
% $(\fm i)$ (resp. $(\fli i)$) corresponds to abstraction on a linear (resp. non-linear) variable,
%}
%
%\onlySlide*{4}
%{
%an  argument {\blue $u$} of a term {\red $t$} of type {\red $A\fli B$} must have at most one 
%free variable {\blue $z$}, which is moreover linear.
%
%{\red $\rightarrow$ prevents 2nd exponentiation scheme (contraction-iteration)}.
%}
%
%\onlySlide*{5}
%{
%  the rule ($\pa$ i) allows to turn linear variables (in $\Gamma$) into non-linear ones.
%
%\medskip
%
%{\red $\rightarrow$ prevents 1st exponentiation scheme (iteration-iteration)}.
%}
%
%%\fromSlide*{6}
%%{
%% \begin{prop}
%%If $\cal D$ has conclusion $\Gamma;\Delta \vdash_{DLAL} t: A$
%%then  $|t| \leq |{\cal D}|$.
%%\end{prop}  
%%}
%
%\onlySlide*{7}
%{
% \textit{Depth} $d$ of a derivation $\cal D$: maximal number of ($\pa$ i) and r.h.s.
% premises of ($\fli$ e) in 
%a branch of $\cal D$.
%}
%
%\fromSlide*{8}
%{
% (*) $\alpha \notin \Gamma_1, \Delta_1$.
%}
%
%\end{frame} 
%%}

%----------
\begin{frame} \frametitle{DLAL and system F}

\begin{itemize}
\item Forgetful map $(.)^-$ from DLAL to F:
\begin{itemize}
 \item remove occurrences of $\S$,
 \item replace $\fm$ and $\fli$ with $\rightarrow$.
\end{itemize}

 $(.)^-$ gives a map from DLAL derivations to system F derivations.

\item Data types in DLAL:

\medskip


%\begin{center}
{\tiny
\begin{tabular}{l@{\hspace{0mm}}ll}
& \quad F & \quad DLAL \\
%$N^{EAL}$ & $N^{LAL}$ \\
\hspace{-1.2cm}
 Church integers& $\forall \al.   (\al \rightarrow \al) \rightarrow  (\al \rightarrow \al)$ &
 $\forall \al.  (\al \fm \al) \fli \S (\al \fm \al)$\\
\hspace{-1.2cm}
  binary lists
&$\forall \al.   (\al \rightarrow \al) \rightarrow  (\al \rightarrow \al)
 \rightarrow (\al \rightarrow \al)$
&
$\forall \al. (\al \fm \al) {\red \fli} (\al \fm \al) {\red \fli} \S (\al {\blue \fm} \al)$
\end{tabular}
}

\medskip

{\tiny
Example for binary lists: $w=\langle 1, 0, 0 \rangle$:

$$ \un{w}={\red \lambda s_0}^{\black (\al \rightarrow \al)}. {\red \lambda s_1}^{\black (\al \rightarrow \al)}.
{\blue \lambda x}^{\black \al}. (s_1\;(s_0\; (s_0\; x)))~.$$
}
\end{itemize}

\end{frame} 

%----------
\begin{frame} \frametitle{Intuitionistic Proof-Nets for DLAL terms}

\vspace{-5mm}
$(A \fli B)^{\star}=\bs A^{\star} \fm B^{\star}$

%\smallskip
%$\moda_i= \bs \mbox{ or } \pa$
  
\vspace{-7mm}

\begin{figure} %[ht]
\begin{center}
\input PN_35.pstex_t
\end{center}
%\caption{Lambda terms and Light proof-nets.}\label{schema1}

\end{figure}

\vspace{-4mm}

\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{Proof-net reduction}

\vspace{-5mm}
\begin{figure} %[ht]
\begin{center}
\input redPN_mult25.pstex_t \hspace{12mm} \input redPN_cont25.pstex_t

\input redPN_!!25.pstex_t
\hspace{12mm}\input redPN_pp25.pstex_t
\end{center}
%\caption{Lambda terms and Light proof-nets.}\label{schema1}
\end{figure}
%\vspace{-5mm}
During normalization: the depth of an edge is unchanged.
\end{frame} 

%----------
\begin{frame} \frametitle{Example}

$$M= (\la f. (f \;(f \; x)))((\la h. h) \; g) $$
 It can be given the following simple type:

$$M= (\la f^{\blue \al \rightarrow \al}. (f \;(f \; x^{\blue \al}))((\la h^{\blue \al \rightarrow \al}. h) \; g^{\blue \al \rightarrow \al}) : {\blue \al} $$

\end{frame} 


%----------
\begin{frame} \frametitle{Example}

$$M= (\la f. (f \;(f \; x)))((\la h. h) \; g) $$

\begin{figure}[ht]
\begin{center}
\input exemplesquelette40.pstex_t   %% réduire à échelle 40 ?
%\input exemplesquelette60.pstex_t
\end{center}
%\caption{Example of Classical Proof-Net.}\label{exampleCPN}
\end{figure}

\end{frame} 

%------------------
\begin{frame} \frametitle{Example of type derivation}

$$M= (\la f. (f \;(f \; x)))((\la h. h) \; g) $$

%\hspace{-5mm}
\begin{center}
\begin{figure}[ht]
{\tiny
\begin{prooftree}
%\AxiomC{$;f_1: \al \fm \al \vdash f_1: \al \fm \al$ }
%\AxiomC{$;f_2: \al \fm \al \vdash f_2: \al \fm \al$ }
%\AxiomC{$;x: \al \vdash x: \al$ }
%\BinaryInfC{$; f_2: \al \fm \al , x: \al   \vdash (f_2) \; x: \al  $}
\AxiomC{\dots}
\UnaryInfC{$; f_2: \al \fm \al , x: \al   \vdash (f_2) \; x: \al  $}
\AxiomC{$;f_1: \al \fm \al \vdash f_1: \al \fm \al$ }
   \kernHyps{10mm}  
\BinaryInfC{$; f_1: \beta, f_2: \beta, x: \al \vdash (f_1) \; ((f_2) \; x ): \al$}
 \LeftLabel{($\pa$ i)}\UnaryInfC{{\blue $ f_1: \beta, f_2: \beta; x: \pa \al \vdash (f_1) \; ((f_2) \; x ): \pa \al$}}
\UnaryInfC{$ f: \beta; x: \pa \al \vdash (f) \; ((f) \; x ): \pa \al$}
\UnaryInfC{$ ; x:\pa \al  \vdash\la f.  (f) \; ((f) \; x ):  \beta \fli \pa \al $}

%\AxiomC{$;g: \al \fm \al\vdash g: \al \fm \al$ }
\AxiomC{$;h: \beta\vdash h: \beta$ }
\UnaryInfC{$; \vdash \la h . h:  \beta \fm  \beta $}
\AxiomC{$;g: \beta\vdash g: \beta$ }
%{\red
 \BinaryInfC{{\red $; g: \beta \vdash (\la h . h)\; g: \beta $}}
%}
\insertBetweenHyps{\hspace{-1.9cm}}
\LeftLabel{($\fli$ e)}\BinaryInfC{$g: \beta; x: \pa \al \vdash (\la f.  (f) \; ((f) \; x ))  ((\la h . h)\; g): \pa \al $}
\end{prooftree}
}
where $\beta=\al \fm \al .$
\end{figure}
\end{center}
\end{frame} 

%---------------
\begin{frame} \frametitle{Example}

$$M= (\la f. {\blue (f \;(f \; x))}){\red ((\la h. h) \; g)} $$

%\vspace{-4mm} 
%we want to turn it into an (intuitionistic) proof-net like: %PN like:

%{\tiny
%$
%\begin{array}{ccc}
%@ &  = & (\fm L) \\
%\la & = & (\fm R)
%\end{array}
%$
%}
\begin{figure}[ht]
\begin{center}
\input examplePNcolors40.pstex_t
%\input examplePN40.pstex_t   
\end{center}
%\caption{Example of Classical Proof-Net.}\label{exampleCPN}
\end{figure}

\end{frame} 



%-----------
\begin{frame} \frametitle{Boxes}
\vspace{-3mm} 
Boxes in linear logic proof-nets have 2 characteristics:
\begin{enumerate}
\item \textit{logically:}

 they correspond to a sequentiality information on the graph.
\item \textit{dynamically:}

 they delimitate portions of the graph that can be duplicated.
\end{enumerate}
 Note that in LAL, (2) is not relevant for $\pa$ boxes, since they
cannot be duplicated.

 In Light logics, the crucial point of boxes is that they allow to define
some \textit{invariants} of the dynamics of the graphs:
\begin{itemize}
\item depth of edges,
\item quantitative invariant: the number of inputs of
duplicable boxes ($\bs$ boxes) is at most one.
\end{itemize} 
%In fact, the $\pa$ boxes can be dropped if we manage to maintain
% in another way the invariant of depth.
\end{frame} 

%----------
\begin{frame} \frametitle{DLAL: complexity bounds}

 DLAL satisfies the subject-reduction property.

\medskip

\begin{theo}[Strong Ptime bound]
If $t$ is typable in DLAL with a derivation of depth 
 $d$, then 
any $\beta$ reduction of $t$ can be performed in 
time $O((d+1)\cdot|t|^{2^{d+1}})$.
%sequence of $\beta$-reducts of $t$ 
%has length bounded by  $O((d+1)\cdot|t|^{2^{d+1}})$.
\end{theo}

Remarks:
\begin{itemize}
%\item we are dealing here with $\beta$-réduction,
%and not anymore with proof-net reduction;
\item one in fact shows a bound $O((d+1)\cdot|t|^{2^{d}})$ on the \textit{number} 
of $\beta$-steps and then uses the fact that the cost of each step is here bounded; 
\item this bound holds for any reduction strategy;
\item in particular, if $\vdash t: W \fm \S^k W$ then $t$ is Ptime.
\end{itemize}

%\medskip
%Note that here the bound is with respect to $\beta$ reduction: the boxing structure
%is not needed for polynomial time evaluation.
%\medskip
 %
%\begin{theo}[Completeness]
% For any polynomial time function $f:\{0,1\}^{\ast} \rightarrow \{0,1\}^{\ast}$,
%there exists a term $t$ representing it and typable
%in DLAL with a type $W \fm \pa^k W$, for a certain integer $k\in \NN$. 
%\end{theo}
% However  DLAL is not very expressive from an intensional point of view:
%some simple Ptime lambda terms might not be typable.
\end{frame} 

%----------

%\overlays{1}{
\begin{frame} \frametitle{Coercions in DLAL}
\vspace{-4mm}
 In practice we often need to change the type of arguments,
for instance from $\pa N$ to $N$, or from non-linear to linear position.

This is possible for \textit{data} arguments (\textit{e.g.} $N$ or
$W$), thanks to \textit{coercions}.

\smallskip

%dans  ILAL on avait: $coerc^{p,q}: N \fm \pa^{p+1} \bs ^q N$

In DLAL one can define terms with the following types:


$\begin{array}{cccc}
 \mbox{coer}_1 &:& N \fm \pa N & \\
\mbox{coer}_2  &:& \pa (N \fli A) \fm (N \fm \pa A)
\end{array}
$

such that:

 $\begin{array}{cccc}
 (\mbox{coer}_1 \; \un{n})&\rightarrow &\un{n}\\
(\mbox{coer}_2 \; t \; \un{n})  &\rightarrow & (t \; \un{n})
\end{array}
$

 Similarly, there exists a term contracting arguments by:


$\begin{array}{cccc}
 \mbox{cont} &:& \pa (N \fli N \fm A) \fm (N \fm \pa A)
\end{array}
$
 with:

 $\begin{array}{cccc}
 (\mbox{cont} \;t\;  \un{n})&\rightarrow & (t \; \un{n} \; \un{n} )\\
\end{array}
$

%
%exemple: 
%
%$\begin{array}{cccc}
% mult &:& N \fli (N \fm \pa N) & \\
%mult' &:& N \fm \pa (N \fm \pa N) & \mbox{ par  (coerc1)}\\
%mult'' &:& N \fm N \fm \pa \pa N & \mbox{ par (coerc2)}
%\end{array}
%$


\begin{prop}
 If $P \in \mathbb{N}[X]$, then there exists a term $t_P$ representing
$P$ and an integer $k$ such that: $\vdash_{DLAL} t_P: N \fm \pa^k N$.
\end{prop}
\end{frame} 


%----------
\begin{frame} \frametitle{DLAL: PTIME extensional completeness}
 
\bigskip 

\begin{theo}[Completeness]
 For any polynomial time function $f:\{0,1\}^{\ast} \rightarrow \{0,1\}^{\ast}$,
there exists a term $t$ representing it and typable
in DLAL with a type $W \fm \pa^k W$, for a certain integer $k\in \NN$. 
%The functions representable by terms typeable in DLAL
%are exactly the functions of FP.
\end{theo}
\medskip

 However  DLAL (or LAL) is not very expressive from an intensional point of view:
some simple Ptime lambda terms might not be typable.
\end{frame} 

%%-----------
%\begin{frame} \frametitle{Relating the Bellantoni-Cook algebra and Linear logic}
%
% We show how to embed a variant of BC into DLAL, following Murawski/Ong [MO04]
%(see also Tranquilli's Master thesis, 2005)
%
%\medskip
%
%\begin{tabular}{c}
% $f(\vec{x}; \vec{y})$ will be represented by\\
% $; \vec{x}: W, \vec{y}:\pa^k W \vdash_{DLAL} t: \pa^k W$, for some $k$
%\end{tabular}
%
%\medskip
%
%Note that:
%\begin{itemize}
%\item in $f(\vec{x}; \vec{y})$,  $\vec{x}$ stands
%for $x_1, \dots, x_n$,
%\item in the DLAL judgement,  $; \vec{x}: W$ stands for
% $x_1:W, \dots, x_n:W$.
%
%\end{itemize}
%\end{frame} 
%
%
%
%%------------
%\begin{frame} \frametitle{The algebra $\mbox{BC}^-$}
%
% In the DLAL judgements given, observe that normal variables (of type $W$) can be contracted,
%but that safe ones (of type $\pa^k W$) cannot.
%
%Fragment of BC with non-contractible safe variables:  $\mbox{BC}^-$.
%
%\medskip
%$\mbox{BC}^-$ is defined by:
%
%\begin{tabular}{cc}
%recursion: & $f(\epsilon, \vec{x}; \vec{y})=h(\vec{x};\vec{y})$\\
%           & $f(a.z, \vec{x}; \vec{y})=g(a,z,\vec{x};f(z, \vec{x}; \vec{y}))$\\
%composition: &
%\end{tabular}
% $f(\vec{x}; \vec{y})= g(h_1(\vec{x};), \dots, h_m(\vec{x};);h_{m+1} (\vec{x};\vec{y_1}), \dots,
% h_{k} (\vec{x};\vec{y_i}))$
%
%where $\vec{y_1},\dots, \vec{y_i}$ is a partition of $\vec{y}$.
%
%basic functions: as in BC.
%\end{frame} 
%
%
%%------------
%\begin{frame} \frametitle{$\mbox{BC}^-$ inside DLAL}
%
%%\bigskip
%
%\begin{prop}{[MO04]}
% The algebra  $\mbox{BC}^-$ can be embedded in DLAL.
%\end{prop}
%
%
% However $\mbox{BC}^-$ is (presumably) not complete for PTIME.
%\medskip
%
%But  one can consider extra constructs to enrich the algebra:
%
%\begin{itemize}
%\item a form of \textit{definition by cases}
% $$ \mbox{case}_K(;u)[p_1:f_1|\dots |p_m:f_m|\mbox{else}:f_{m+1}]$$
%\item a restricted \textit{recursion on safe arguments}: $\sigma\mbox{rec}$
%
%$\begin{array}{ccc}
% f(\vec{x}; \epsilon, \vec{y})&=& h(\vec{x}; \vec{y})\\
% f(\vec{x}; a.z, \vec{y})&=& \mbox{step}_i(; f(\vec{x};z,\vec{y}))
%\end{array}
%$
%
%with $\mbox{step}_i$ of a specific form (permutation)
%\end{itemize}
% See [MO04] for complete definitions.
%\end{frame} 
%
%
%%------------
%\begin{frame} \frametitle{Extension of $\mbox{BC}^-$}
%
%Let $\mbox{BC}^{\pm}$ be the algebra defined as $\mbox{BC}^-$ but with these 2 new constructs.
%
%\begin{theo}{[MO04]}
%\begin{enumerate} 
%\item $\mbox{BC}^{\pm}$ is sound and extensionally complete for PTIME,
%\item $\mbox{BC}^{\pm}$ can be embedded in DLAL.
%\end{enumerate}
%\end{theo}
%The second point comes from the fact that the new constructs can be represented
%in DLAL.
%\end{frame} 

%------------
\begin{frame} \frametitle{Conclusion}

\begin{itemize}
\item Other type systems derived from LL characterize different complexity classes:
Logspace [Schöpp07], Pspace [GMR08]
\item the relations between different the light logics and possible ways
to unfiy them are still to explore
\item type inference can be performed by constraints solving (e.g. for DLAL)
\item this approach has a modest intensional expressivity

 could it be combined to other ICC systems for more flexibility~?   
\end{itemize}
\end{frame} 
%%------------
%\begin{frame} \frametitle{Some other directions in ICC}
%
%\begin{itemize}
%\item higher-order type systems for safe recursion
%(Hofmann 00, Bellantoni-Niggl-Schwichtenberg 00)
%\item non-size-increasing computation: linear 
%type system with a basic type $\diamond$ (Hofmann 03)
%\item functional languages with restricted operations
%(no $\mathtt{cons}$): characterizations of Ptime,
%Logspace (Jones 99) 
%\end{itemize}
%
%\end{frame} 
%%------------
%\begin{frame} \frametitle{Conclusion on ICC}
%ICC has provided:
%\begin{enumerate}
% \item some machine-independent characterizations of complexity classes of functions,
%\item some criteria for verifying statically that a program,
%admits a certain complexity bound.
%\end{enumerate}
% For (1) it would be useful to relate together the various approaches.
%
%\smallskip 
%
% For (2): some recent works  try to take advantage of techniques coming
%from termination analysis (e.g. size-change-principle) and possibly
%from abstraction techniques.
%
%\end{frame} 

\end{document}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%% REGLES POUR DLAL %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame} \frametitle{DLAL rules}
%\DefaultTransition{Dissolve}
{\tiny
\begin{center}
\begin{tabular}{l@{\hspace{-2mm}}l}
  {\infer[\mbox{(Id)}]{; x:A \vdash x:A}{}} & \\
% &\\
 {\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]

{\infer[\mbox{($\fli$ i)}]{\Gamma_1; \Delta_1 \vdash \la x. t: A \fli B }
 {\Gamma_1, x:A ; \Delta_1\vdash t:B}}
  & 
{\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}}

\\[1ex]
{\infer[\mbox{(Weak)}]{\Gamma_1, \Gamma_2; \Delta_1, \Delta_2 \vdash t: A }
 {\Gamma_1; \Delta_1 \vdash t:A}}
  &
{\infer[\mbox{(Cntr)}]{x:A, \Gamma_1; \Delta_1 \vdash t[x \slash x_1, x \slash x_2] :B }{x_1:A,x_2:A, \Gamma_1; \Delta_1 \vdash t:B }}
 
\\[1ex]
{\infer[\mbox{($\pa$ i)}]{\Gamma ; x_1:\pa B_1, \dots, x_n:\pa B_n  \vdash t: \pa A }
 {  ; \Gamma, x_1:B_1, \dots, x_n:B_n \vdash t:A}}
  &
{\infer[\mbox{\hspace{-1mm}($\pa$ e)}]{\Gamma_1,\Gamma_2; \Delta_1, \Delta_2 \vdash t[u \slash x] :B }
  {\Gamma_1; \Delta_1 \vdash u: \pa A  & \Gamma_2; x:\pa A, \Delta_2 \vdash t:B}}
\\[1ex]
{\infer[\mbox{($\forall$ i) (*)}]{{ \Gamma_1; \Delta_1 \vdash  t:\forall \alpha. A}}{{ \Gamma_1; \Delta_1 \vdash t:A}}}
 &
 {\infer[\mbox{($\forall$ e)}]{\Gamma_1; \Delta_1 \vdash t:A[B \slash \al] }
{\Gamma_1; \Delta_1 \vdash t:\forall \al. A}} 
 \end{tabular}
}
\end{center}
\end{frame}
