Index: unboundedArithmetic.tex
===================================================================
--- unboundedArithmetic.tex	(revision 190)
+++ unboundedArithmetic.tex	(revision 191)
@@ -105,7 +105,8 @@
 }
 
 \author{Patrick Baillot and Anupam Das}
-\institute{CNRS / ENS Lyon}
+\institute{CNRS / ENS Lyon\\
+DICE-FOPARA 2017 workshop, Uppsala}
 
 
 \begin{document}
@@ -124,14 +125,14 @@
       & \ICC{(ICC)}\\
  \hline
  &\\
- & function algebras\\
- & types/proofs-as-programs\\
- & arithmetics / logics\\
+% & function algebras\\
+% & types/proofs-as-programs\\
+arithmetic & arithmetics / logics\\
  & \\
  large variety of & resource-free characterizations of\\
  complexity classes & complexity classes (e.g. ramification)\\
  &\\
- corresp. with & extensions to programming languages\\
+ correspondence with & extensions to programming languages\\
  \textit{proof-complexity} &
  \end{tabular}
   \end{frame}
@@ -149,8 +150,8 @@
  \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))$\\
+  Buss ($S_2$): & Leivant (intrinsic theories): \\
+  $\forall x, {\exists y } . \; A_f(x,y)$ & $\forall x. N_1(x) \rightarrow N_0(f(x))$\\
   &\\
   FP, FPH & FP
   \end{tabular}
@@ -176,10 +177,45 @@
   \frametitle{Recap : the polynomial hierarchy}
  
  \begin{itemize}
-\item  to be done: definition \dots
- \end{itemize}
+\item  NP: polynomially checkable with polysize witness
+
+$NP=\Sigma_1^P$ example: $k$-CLIQUE
+
+$$\exists^{|s_1|\leq k } s_1, (|s_1|=k \cand \mbox{CLIQUE}(s_1,x))$$
+\item  $\Sigma_2^P$ example: $k$-MAXCLIQUE
+\end{itemize}
+$$ \begin{array}{l}
+ \exists^{|s_1|\leq k } s_1, \forall^{|s_2|\leq k+1 } s_2,\\
+  (|s_1|=k \cand \mbox{CLIQUE}(s_1,x) \cand (|s_2|\geq k+1 \rightarrow \neg  \mbox{CLIQUE}(s_2,x))   )
+\end{array}
+$$
+\begin{itemize}
+\item  $\Sigma_i^P$:
+$$
+ \exists^{|s_1|\leq P_1(x) } s_1, \forall^{|s_2|\leq P_2(x) } s_2, \dots  Q^{|s_i|\leq P_i(x) } s_i, 
+  \mbox{Pred}(\vec s, x)$$
+  for Pred a Ptime predicate.
+\end{itemize}
  \end{frame}
 
+
+\begin{frame}
+  \frametitle{Recap : the polynomial hierarchy}
+ 
+ \begin{itemize}
+\item polynomial hierarchy: 
+$$ \mbox{PH}= \cup_i \Sigma_i^P$$
+\item functional version:
+\begin{eqnarray*}
+  \fphi{i} &=& \mbox{FP}^{\Sigma_{i-1}^P}\\
+  \mbox{FPH} &=& \cup_i   \fphi{i} 
+  \end{eqnarray*}
+  \end{itemize}
+
+in particular:
+
+ $\fphi{1}=\mbox{FP}, \qquad \fphi{2}=\mbox{FP}^{\mbox{NP}}$.
+\end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \begin{frame}
@@ -204,7 +240,12 @@
  We want to use:
  \begin{itemize}
 \item {\ICC{ramification}} (distinction safe / normal arguments) from   {\ICC{ICC}}
-   \item induction calibrated by logical complexity, from  {\BA{bounded arithmetic}}
+   \item induction calibrated by logical complexity (quantifiers), from  {\BA{bounded arithmetic}}
+%   \item our \textit{key idea}:
+%   
+%   trade{ \BA{bounded quantifiers $\forall x \leq t$,  $\exists x \leq t$ of bounded arithmetic}}
+%   
+%   for {\ICC{unbounded \textit{safe} quantifiers $\forall^{\safe } x$,  $\exists^{\safe} x$ in a ramified arithmetic}}
 \end{itemize}
  \end{frame}
 
@@ -220,14 +261,43 @@
 ${\red{N_1}}$ (\textit{normal}) integers can trigger induction/recursion
 
 ${{N_0}}$ (\textit{safe})  integers cannot; they can just be finitely explored
-\item ramified recursion scheme:
+
+%\smallskip
+
+\item BC function algebra (Bellantoni-Cook 92):
+
+ $f({\red{\vec u}}^{\; {\red{N_1}}}{\textbf ;} \vec x^{\; N_0})$
+
+ safe recursion scheme:
 $$ f({\red{\succ{i} u, \vec v}}{\textbf ;} \vec x)=F_i ({\red{u,\vec v}}{\textbf ; }f(u, \vec v;\vec x), \vec x)$$
 \item function algebra for FP: Bellantoni-Cook 92, Leivant 93
 
