Index: CSL17/DICE2017_TALK/unboundedArithmetic.pdf
===================================================================
Cannot display: file marked as a binary type.
svn:mime-type = application/octet-stream
Index: CSL17/DICE2017_TALK/ph-macros.tex
===================================================================
--- CSL17/DICE2017_TALK/ph-macros.tex	(revision 188)
+++ CSL17/DICE2017_TALK/ph-macros.tex	(revision 189)
@@ -5,6 +5,7 @@
 
 %\newtheorem{theorem}{Theorem}
 \newtheorem{proposition}[theorem]{Proposition}
+\newtheorem{conjecture}[theorem]{Conjecture}
 %\newtheorem{lemma}[theorem]{Lemma}
 %
 %
@@ -15,7 +16,13 @@
 \newcommand{\Nat}{\mathbb{N}}
 \newcommand{\arith}{B}
 \newcommand{\basic}{\mathit{BASIC}}
+\newcommand{\RC}{RC}                                           % name for ramified classical logic
+\newcommand{\RCi}{$\Sigma_i^{{N_0}}$-RC}
+\newcommand{\safeRC}{$\Sigma^{{N_0}}$-RC}
 
+
+
+
 \newcommand{\ind}{\mathit{IND}}
 \newcommand{\pind}{\mathit{PIND}}
 \newcommand{\cind}[1]{#1\text{-}\ind}
Index: CSL17/DICE2017_TALK/unboundedArithmetic.synctex.gz
===================================================================
Cannot display: file marked as a binary type.
svn:mime-type = application/octet-stream
Index: CSL17/DICE2017_TALK/unboundedArithmetic.aux
===================================================================
--- CSL17/DICE2017_TALK/unboundedArithmetic.aux	(revision 188)
+++ CSL17/DICE2017_TALK/unboundedArithmetic.aux	(revision 189)
@@ -30,8 +30,20 @@
 \@writefile{nav}{\headcommand {\beamer@framepages {6}{6}}}
 \@writefile{nav}{\headcommand {\slideentry {0}{0}{7}{7/7}{}{0}}}
 \@writefile{nav}{\headcommand {\beamer@framepages {7}{7}}}
-\@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}}}
+\@writefile{nav}{\headcommand {\slideentry {0}{0}{8}{8/8}{}{0}}}
+\@writefile{nav}{\headcommand {\beamer@framepages {8}{8}}}
+\@writefile{nav}{\headcommand {\slideentry {0}{0}{9}{9/9}{}{0}}}
+\@writefile{nav}{\headcommand {\beamer@framepages {9}{9}}}
+\@writefile{nav}{\headcommand {\slideentry {0}{0}{10}{10/10}{}{0}}}
+\@writefile{nav}{\headcommand {\beamer@framepages {10}{10}}}
+\@writefile{nav}{\headcommand {\slideentry {0}{0}{11}{11/11}{}{0}}}
+\@writefile{nav}{\headcommand {\beamer@framepages {11}{11}}}
+\@writefile{nav}{\headcommand {\slideentry {0}{0}{12}{12/12}{}{0}}}
+\@writefile{nav}{\headcommand {\beamer@framepages {12}{12}}}
+\@writefile{nav}{\headcommand {\slideentry {0}{0}{13}{13/13}{}{0}}}
+\@writefile{nav}{\headcommand {\beamer@framepages {13}{13}}}
+\@writefile{nav}{\headcommand {\beamer@partpages {1}{13}}}
+\@writefile{nav}{\headcommand {\beamer@subsectionpages {1}{13}}}
+\@writefile{nav}{\headcommand {\beamer@sectionpages {1}{13}}}
+\@writefile{nav}{\headcommand {\beamer@documentpages {13}}}
+\@writefile{nav}{\headcommand {\def \inserttotalframenumber {13}}}
Index: CSL17/DICE2017_TALK/unboundedArithmetic.tex
===================================================================
--- CSL17/DICE2017_TALK/unboundedArithmetic.tex	(revision 188)
+++ CSL17/DICE2017_TALK/unboundedArithmetic.tex	(revision 189)
@@ -163,7 +163,7 @@
  
  \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
