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

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