
%\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\\
DICE-FOPARA 2017 workshop, Uppsala}


\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\\
arithmetic & arithmetics / logics\\
 & \\
 large variety of & resource-free characterizations of\\
 complexity classes & complexity classes (e.g. ramification)\\
 &\\
 correspondence 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_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}
  \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, {\ICC{ICC logics}}  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  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_1\subsetneq s_2 \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}
  \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  of {\ICC{ICC logics}}, by exploring the power of quantification (under-investigated in ICC)
\end{itemize}
 \end{frame}

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

\begin{frame}
  \frametitle{Methodology}
 
 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}:
%   
%   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}

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

\begin{frame}
  \frametitle{Ramification}
 
 \begin{itemize}
\item   ramification, a.k.a. tiering, safe recursion
\item distinguish two levels of data-types:

${\red{N_1}}$ (\textit{normal}) integers can trigger induction/recursion

${{N_0}}$ (\textit{safe})  integers cannot; they can just be finitely explored

%\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 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}
 
 \begin{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{Specifying the functions}
 
 Various approaches at hand to specify a function $f$ in a logic:
 \begin{itemize}
\item   {\BA{formula specification}} (bounded arithmetic):

a formula $A_f$ defines the graph of $f$
\item {\ICC{equational specification}} (Leivant: intrinsic theories)

conjunction of first-order equations defining $f$

\item combinatory terms (applicative theories: Feferman, Cantini, Kahle-Oitavem \dots)

terms of combinatory algebra computing $f$
\item \dots

\end{itemize}
 \end{frame}

\begin{frame}
  \frametitle{Our logical system}
 
 Ramified classical arithmetic (\RC):
 \begin{itemize}
\item  1st-order classical logic \dots
\item \dots over the language:
\begin{itemize}
 \item functions and constants: $0, \succ, +, \cdot, \smsh, |.|$
 \item predicates: $\leq, {\ICC{N_0}},  {\ICC{N_1}}$
\end{itemize}
\item with axioms:
 \begin{itemize}
\item BASIC theory: defining $\succ, +, \cdot, \smsh, |.|$ (as in Buss' $S_2$, but sorted)
\smallskip

notation:

$\begin{array}{lcl}
\succ{0}x &:=& 2\cdot x\\
\succ{1}x & :=& \succ{}(2\cdot x)
\end{array}
 $
      \item polynomial induction IND:
 \end{itemize}
 \end{itemize}
 {\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{Classification of quantifications}
 
% Write $Q$ for $\forall$ or $\exists$.
 \begin{itemize}
\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}

%%%%%%%%%%%
\begin{frame}
  \frametitle{Quantifier hierarchy}
 
 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{Result and work-in-progress}
 
 \begin{claim}[Soundness]
  If $f$ is provably total in \RCi\, then $f$ belongs to $\fphi{i}$.
 \end{claim}
 
  \begin{claim}[Completeness]
  If $f$ $f$ belongs to $\fphi{i}$ then $f$ is provably total in \RCi\ .
 \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}

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

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

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

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