+\item in particular, {\ICC{ICC logics}}  not so satisfactory for non-deterministic classes
 
 e.g. NP, PH (polynomial hierarchy) \dots
 
@@ -185,14 +185,14 @@
 \begin{frame}
   \frametitle{Our goal}
  
- design an { \ICC{unbounded}} {\BA{arithmetic}} for characterizing FPH
+ 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
+\item enlarge the toolbox  of {\ICC{ICC logics}}, by exploring the power of quantification (under-investigated in ICC)
 \end{itemize}
  \end{frame}
 
@@ -203,1994 +203,143 @@
  
  We want to use:
  \begin{itemize}
-\item {\ICC{ramification}}   
-\item
+\item {\ICC{ramification}} (distinction safe / normal arguments) from   {\ICC{ICC}}
+   \item induction calibrated by logical complexity, from  {\BA{bounded arithmetic}}
 \end{itemize}
  \end{frame}
 
-
-\end{document}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%----------
-
 %%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \begin{frame}
-  \frametitle{}
+  \frametitle{Ingredients for a logical characterization}
  
  \begin{itemize}
-\item   \end{itemize}
+\item  choose a way to \textit{specify} functions
+\item choose a logic:
+
+logical system + axioms, induction scheme
+\item prove soundness:
+
+realizability-like argument, with a well-chosen \textit{target language}
+\item prove completeness
+\end{itemize}
  \end{frame}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \begin{frame}
-  \frametitle{Introduction}
+  \frametitle{Specifying the functions}
  
+ Various approaches to specify a function $f$:
  \begin{itemize}
-\item  \textit{Implicit computational complexity} (ICC) : 
+\item   {\BA{formula specification}} (bounded arithmetic):
 
-characterizing complexity classes by programming languages / calculi  without  explicit bounds, 
+a formula $A_f$ defines the graph of $f$
+\item {\ICC{equational specification}} (Leivant: intrinsic theories)
 
-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}
+conjunction of first-order equations defining $f$
 
+\item applicative theories (Cantini, Kahle-Oitavem \dots)
 
- \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}
+combinatory term computing $f$
+\item \dots
 
-  \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{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{frame}
+  \frametitle{Our logical system}
  
-$$\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}
-
+ Ramified classical logic (\RC):
+ \begin{itemize}
+\item  1st-order classical logic \dots
+\item \dots over the language:
 \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}
-$$
+ \item functions and constants: $0, \succ, +, \cdot, \smsh, |.|$
+ \item predicates: $\leq, {\ICC{N_0}},  {\ICC{N_1}}$
 \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 $$
-
+\item with axioms:
+ \begin{itemize}
+\item BASIC theory: defining $\succ, +, \cdot, \smsh, |.|$ (as in Buss' $S_1$)
 \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}
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+notation:
 
-\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\\
+$\begin{array}{lcl}
+\succ{0}x &:=& 2\cdot x\\
+\succ{1}x & :=& \succ{}(2\cdot x)
 \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
+ $
+      \item polynomial induction IND:
  \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}
+ {\small $$    A(0) 
+\rightarrow (\forall x^{\normal} . ( A(x) \rightarrow A(\succ{0} x) ) )
+\rightarrow  (\forall x^{\normal} . ( A(x) \rightarrow A(\succ{1} x) ) ) 
+\rightarrow  \forall x^{\normal} . A(x) $$
+   }
+   
+   Define all that within a sequent calculus system.
+   
+  $\mathcal{C}$-\RC\  is \RC\ with IND restricted to formulas $A$ belonging to the class  $\mathcal{C}$ of formulas.
+ \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):
+\begin{frame}
+  \frametitle{Classification of quantifications}
  
