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

We consider extensions of theories based on the Bellantoni-Cook function algebra for polynomial time functions (FP) by induction principles without bounds on quantifiers. Instead, we limit quantification to 'safe' arguments and show that the provably total functions are just those of the functional polynomial hierarchy (FPH). Our witness extraction proof relies on free-cut elimination in the logic, making use of the witness function method, due to Buss, rather than realisability and Dialectica approaches more common in implicit complexity. Our results closely resemble analogous ones from bounded arithmetic, only for an unbounded setting, and the proof generalises those for previous approaches characterising FP via ramified theories. 

\patrick{Remove: We present further comparisons to the bounded arithmetic setting and give tiered arithmetic theories analogous to the Si2 and Vi hierarchies of bounded arithmetic.} 

\end{abstract}

%\begin{abstract}

%We consider extensions of equational theories based on the Bellantoni-Cook function algebra for FPTIME by induction principles without bounds on quantifiers. Instead, we limit quantification to 'safe' variables and show that the provably total functions are just those of FPH. This closely resembles analogous results from bounded arithmetic, only for an unbounded setting, and the proof generalises those for previous approaches characterising FPTIME via the Bellantoni-Cook framework. We present further comparisons to the bounded arithmetic setting and give two-sorted arithmetic theories analogous to the Si2 and Vi hierarchies of bounded arithmetic. 

% \end{abstract}