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

Examples include bounded arithmetic \cite{Buss86book} \cite{Krajicek:1996:BAP:225488} \cite{Cook:2010:LFP:1734064}, applicative theories \cite{Cantini02} \cite{KahOit:13:ph-levels}, intrinsic and ramified theories \cite{Leivant94:intrinsic-theories} \cite{BelHof:02}, fragments of linear logic \cite{GirardSS92:bounded-ll} \cite{Girard94:lll} \cite{Lafont04} \cite{Baillot15} and fragments of intuitionistic logic \cite{Leivant94:found-delin-ptime}.

To some extent there is a distinction between various notions of `representability', namely between logics that \emph{type} terms computing functions of a given complexity class, and theories that prove the \emph{totality} or \emph{convergence} of programs computing functions in a given complexity class.

 Bounded arithmetic is a deep and well-established field, and one of its advantages is its great versatility, allowing a characterization of a wide range of complexity classes, such as $\ptime$, the polynomial hierarchy $\ph$, $\pspace$, $\mathbf{NC}^i$ etc. 

 %It is also closely related to \textit{proof complexity}, the research field investigating the size of propositional proofs in various proof systems. Finally it is also employed for the research direction of \textit{bounded reverse mathematics}. 

 Systems in implicit complexity typically imposes constraints on the comprehension scheme, the primitive recursion scheme or the structural rules of proof systems (namely \emph{contraction}). 

% But it seems to us that first-order quantification has not yet been investigated as much as it deserves. We believe that this is one reason of the modest achievements of implicit complexity concerning non-deterministic classes.

\section{Preliminaries}

\label{sect:prelims}

%\anupam{Should recall polymax bounded functions and the polychecking lemma, e.g.\ from Bellantoni's FPH paper or thesis. Quite important, even if proof not given.}

	\begin{itemize}

	\item The boolean predicates $\notfn (;x)$,  $\andfn(;x,y)$, $\orfn(;x,y)$, $\equivfn(;x,y)$ can all be defined on safe arguments, simply by computing by case distinction using the conditional function.

	%\item $\bit(l;x)$ returns the $\mode l$th bit of $x$.

	For that let us first define the function $\shorten(l;x)$ which returns the $|x|- |l|$ prefix of $x$, as follows:

	\begin{eqnarray*}

	\shorten(\epsilon;x) &=&x\\

	\end{eqnarray*}

	Then we define $\bit(l;x)$  as follows:

	$$\bit(l;x)=C(;\shorten(pl;x),\epsilon,0,1).$$ 

%\nb{Remember polymax bounded checking lemma! Quite important. Also need to bear this in mind when adding functions.}

\begin{definition}[$\mubc$ and $\mubc^i$ programs]

The algebra $\mubc$ is generated from $\bc$ by the following additional operation:

\begin{enumerate}

			\setcounter{enumi}{7}

	$$f(\vec u; \vec x):= \begin{cases}

	s_1 \mu y.(h(\vec u; \vec x, y)\mod 2 = 0)& \mbox{ if  there exists such a $y$,} \\

	0  & \mbox{ otherwise,}

where $\mu y.(h(\vec u; \vec x , y)\mod 2 = 0)$ is the least $y$ such that the equality holds.

%We will denote this function $f$ as $\mu y^{+1} . h(\vec u ; \vec x , y) =_2 0$.

 \end{definition}

 A polynomial $q$ satisfying this condition is called a \textit{threshold} for $f$.

 \end{definition}

 One then has:

 	\label{lem:bounded-minimisation}

If  $f(\vec u; \vec x,y)$ is a polynomial checking function on $\vec u$ and $q$ is a threshold, then for any $\vec u$ and $\vec x$ we have:

$$ (\exists y.   f(\vec u; \vec x,y)\mbox{ mod } 2=0) \Rightarrow (\exists y.  (\size{y}\leq q(\size{\vec{x}})+2) \mbox{ and } f(\vec u; \vec x,y) \mbox{ mod } 2=0) .$$

 	\label{lem:polychecking}

 Let $\Phi$ be a class of polymax bounded polynomial checking functions. If $f(\vec u; \vec x)$ is in $\mubc(\Phi)$, then $f$ is  a polymax bounded function  polynomial checking function on $\vec u$.

 \end{lemma}

 \begin{proposition}

  If $\Phi$ is a class of polymax bounded polynomial checking functions, then  $\mubc(\Phi)$ satisfies the properties of Thm \ref{thm:mubc}.

 \end{proposition}

The property is easily verified for the class of initial functions of  $\mubci{i-1}$: constant, projections, (binary) successors, predecessor, conditional, as already shown in Sect. \ref{sect:graphsbasicfunctions}. Now let us examine the three constructions: predicative minimisation, predicative (safe) recursion and composition. 

\paragraph*{Predicative minimisation}

By definition $g$ is in $\mubci{i-2}$, and so by the inductive hypothesis there is a $\Sigma^{\safe}_{i-1}$ formula $A_g (\vec u , \vec x , x , y)$ computing the graph of $g$ such that,

\[

\arith^i \proves \forall \vec u^\normal . \forall \vec x^\safe , x^\safe . \exists ! y^\safe . A_g(\vec u , \vec x , x , y)