-          logic for FP: Leivant 95, Cantini 00 
+          logic for FP: Leivant 95, Cantini 02, Bellantoni-Hofmann 02 
 \end{itemize}
  \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+\begin{frame}
+  \frametitle{Methodology: our key idea}
+ 
+% We want to use:
+ \begin{itemize}
+%\item {\ICC{ramification}} (distinction safe / normal arguments) from   {\ICC{ICC}}
+%   \item induction calibrated by logical complexity (quantifiers), from  {\BA{bounded arithmetic}}
+%   \item our \textit{key idea}:
+   
+\item   trade
+   
+    { \BA{bounded quantifiers $\forall x \leq t$,  $\exists x \leq t$ of bounded arithmetic}}
+   
+   for
+   
+    {\ICC{unbounded \textit{safe} quantifiers $\forall^{\safe } x$,  $\exists^{\safe} x$ in a ramified arithmetic}}
+\item calibrate the arithmetic by considering the number of ({\ICC{safe}}) quantifier alternations in induction formulas $A$, as in 
+{\BA{bounded arithmetic}}
+\end{itemize}
+ \end{frame}
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}
   \frametitle{Ingredients for a logical characterization}
@@ -249,7 +319,7 @@
 \begin{frame}
   \frametitle{Specifying the functions}
  
- Various approaches to specify a function $f$:
+ Various approaches at hand to specify a function $f$ in a logic:
  \begin{itemize}
 \item   {\BA{formula specification}} (bounded arithmetic):
 
@@ -258,9 +328,9 @@
 
 conjunction of first-order equations defining $f$
 
-\item applicative theories (Cantini, Kahle-Oitavem \dots)
+\item combinatory terms (applicative theories: Feferman, Cantini, Kahle-Oitavem \dots)
 
-combinatory term computing $f$
+terms of combinatory algebra computing $f$
 \item \dots
 
 \end{itemize}
@@ -269,7 +339,7 @@
 \begin{frame}
   \frametitle{Our logical system}
  
- Ramified classical logic (\RC):
+ Ramified classical arithmetic (\RC):
  \begin{itemize}
 \item  1st-order classical logic \dots
 \item \dots over the language:
@@ -279,7 +349,7 @@
 \end{itemize}
 \item with axioms:
  \begin{itemize}
