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\\

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}

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