- 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$.
+ Write $Q$ for $\forall$ or $\exists$.
+ \begin{itemize}
+\item   safe ($N_0$)/normal ($N_1$) quantifiers:
 
+$$Q^{N_i}x.A := Qx.(N_i(x) \rightarrow A)$$
+\item sharply bounded quantifiers:
+$$Q^{N_i}|x|\leq t.\; A := Qx.(N_i(x) \rightarrow (|x|\leq t) \rightarrow A)$$
 \end{itemize}
-\end{frame}
-%%%%%%%%%
+ \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{frame}
+  \frametitle{Quantifier hierarchy}
  
-\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$.
+ We define:
+ \begin{itemize}
+\item $\Sigma^\safe_0 = \Pi^\safe_0 $= formulas with only sharply bounded quantifiers,
+\item $\Sigma^\safe_{i+1}$= closure of $\Pi^\safe_i $ under $\cor, \cand $, safe existentials and sharply bounded quantifiers,
+\item  $\Pi^\safe_{i+1}$ = closure of $\Sigma^\safe_i $ under $\cor, \cand $, safe universals and sharply bounded quantifiers,
+\item $\Sigma^\safe= \cup_i \Sigma^\safe_i$.
 \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.
+\begin{frame}
+  \frametitle{Result and work-in-progress}
  
-\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:
+ \begin{theorem}[Soundness]
+  If $f$ is provably total in \RCi\, then $f$ belongs to $\fphi{i}$.
+ \end{theorem}
  
- 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{conjecture}[Soundness]
+  If $f$ is provably total in \RCi\, then $f$ belongs to $\fphi{i}$.
+ \end{conjecture}
 
-%%%%%%%%%
-\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}
+\begin{frame}
+  \frametitle{}
  
-\bigskip 
+ \begin{itemize}
+\item   \end{itemize}
+ \end{frame}
 
-\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}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%
Index: CSL17/DICE2017_TALK/unboundedArithmetic.log
===================================================================
--- CSL17/DICE2017_TALK/unboundedArithmetic.log	(revision 188)
+++ CSL17/DICE2017_TALK/unboundedArithmetic.log	(revision 189)
@@ -1,4 +1,4 @@
-This is pdfTeX, Version 3.1415926-2.4-1.40.13 (TeX Live 2012) (format=pdflatex 2012.6.30)  22 APR 2017 00:02
+This is pdfTeX, Version 3.1415926-2.4-1.40.13 (TeX Live 2012) (format=pdflatex 2012.6.30)  22 APR 2017 02:02
 entering extended mode
  \write18 enabled.
  file:line:error style messages enabled.
@@ -1066,6 +1066,63 @@
 [7
 
 ]
