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

%\documentclass[pdf, pleasingblue,slideColor,colorBG]{prosper}

\documentclass{beamer}

\usepackage{amsfonts,latexsym,amssymb, amsmath}

\usepackage{stmaryrd}

\usepackage{graphicx}

\usepackage{eepic}

\usepackage[dvips]{epsfig}

%\usepackage{psfig}

%\input head.tex

\usepackage{proof,bussproofs}

%\usepackage{ desseins_s}

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

%\usepackage[dvipsnames]{xcolor}

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

%\bibliographystyle{plainurl}% the recommended bibstyle

%\usepackage[lutzsyntax]{virginialake}

\input{ph-macros}

\setbeamercolor{block title}{bg=blue!10}

\setbeamercolor{block body}{bg=blue!10}

\definecolor{monred}{HTML}{9D0909}

%\definecolor{monbleu}{RVB}{0,0,1}

 \def\red#1{\color{red}{#1}}

 \def\blue#1{\color{blue}{#1}}

 \def\green#1{\color{green}{#1}}

\def\black{}

\def\BA#1{\color{red}{#1}}

 \def\ICC#1{\color{blue}{#1}}

%%%%%%%%%%%%%ENVIRONMENTS AND THEOREM-STYLES %%%%%%%%%%%%%%%%%%

%\def\un#1{\underline{#1}}

%\def\point#1{{\bf #1.}}

%%\newcommand{\etq}[1]{\mbox{\scriptsize\bf #1}}

%\newcommand{\etq}[1]{\mbox{{\bf #1}}}

%\newcommand{\Rulone}[1]{%

%          \begin{center}

%           \makebox[12cm]{\hspace*{\fill}

%                 \begin{minipage}[c]{6cm} #1 \end{minipage} \hspace*{\fill}

%                }

%          \end{center}

%  }

%

%\newcommand{\centra}[1]{\begin{center} #1 \end{center}}

%

%\newcommand{\Rultwo}[2]{%

%          \begin{center}

%           \makebox[12cm]{

%         \makebox[6cm]{\begin{minipage}[c]{6cm} #1 \end{minipage}} \hspace{20pt}

%         \makebox[6cm]{\begin{minipage}[c]{6cm} #2 \end{minipage}}

%                }

%          \end{center}

%  }

%\newcounter{ex}

%%\newtheorem{example}[ex]{Example}

%

%

%\def\para#1{\paragraph{#1}}

%\newtheorem{theo}{Theorem}

%\newtheorem{de}{Definition}

%\newtheorem{prop}[theo]{Proposition}

%\newtheorem{lem}[theo]{Lemma}

%\newtheorem{Cor}[theo]{Corollary}

%\newtheorem{remark}[theo]{Remark}

%\newcounter{pb}

%\newtheorem{problem}[pb]{Problem}

%\newenvironment{proof}{\noindent{\bfseries Proof :}}{\hbox{}\hfill$\Box$}

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

%% Definition of new colors

%\newrgbcolor{LemonChiffon}{1. 0.98 0.8}

%

%\newrgbcolor{LightBlue}{0.68 0.85 0.9}

%\newrgbcolor{Dgreen}{0  0.6 0.4}

%%\newrgbcolor{DBlue}{0  0 0.5}

%\newrgbcolor{DBlue}{0  0 0.6}

%\newrgbcolor{Dblue}{0  0 0.6}

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

%%% MORE Color definitions

%\newrgbcolor{DarkGray}{.284 .210 .410}

%\newrgbcolor{Violet}{.2 .2  .9}

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

\mode<presentation>

{

  \usetheme{Warsaw}

  % or ...

  \setbeamercovered{transparent}

  % or whatever (possibly just delete it)

}

\title{Towards an Unbounded Implicit Arithmetic for\\

the Polynomial Hierarchy

}

\author{Patrick Baillot and Anupam Das}

\institute{CNRS / ENS Lyon}

\begin{document}

\maketitle

\begin{frame}

  \frametitle{Introduction}

 2 cousin approaches to logical characterization of complexity classes:

\bigskip

 \begin{tabular}{l|l}

 \BA{Bounded arithmetic (86 -- )} & \ICC{Implicit computational complexity  (91 --)}\\

      & \ICC{(ICC)}\\

 \hline

 &\\

 & function algebras\\

 & types/proofs-as-programs\\

 & arithmetics / logics\\

 & \\

 large variety of & resource-free characterizations of\\

 complexity classes & complexity classes (e.g. ramification)\\

 &\\

 corresp. with & extensions to programming languages\\

 \textit{proof-complexity} &

 \end{tabular}

  \end{frame}

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

\begin{frame}

  \frametitle{Introduction}

$$  \mbox{"\textit{$f$ is provably total in system} XXX"} \Leftrightarrow \quad f \in \mbox{ complexity class YYY }$$

\bigskip

 \begin{tabular}{l|l}

 \BA{Bounded arithmetic}  \qquad \qquad & \ICC{Implicit computational complexity}\\

 \hline

 &\\

  Buss ($S_1$): & Leivant (intrinsic theories): \\

  $\forall x, {\BA{\exists y \leq t}} . \; A_f(x,y)$ & $\forall x. N_1(x) \rightarrow N_0(f(x))$\\

  &\\

  FP, FPH & FP

  \end{tabular}

  \end{frame}

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

\begin{frame}

  \frametitle{{A current limitation of ICC logics}}

 \begin{itemize}

\item fewer complexity classes characterized by {\ICC{ICC logics}} than by {\BA{bounded arithmetic}}

\item in particular, {\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}

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