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


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

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

%\bibliographystyle{plainurl}% the recommended bibstyle

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



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


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

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

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

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

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


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

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


\begin{document}
\maketitle


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

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

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

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

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

\begin{frame}
  \frametitle{{A current limitation of ICC logics}}
 
 \begin{itemize}
\item fewer complexity classes characterized by {\ICC{ICC logics}} than by {\BA{bounded arithmetic}}
\item in particular, {\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  to be done: definition \dots
 \end{itemize}
 \end{frame}

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

\begin{frame}
  \frametitle{Our goal}
 
 design an {\ICC{unbounded}} {\BA{arithmetic}} for characterizing FPH
 
 \medskip 
 
 expected benefits:
 \begin{itemize}
\item   bridge  {\BA{bounded arithmetic}}  and {\ICC{ICC logics}}
\item enlarge the toolbox  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, from  {\BA{bounded 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
\item ramified 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 
\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 to specify a function $f$:
 \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 applicative theories (Cantini, Kahle-Oitavem \dots)

combinatory term computing $f$
\item \dots

\end{itemize}
 \end{frame}

\begin{frame}
  \frametitle{Our logical system}
 
 Ramified classical logic (\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_1$)
\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$)/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}

%%%%%%%%%%%
\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{theorem}[Soundness]
  If $f$ is provably total in \RCi\, then $f$ belongs to $\fphi{i}$.
 \end{theorem}
 
  \begin{conjecture}[Soundness]
  If $f$ is provably total in \RCi\, then $f$ belongs to $\fphi{i}$.
 \end{conjecture}

\end{frame}

\end{document}

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

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

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

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