+Overfull \hbox (30.40973pt too wide) has occurred while \output is active
+ [][][][]  
+ []
+
+[8
+
+]
+Overfull \hbox (30.40973pt too wide) has occurred while \output is active
+ [][][][]  
+ []
+
+[9
+
+]
+Overfull \hbox (5.31305pt too wide) detected at line 285
+\OT1/mathkerncmss/m/sl/10 A\OT1/cmss/m/n/10 (0) \OMS/cmsy/m/n/10 ! \OT1/cmss/m/
+n/10 (\OMS/cmsy/m/n/10 8\OT1/mathkerncmss/m/sl/10 x[]\OML/cmm/m/it/10 :\OT1/cms
+s/m/n/10 (\OT1/mathkerncmss/m/sl/10 A\OT1/cmss/m/n/10 (\OT1/mathkerncmss/m/sl/1
+0 x\OT1/cmss/m/n/10 ) \OMS/cmsy/m/n/10 ! \OT1/mathkerncmss/m/sl/10 A\OT1/cmss/m
+/n/10 (\OT1/mathkerncmss/m/sl/10 s[]x\OT1/cmss/m/n/10 ))) \OMS/cmsy/m/n/10 ! \O
+T1/cmss/m/n/10 (\OMS/cmsy/m/n/10 8\OT1/mathkerncmss/m/sl/10 x[]\OML/cmm/m/it/10
+ :\OT1/cmss/m/n/10 (\OT1/mathkerncmss/m/sl/10 A\OT1/cmss/m/n/10 (\OT1/mathkernc
+mss/m/sl/10 x\OT1/cmss/m/n/10 ) \OMS/cmsy/m/n/10 ! \OT1/mathkerncmss/m/sl/10 A\
+OT1/cmss/m/n/10 (\OT1/mathkerncmss/m/sl/10 s[]x\OT1/cmss/m/n/10 ))) \OMS/cmsy/m
+/n/10 ! 8\OT1/mathkerncmss/m/sl/10 x[]\OML/cmm/m/it/10 :\OT1/mathkerncmss/m/sl/
+10 A\OT1/cmss/m/n/10 (\OT1/mathkerncmss/m/sl/10 x\OT1/cmss/m/n/10 )
+ []
+
+
+Overfull \hbox (30.40973pt too wide) has occurred while \output is active
+ [][][][]  
+ []
+
+[10
+
+]
+Overfull \hbox (30.40973pt too wide) has occurred while \output is active
+ [][][][]  
+ []
+
+[11
+
+]
+Overfull \hbox (30.40973pt too wide) has occurred while \output is active
+ [][][][]  
+ []
+
+[12
+
+]
+Overfull \hbox (30.40973pt too wide) has occurred while \output is active
+ [][][][]  
+ []
+
+[13
+
+]
 \tf@nav=\write6
 \openout6 = `unboundedArithmetic.nav'.
 
@@ -1075,11 +1132,11 @@
 \tf@snm=\write8
 \openout8 = `unboundedArithmetic.snm'.
 
-Package atveryend Info: Empty hook `BeforeClearDocument' on input line 212.
-Package atveryend Info: Empty hook `AfterLastShipout' on input line 212.
+Package atveryend Info: Empty hook `BeforeClearDocument' on input line 330.
+Package atveryend Info: Empty hook `AfterLastShipout' on input line 330.
  (./unboundedArithmetic.aux)
