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

\newtheorem{claim}[theorem]{Claim}

\institute{CNRS / ENS Lyon\\

DICE-FOPARA 2017 workshop, Uppsala}

% & function algebras\\

% & types/proofs-as-programs\\

arithmetic & arithmetics / logics\\

 correspondence with & extensions to programming languages\\

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

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

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

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

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

%\smallskip

\item BC function algebra (Bellantoni-Cook 92):

 $f({\red{\vec u}}^{\; {\red{N_1}}}{\textbf ;} \vec x^{\; N_0})$

 safe recursion scheme:

          logic for FP: Leivant 95, Cantini 02, Bellantoni-Hofmann 02 

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

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

 Various approaches at hand to specify a function $f$ in a logic:

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

terms of combinatory algebra computing $f$

 Ramified classical arithmetic (\RC):

\item BASIC theory: defining $\succ, +, \cdot, \smsh, |.|$ (as in Buss' $S_2$, but sorted)

% Write $Q$ for $\forall$ or $\exists$.

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

 \begin{claim}[Soundness]

 \end{claim}

  \begin{claim}[Completeness]

 \end{claim}

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

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