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

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.

But a perhaps more important distinction is whether the constraints on the logic or theory are

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

  Another benefit is that implicit complexity systems can sometimes be extended into techniques for statically controlling the complexity of programs, e.g. in functional or imperative languages (e.g. \cite{Hofmann00,Hofmann03}, \cite{Marion11}).  However the variety of complexity classes that have been characterized in this implicit way is not as large as for bounded arithmetic. In particular implicit complexity has not managed to characterize non-deterministic classes, such as $\mathbf{NP}$ or $\ph$, in a purely logical way.\footnote{Actually some characterizations of such classes do exist, but they either take the form of a function algebra \cite{bellantoni1995fph} or of a type system extended with a non-logical feature \cite{GaboardiMarionRonchi12}.} 

% 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.

%  

  In the present work we aim to bridge the gap to bounded arithmetic by constructing `implicit' theories that characterise the functional polynomial hierarchy $\fph$ and its levels. We consider a base theory similar to that of bounded arithmetic, but we allow induction on \emph{unbounded} formulae, i.e.\ without any explicit bounds. 

%  Our methodology will be the following one: 

Naturally another constraint is in order, and for this we will use the concept of \textit{ramification} that is common in implicit complexity \cite{Leivant95,BellantoniCook92}.

%, adapt it in the setting of first-order arithmetic, and then explore some properties relative to quantification. First 

In a nutshell, recursion is permitted on normal arguments, but recursive calls can only appear in safe positions. Basic operations, such as conditionals and Boolean predicates, can be performed on safe arguments. 

Functions defined in this way correspond to polynomial time functions \cite{BellantoniCook92}. 

  %The key step we make is to focus our attention on \textit{safe quantifiers} that is to say quantifiers on safe variables.    

  These safe quantifiers play a r\^ole analogous to bounded quantifiers in bounded arithmetic. In particular we will consider a hierarchy $\Sigma_i^{\safe}$ of formulas, according to the number of alternations of safe quantifiers, to define a hierarchy of theories $\arith^i$ allowing induction on $\Sigma^\safe_i$ formulae. 

  We show that such a theory proves the totality of precisely the $\fph_i$ functions, relying on a recursion-theoretic characterisation of $\fph$ due to Bellantoni \cite{bellantoni1995fph} to both extract programs and prove completeness of the theory with respect to $\fph_i$.

%   Our approach in this paper is to use the formula-specification point of view, because it is convenient for the polynomial hierarchy. 

   The arithmetic of \cite{KahOit:13:ph-levels} characterizes $\fph$, but it is not implicit, relying on axioms defining bounded schemes.

%   Some other works are closer to our methodology in the sense that they are implicit arithmetics and rely on a notion of ramification, but they characterize other complexity classes. 

   The paper \cite{BelHof:02} also provides a characterization of $\fptime$, with two differences: on the one hand induction is on arbitrarily quantified formulas, and on the other hand the underlying logic is not classical logic but a variant of linear logic, with a modality for normal arguments. Our paper \cite{BaillotDas16} proves a similar result, but with a different method.

   The lack of contraction is crucial here to stop the theory from exhausting higher complexity classes. 

  \medskip

  \noindent

  \textbf{Outline.} The rest of this paper proceeds as follows. We first give some background on function algebras for $\fptime$ and $\fph$ respectively in Sect.~\ref{sect:prelims}. 

  %Then we describe an encoding of sequences which will be instrumental in the proof of our result. 

  More detailed proofs can be found in the technical report \cite{BaiDas17:fph-techreport}.