-Package atveryend Info: Executing hook `AtVeryEndDocument' on input line 212.
-Package atveryend Info: Executing hook `AtEndAfterFileList' on input line 212.
+Package atveryend Info: Executing hook `AtVeryEndDocument' on input line 330.
+Package atveryend Info: Executing hook `AtEndAfterFileList' on input line 330.
 Package rerunfilecheck Info: File `unboundedArithmetic.out' has not changed.
 (rerunfilecheck)             Checksum: D41D8CD98F00B204E9800998ECF8427E;0.
 
@@ -1087,27 +1144,29 @@
 LaTeX Font Warning: Size substitutions with differences
 (Font)              up to 1.0pt have occurred.
 
-Package atveryend Info: Empty hook `AtVeryVeryEnd' on input line 212.
+Package atveryend Info: Empty hook `AtVeryVeryEnd' on input line 330.
  ) 
 Here is how much of TeX's memory you used:
- 16135 strings out of 493488
- 301549 string characters out of 3141326
- 375926 words of memory out of 3000000
- 19007 multiletter control sequences out of 15000+200000
- 11676 words of font info for 45 fonts, out of 3000000 for 9000
+ 16246 strings out of 493488
+ 303725 string characters out of 3141326
+ 378999 words of memory out of 3000000
+ 19100 multiletter control sequences out of 15000+200000
+ 16100 words of font info for 64 fonts, out of 3000000 for 9000
  957 hyphenation exceptions out of 8191
- 49i,16n,62p,455b,549s stack positions out of 5000i,500n,10000p,200000b,50000s
+ 49i,16n,62p,455b,587s stack positions out of 5000i,500n,10000p,200000b,50000s
 </usr/local/texlive/2012/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb
-></usr/local/texlive/2012/texmf-dist/fonts/type1/public/amsfonts/cm/cmss10.pfb>
-</usr/local/texlive/2012/texmf-dist/fonts/type1/public/amsfonts/cm/cmss12.pfb><
-/usr/local/texlive/2012/texmf-dist/fonts/type1/public/amsfonts/cm/cmss8.pfb></u
-sr/local/texlive/2012/texmf-dist/fonts/type1/public/amsfonts/cm/cmssi10.pfb></u
-sr/local/texlive/2012/texmf-dist/fonts/type1/public/amsfonts/cm/cmssi8.pfb></us
-r/local/texlive/2012/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb>
-Output written on unboundedArithmetic.pdf (7 pages, 83999 bytes).
+></usr/local/texlive/2012/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb><
+/usr/local/texlive/2012/texmf-dist/fonts/type1/public/amsfonts/cm/cmss10.pfb></
+usr/local/texlive/2012/texmf-dist/fonts/type1/public/amsfonts/cm/cmss12.pfb></u
+sr/local/texlive/2012/texmf-dist/fonts/type1/public/amsfonts/cm/cmss8.pfb></usr
+/local/texlive/2012/texmf-dist/fonts/type1/public/amsfonts/cm/cmssi10.pfb></usr
+/local/texlive/2012/texmf-dist/fonts/type1/public/amsfonts/cm/cmssi8.pfb></usr/
+local/texlive/2012/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/l
+ocal/texlive/2012/texmf-dist/fonts/type1/public/amsfonts/latxfont/lasy10.pfb>
+Output written on unboundedArithmetic.pdf (13 pages, 117179 bytes).
 PDF statistics:
- 250 PDF objects out of 1000 (max. 8388607)
- 218 compressed objects within 3 object streams
- 15 named destinations out of 1000 (max. 500000)
- 79 words of extra memory for PDF output out of 10000 (max. 10000000)
+ 422 PDF objects out of 1000 (max. 8388607)
+ 379 compressed objects within 4 object streams
+ 27 named destinations out of 1000 (max. 500000)
+ 91 words of extra memory for PDF output out of 10000 (max. 10000000)
 
Index: CSL17/DICE2017_TALK/unboundedArithmetic.nav
===================================================================
--- CSL17/DICE2017_TALK/unboundedArithmetic.nav	(revision 188)
+++ CSL17/DICE2017_TALK/unboundedArithmetic.nav	(revision 189)
@@ -13,8 +13,20 @@
 \headcommand {\beamer@framepages {6}{6}}
 \headcommand {\slideentry {0}{0}{7}{7/7}{}{0}}
 \headcommand {\beamer@framepages {7}{7}}
-\headcommand {\beamer@partpages {1}{7}}
-\headcommand {\beamer@subsectionpages {1}{7}}
-\headcommand {\beamer@sectionpages {1}{7}}
-\headcommand {\beamer@documentpages {7}}
-\headcommand {\def \inserttotalframenumber {7}}
+\headcommand {\slideentry {0}{0}{8}{8/8}{}{0}}
+\headcommand {\beamer@framepages {8}{8}}
+\headcommand {\slideentry {0}{0}{9}{9/9}{}{0}}
+\headcommand {\beamer@framepages {9}{9}}
+\headcommand {\slideentry {0}{0}{10}{10/10}{}{0}}
+\headcommand {\beamer@framepages {10}{10}}
+\headcommand {\slideentry {0}{0}{11}{11/11}{}{0}}
+\headcommand {\beamer@framepages {11}{11}}
+\headcommand {\slideentry {0}{0}{12}{12/12}{}{0}}
+\headcommand {\beamer@framepages {12}{12}}
+\headcommand {\slideentry {0}{0}{13}{13/13}{}{0}}
+\headcommand {\beamer@framepages {13}{13}}
+\headcommand {\beamer@partpages {1}{13}}
+\headcommand {\beamer@subsectionpages {1}{13}}
+\headcommand {\beamer@sectionpages {1}{13}}
+\headcommand {\beamer@documentpages {13}}
+\headcommand {\def \inserttotalframenumber {13}}
