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

\documentclass[a4paper,UKenglish]{lipics-v2016}

%This is a template for producing LIPIcs articles.

%See lipics-manual.pdf for further information.

%for A4 paper format use option "a4paper", for US-letter use option "letterpaper"

%for british hyphenation rules use option "UKenglish", for american hyphenation rules use option "USenglish"

% for section-numbered lemmas etc., use "numberwithinsect"

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

% Author macros::begin %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\title{An implicit characterisation of the polynomial hierarchy in an unbounded arithmetic}

%\titlerunning{An implicit characterisation of the polynomial hierarchy} %optional, in case that the title is too long; the running title should fit into the top page column

%% Please provide for each author the \author and \affil macro, even when authors have the same affiliation, i.e. for each author there needs to be the  \author and \affil macros

\author[1]{Patrick Baillot}

\author[2]{Anupam Das}

\affil[1]{LIP, ENS Lyon\\

  \texttt{patrick.baillot@ens-lyon.fr}}

\affil[2]{LIP, ENS Lyon\\

  \texttt{anupam.das@ens-lyon.fr}}

\authorrunning{P. Baillot and A. Das} %mandatory. First: Use abbreviated first/middle names. Second (only in severe cases): Use first author plus 'et. al.'

\Copyright{Patrick Baillot and Anupam Das}%mandatory, please use full first names. LIPIcs license is "CC-BY";  http://creativecommons.org/licenses/by/3.0/

\subjclass{F.4.1 Mathematical Logic %-- please refer to \url{http://www.acm.org/about/class/ccs98-html}

	}% mandatory: Please choose ACM 1998 classifications from http://www.acm.org/about/class/ccs98-html . E.g., cite as "F.1.1 Models of Computation".

\keywords{Polynomial hierarchy,

	Implicit complexity,

	Proof theory,

	Bounded arithmetic,

	Witness extraction,

	Ramification.}% mandatory: Please provide 1-5 keywords

% Author macros::end %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%Editor-only macros:: begin (do not touch as author)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\EventEditors{John Q. Open and Joan R. Acces}

\EventNoEds{2}

\EventLongTitle{42nd Conference on Very Important Topics (CVIT 2016)}

\EventShortTitle{CVIT 2016}

\EventAcronym{CVIT}

\EventYear{2016}

\EventDate{December 24--27, 2016}

\EventLocation{Little Whinging, United Kingdom}

\EventLogo{}

\SeriesVolume{42}

\ArticleNo{23}

% Editor-only macros::end %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}

\maketitle

\begin{abstract}

We consider extensions of theories based on the Bellantoni-Cook function algebra for polynomial time functions ($\fptime$) 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 \emph{free-cut elimination} in the logic, making use of the \emph{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 $\fptime$ 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}

\input{intro}

\input{preliminaries}

%\input{sequence-coding}

\input{arithmetic}

\input{soundness}

\input{completeness}

%\input{further}

\input{conclusions}

%\subparagraph*{Acknowledgements.}

%

%I want to thank \dots

%%

%% Bibliography

%%

%% Either use bibtex (recommended),

\newpage

\bibliography{ph-biblio}

%% .. or use the thebibliography environment explicitely

\newpage

\appendix

\input{appendix-arithmetic}

%%\input{pv-theories}

%\input{appendix-sequent-calculus}

%\input{appendix-soundness}

\input{appendix-completeness}

\end{document}