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{Dummy classification -- 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{Dummy keyword -- please provide 1--5 keywords}% 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 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),

\bibliography{ph-biblio}

%% .. or use the thebibliography environment explicitely

\newpage

\appendix

\input{appendix-arithmetic}

\input{pv-theories}

\end{document}

\grid