-\item BASIC theory: defining $\succ, +, \cdot, \smsh, |.|$ (as in Buss' $S_1$)
+\item BASIC theory: defining $\succ, +, \cdot, \smsh, |.|$ (as in Buss' $S_2$, but sorted)
 \smallskip
 
 notation:
@@ -308,13 +378,19 @@
 \begin{frame}
   \frametitle{Classification of quantifications}
  
- Write $Q$ for $\forall$ or $\exists$.
+% 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)$$
+\item   safe ($N_0$) quantifiers:
+\begin{eqnarray*}
+\forall^{N_0}x.A &:=& \forall x.(N_0(x) \rightarrow A)\\
+\exists^{N_0}x.A &:=& \exists x.(N_0(x) \cand A)
+\end{eqnarray*}
+\item sharply bounded normal ($\normal$) quantifiers:
+\begin{eqnarray*}
+\forall^{N_1}x\leq |t| .A &:=& \forall x.(N_1(x) \rightarrow (x\leq |t|) \rightarrow A)\\
+\exists^{N_1}x\leq |t| .A &:=& \exists x.(N_1(x) \cand(x\leq |t|) \cand A)
+\end{eqnarray*}
+%$$Q^{N_i}x\leq |t|.\; A := Qx.(N_i(x) \rightarrow (x\leq |t|) \rightarrow A)$$
 \end{itemize}
  \end{frame}
 
@@ -336,16 +412,149 @@
 \begin{frame}
   \frametitle{Result and work-in-progress}
  
- \begin{theorem}[Soundness]
+ \begin{claim}[Soundness]
   If $f$ is provably total in \RCi\, then $f$ belongs to $\fphi{i}$.
- \end{theorem}
+ \end{claim}
  
-  \begin{conjecture}[Soundness]
+  \begin{claim}[Completeness]
   If $f$ is provably total in \RCi\, then $f$ belongs to $\fphi{i}$.
- \end{conjecture}
+ \end{claim}
 
 \end{frame}
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+  \frametitle{Proof idea for soundness: target language $\mu$BC}
+ 
+ \begin{itemize}
+\item   target language: $\mu$BC, a function algebra (Bellantoni 93) extending BC and characterizing FPH
+\item BC algebra:  $f({\red{\vec u}}^{\; {\red{N_1}}}{\textbf ;} \vec x^{\; N_0})$
+\begin{itemize}
+  \item initial functions: $p$, $\pi^n_i$, \dots
+  \item safe recursion
+  \item safe composition
+\end{itemize}
+
+BC characterizes the class FP (Bellantoni-Cook 92).
+%\item $\mu$BC: extends BC with \textit{predicative minimization}
+%
+%$f({\red{\vec u}}; \vec x):= \begin{cases}
+% s_1(\mu y.h({\red{\vec u}}; \vec x, y)\mod 2 = 0)& \mbox{ if  there exists such a $y$,} \\
+%0  & \mbox{ otherwise,}
+%\end{cases}
+%$
+%
+% $\mu \mbox{BC}^i$ functions: defined by at most $i$ nestings of minimization
+\end{itemize}
+ \end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+  \frametitle{Proof idea for soundness: target language $\mu$BC}
+ 
+ \begin{itemize}
+%\item   target language: $\mu$BC, a function algebra (Bellantoni 93) extending BC and characterizing FPH
+%\item BC algebra:  $f({\red{\vec u}}^{\; {\red{N_1}}}{\textbf ;} \vec x^{\; N_0})$
+%\begin{itemize}
+%  \item initial functions: $p$, $\pi^n_i$, \dots
+%  \item safe recursion
+%  \item safe composition
+%\end{itemize}
+%
+%BC characterizes the class FP (Bellantoni-Cook 92).
+\item $\mu$BC: extends BC with \textit{predicative minimization}
+
+$f({\red{\vec u}}; \vec x):= \begin{cases}
+ s_1(\mu y.h({\red{\vec u}}; \vec x, y)\mod 2 = 0)& \mbox{ if  there exists such a $y$,} \\
+0  & \mbox{ otherwise,}
+\end{cases}
+$
+
+ $\mu \mbox{BC}^i$ functions: defined by at most $i$ nestings of minimization
+ \item one obtains
+ 
+ \begin{theorem}[Bellantoni 92]
+ 
+ The functions of $\mu$BC are exactly those of FPH.
+ 
+ The functions of  $\mu \mbox{BC}^{\; i-1}$ are exactly those of $\fphi{i}$.
+ \end{theorem}
+\end{itemize}
+ \end{frame}
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+  \frametitle{Proving soundness}
+ 
+ Key intermediary property to prove:
+ \begin{claim}
+ If \RCi\ proves
+ $$\forall \vec u^\normal . \forall \vec x^\safe . \exists y^\safe . A(\vec u ; \vec x , y)$$
+  then there is a $\mubci{i-1}$ program $f(\vec u ; \vec x)$ such that 
+  $$\Nat \models A(\vec u ; \vec x , f(\vec u ; \vec x)).$$
+\end{claim}
+ Proof idea: use witness function method:
+ \begin{itemize}
+  \item use free-cut elimination theorem for the sequent calculus
+  \item then prove the property by induction on sequent calculus rules
+ \end{itemize}
+  \end{frame}
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+  \frametitle{Proving completeness: in progress}
+ 
+ Key intermediary claim:
+ \begin{claim}
+	\label{thm:completeness}
+	For every $\mubci{i-1}$ program $f(\vec u ; \vec x)$ (which is in $\fphi i$), there is a $\Sigma^{\safe}_i$ formula $A_f(\vec u, \vec x)$ such that \RCi\  proves $$\forall^{\normal} \vec u  . \forall^{\safe} \vec x. \exists^{\safe} ! y. A_f(\vec u , \vec x , y )$$ and $$\Nat \models \forall \vec u , \vec x. A(\vec u , \vec x , f(\vec u ; \vec x)).$$
+\end{claim}
+
+For the minimization construction case, we use \textit{well-ordering property} in \RCi\  .
+ \end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+  \frametitle{Related works}
+ 
+ Two previous results \textit{apparently} clash with our claims:
+ \begin{itemize}
+\item   Bellantoni-Hofmann 02:
+
+characterization of FP, with induction on arbitrarily quantified formulas
+
+but \dots the underlying logic is not classical logic, but linear logic
+
+\item   Cantini 02:
+
+characterization of FP in a ramified classical logic, with induction on arbitrarily quantified formulas $A$
+
+but \dots occurrences of $\safe$ in $A$ need to be positive, hence it corresponds to our $\Sigma^{\safe}_1$.
+ \end{itemize}
+ \end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}
+  \frametitle{Conclusion and perspectives}
+ 
+ \begin{itemize}
+\item   we defined a ramified arithmetic with unbounded quantification which we claim is FPH sound, and  FPH complete
+\item this yields an implicit analog of Buss' bounded arithmetic $S_2$, with a characterization of each level  $\fphi{i}$,  %by calibrating induction with quantifier alternation, 
+but where {\BA{bounded quantification}} has been replaced by {\ICC{safe quantification}}
+\item  could \RC\ be presented as a modal logic (as in  Bellantoni-Hofmann02) ?
+\item we think that \RCi\  can be directly embedded into the bounded arithmetic $S^i_2$
+%study direct relationship of \RC\ with the bounded arithmetic $S_2$
+\end{itemize}
+ \end{frame}
+
 \end{document}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
