
\section{Preliminaries}
\label{sect:prelims}
We introduce the polynomial hierarchy and its basic properties, then Bellantoni's characterisation of it based on safe recursion and minimisation \cite{bellantoni1995fph}.

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

\subsection{Polynomial hierarchy}
%(include closure properties)

\begin{definition}
Given $i\geq 0$, a  language $L$ belongs to the class $\sigp{i}$ if there exists a polynomial time predicate $A$ and a polynomial $q$ such that:
$$ x \in L \Leftrightarrow \exists y_1 \in \{0,1\}^{q(\size{x})}\forall y_2 \in \{0,1\}^{q(\size{x})}\dots Q_iy_i\in \{0,1\}^{q(\size{x})}\ A(x,y_1,\dots,y_i)=1$$
where $Q_i=\forall$ (resp. $Q_i=\exists$) if $i$ is even (resp. odd).

The class $\pip{i}$ is defined similarly but with first quantifier $\forall$ instead of $\exists$. 
\end{definition}
In particular: $\sigp{0}=\pip{0}=\ptime$, $\sigp{1}=\np$, $\pip{1}=\conp$. Note that for any $i$ we have $\pip{i}=\mathbf{co}\sigp{i}$ and $\sigp{i}\subseteq \pip{i+1}$,  $\pip{i}\subseteq \sigp{i+1}$.

The polynomial hierarchy is defined as $\ph:=\cup_i \sigp{i}$, and we also have $\ph=\cup_i \pip{i}$.

Given a language $L$ we denote as $\fptime(L)$ the class of functions computable by a deterministic
polynomial time Turing machine with oracle $L$.

We now define the following function classes:
\[
\begin{array}{lcl}
 \fphi{i+1} &:= & \fptime(\sigp{i}),\\
 \fph &:=& \cup_i  \fphi{i}. 
\end{array}
\]
Notice that $ \fphi{i+1} =  \fptime(\pip{i})=  \fptime(\sigp{i}\cup \pip{i})$.

\subsection{Bellantoni-Cook characterisation of $\fptime$ using predicative recursion}
%(perhaps compare with Cobham's using limited recursion)
%
%\anupam{copied below from last year's paper}

We recall the Bellantoni-Cook  algebra $\bc$ of functions defined by \emph{safe} (or \emph{predicative}) recursion on notation \cite{BellantoniCook92}. 
These will be employed for proving both the soundness and completeness results later on. 

We consider functions $f$ over the domain $\Nat$ with sorted arguments $(\vec u ; \vec x)$, where the inputs $\vec u$ are called \textit{normal} and $\vec x$ are called \textit{safe}. 
%Each symbol is given with an arity $m$ and a number $n\leq m$ of normal arguments, and will be denoted as $f(\vec{u};\vec{x})$ where $\vec{u}$ (resp. $\vec{x}$) are the normal (resp. safe) arguments.
%We say that an expression is well-sorted if the arities of function symbols in it is respected.

%\patrick{Note that below I used the terminology 'BC programs', to distinguish them from 'functions' in the extensional sense, which I find clearer. But if you prefer to keep 'BC functions' it is all right for me.}
\begin{definition}
	[$\bc$ programs]
	$\bc$ contains the following initial functions:
	%	\paragraph{Initial functions}
	%	The initial functions are:
	
	\begin{enumerate}
		\item The constant functions $0 (\vec u ; \vec x) \dfn 0$, for each $|\vec u|$ and $| \vec x|$.
		\item The projection functions $\pi^{m,n}_k ( a_1 , \dots , a_m ; a_{m+1} , \dots, a_{m+n} )  := a_k$ for $1 \leq k \leq m+n$.
		\item The successor functions $\succ i ( ; x) \dfn 2x +i$ for $i = 0,1$.
		\item The predecessor function $\pred (; x) \dfn \hlf{x}$.
		\item The conditional function 
		\(
		\cond(;x,y,z)
		 \dfn 
		\begin{cases}
		y & x = 0\  \mathrm{mod}\  2 \\
		z & x = 1\  \mathrm{mod}\  2
		\end{cases}
		\)
	\end{enumerate}
	
	\medskip
	\noindent
$\bc$ is closed under the following operations:



	\begin{enumerate}
		\setcounter{enumi}{5}
		\item Predicative recursion on notation (PRN). If $g, h_0, h_1 $ are in BC then so is $f$ defined by,
		\[
		\begin{array}{rcll}
		f(0, \vec v ; \vec x) & := & g(\vec v ; \vec x) & \\
		f (\succ 0 u , \vec v ; \vec x ) & := & h_0 ( u , \vec v ; \vec x , f (u , \vec v ; \vec x) ) & \text{when $u \neq 0$} \\
		f (\succ 1 u , \vec v ; \vec x ) & := & h_1 ( u , \vec v ; \vec x , f (u , \vec v ; \vec x) ) & 
		\end{array}
		\]
		so long as the expressions are well-formed. % (i.e.\ in number/sort of arguments).
		\item Safe composition. If $g, \vec h, \vec h'$ are in BC then so is $f$ defined by,
		\[
		f (\vec u ; \vec x) \quad := \quad g ( \vec h(\vec u ; ) ; \vec h' (\vec u ; \vec x) )
		\]
		so long as the expression is well-formed.
	\end{enumerate}
\end{definition}
%Note that the  programs of this class can be defined by equational specifications in a natural way, and in the following we will thus silently identify a BC program with the corresponding equational specification.

We will refer to the expressions or terms built up from the rules above as `$\bc$-programs', although we consider $\bc$ itself to be an algebra of functions.
The main property of $\bc$ is:
\begin{theorem}[\cite{BellantoniCook92}]
	$\bc =\fptime$.
\end{theorem}	

%Actually this property remains true if one replaces the PRN scheme by the following more general simultaneous PRN scheme \cite{BellantoniThesis}:
%
%$(f^j)_{1\leq j\leq n}$ are defined by simultaneous PRN scheme  from $(g^j)_{1\leq j\leq n}$, $(h^j_0, h^j_1)_{1\leq j\leq n}$ if for $1\leq j\leq n$ we have:
%\[
%\begin{array}{rcl}
%f^j(0, \vec v ; \vec x) & := & g^j(\vec v ; \vec x) \\
%f^j(\succ i u , \vec v ; \vec x ) & := & h^j_i ( u , \vec v ; \vec x , \vec{f} (u , \vec v ; \vec x) )
%\end{array}
%\]
%for $i = 0,1$,  so long as the expressions are well-formed.

%\anupam{simultaneous recursion?}

%\anupam{also identity, hereditarily safe, expressions, etc.}

%\anupam{we implicitly associate a BC program with its equational specification} 

Consider a well-formed expression $t$ built from function symbols and variables. We say that a variable $y$ occurs \textit{hereditarily safe} in $t$ if, for every subexpression $f(\vec{r}; \vec{s})$ of $t$, the terms in $\vec{r}$ do not contain $y$.
For instance $y$ occurs hereditarily safe in $f(u;y,g(v;y))$, but not in $f(g(v;y);x)$.
\begin{proposition}
	[Properties of $\bc$ programs]
	\label{prop:bc-properties}
	We have the following properties:
	\begin{enumerate}
		\item The identity function is in $\bc$.
		\item Let $t$ be a well-formed expression built from $\bc$ programs and variables, denote its free variables as $\{u_1,\dots, u_n,x_1,\dots, x_k\}$, and assume for each $1\leq i\leq k$, $x_i$ is hereditarily safe in $t$. Then the function $f(u_1,\dots, u_n; x_1,\dots, x_k):=t$ is in $\bc$.
		\item If $f$ is a $\bc$ program, then the function $g(\vec{u},v;\vec{x})$ defined as $f(\vec{u};v,\vec{x})$
		is also a $\bc $ program.
	\end{enumerate}
	
	%\begin{proposition}
	%[Properties of BC programs]
	%\label{prop:bc-properties}
	%We have the following properties:
	%\begin{enumerate}
	%\item Hereditarily safe expressions over BC programs are BC definable.
	%\item Can pass safe input to normal input.
	%\end{enumerate}
\end{proposition}

%\nb{TODO: extend with $\mu$s.}

%\anupam{Should add $+(;x,y)$ as a basic function (check satisfies polychecking lemma!), since otherwise not definable with safe input. Then define unary successor $\succ{} (;x)$ as $+(;x,\succ 1 0)$. }

\begin{example}
	[Some simple functions]
	\label{ex:simple-bc-fns}
%	\todo{Boolean predicates $\notfn, \andfn, \orfn, \equivfn$ .}
%	\todo{$\bit$}
Observe that:
	\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$.
	\item We can define the function $\bit(l;x)$ which returns the $|l|$th least significant bit of $x$. For instance $\bit(11;1011)=0$.
	
	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\\
	\shorten(\succ{i}l;x) &=&p(;\shorten(l;x))
	\end{eqnarray*}
	Then we define $\bit(l;x)$  as follows:
	$$\bit(l;x)=C(;\shorten(pl;x),\epsilon,0,1).$$ 
	\end{itemize}
	\end{example}


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

\subsection{Bellantoni's characterisation of $\fphi{i}$ using predicative minimisation}

Now, in order to characterize $\fph$ and its subclasses $\fphi{i}$ we consider Bellantoni's function algebra $\mubc$, extending $\bc$ by predicative minimisation: 
\begin{definition}[$\mubc$ and $\mubc^i$ programs]
The algebra $\mubc$ is generated from $\bc$ by the following additional operation:

\begin{enumerate}
			\setcounter{enumi}{7}
	\item Predicative minimisation. If $h$ is in $\mubc$, then so is $f$ defined by
	$$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,}
	\end{cases}
	$$
\end{enumerate}
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$.

 For each $i\geq 0$, $\mubc^i$ is the set of $\mubc$ functions obtained by at most $i$ applications of predicative minimisation.\footnote{This is the number of nestings of $\mu$ in a $\mubc$ program.} So $\mubc^0=BC$ and $\mubc =\cup_i \mubc^i$.

 \end{definition}
 


 \begin{theorem}[\cite{BellantoniThesis, Bellantoni95}]\label{thm:mubc}
$\mubc =\fph$. Furthermore, for $i\geq 1$, $\mubc^{i-1} = \fphi{i}$.
 \end{theorem}


\medskip 
\noindent
\textbf{Some computational properties of $\mubc$ programs.}
  	We will need some bounds for $\mubc$ functions that we use later on;
  	all of this material is from \cite{bellantoni1995fph}.
  	
 \begin{definition}
  A function $f(\vec u; \vec x)$ is \textit{polymax bounded} if there exists a polynomial $q$ such that,
  for any $\vec u$ and $\vec x$ one has:

%$\size{u}$
  $$ \size{f(\vec u; \vec x)} \leq q(\size{u_1} , \dots , \size{u_k}) + \max_j \size{x_j}.$$
 \end{definition}
  
 We define the function $\mode$ by $u\mode x:= u \mod 2^{\size{x}}$. Note that this means that as a binary string $u\mode x$ is the suffix of $u$ of length $\size{x}$.
 \begin{definition}
 A function $f(\vec u; \vec x)$ is a \textit{polynomial checking function} on $\vec u$ if there exists a polynomial $q$
 such that, for any $\vec u$, $\vec x$, $y$ and $z$ such that $\size{y} \geq q(\size{\vec u})+ \size{z}$ we have:
 $$ f(\vec u; \vec x) \mode z = f(\vec u; \vec x \mode y)\mode z.$$
 A polynomial $q$ satisfying this condition is called a \textit{threshold} for $f$.
 \end{definition}
 One then has:
 \begin{lemma}[Bounded minimisation, \cite{BellantoniThesis}]
 	\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) .$$
 \end{lemma}
 
 Finally we can state an important lemma about $\mubc$.
  If $\Phi$ is a class of functions, we denote by $\mubc(\Phi)$ the class obtained as $\mubc$ but adding $\Phi$ to the set of initial functions.
 \begin{lemma}[Polychecking Lemma, \cite{BellantoniThesis}]
 	\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}
 The following property follows from \cite{BellantoniThesis, Bellantoni95}:
 \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}
 
 \subsection{Some properties and extensions of $\bc$ and $\mubc$}\label{sect:somepropertiesofmubc}
 
We will state some results here that we rely on in the later sections.
 
  Consider the addition function $+$ with two safe arguments, so denoted as $+(;x,y)$. It is clear that if $+(;x,y)=z$, then we have $|z| \leq \max(|x|,|y|)+1$, so $+$ is a polymax bounded function. Moreover for any $n$, the $n$th least significant bits of $z$ only depend on the $n$th least significant bits  of $x$ and $y$, so $+(;x,y)$ is a polynomial checking function (on no normal argument), with threshold $q(x,y)=0$.
  
  Thus, we will freely add $+(;x,y)$ to the $\mubc $ framework and define unary successor $\succ{} (;x) \dfn +(;x, \succ 1 0)$.
%  In the following we will consider $\mubc(\Phi)$ with $\Phi$ containing the function $+(;x,y)$, but write it simply as $\mubc$. Note that addition could be defined in $\bc$ (hence in $\mubc$), but not with two safe arguments because the definition would use safe recursion. We will also use the unary successor $\succ{} (;x)$, which is defined thanks to addition as  as $\succ{} (;x)=+(;x,\succ 1 0)$.
%  
In the same way, although for more simple reasons, we may add the functions $\#$ and $|\cdot|$ that we introduce later in Sect.~\ref{sect:arithmetic} to $\mubc$ containing only normal arguments since they are polynomial-time computable.
  
  
  One important closure property we will need for $\mubc $ functions, namely to define `witness functions' later on, is the following:
  \begin{lemma}
  	[Sharply bounded lemma]
  	\label{lem:sharply-bounded-recursion}
  	Let $f_A$ be the characteristic function of a predicate $A(u , \vec u ; \vec x)$.
  	Then the characteristic functions of $\forall u \leq |v| . A(u,\vec u ; \vec x)$ and $\exists u \leq |v| . A(u , \vec u ; \vec x)$ are in $\bc(f_A)$.
  \end{lemma}
  \begin{proof}
  	For the $\forall$ case, we define the characteristic function $f(v , \vec u ; \vec x)$ by predicative recursion on $v$ as:
  	\[
  	\begin{array}{rcl}
  	f(0, \vec u ; \vec x) & \dfn & f_A (0 , \vec u ; \vec x) \\
  	f(\succ i v , \vec u ; \vec x) & \dfn & \cond ( ; f_A (|\succ i v|, \vec u ; \vec x) , 0 , f(v , \vec u ; \vec x) )
  	\end{array}
  	\]
  	The $\exists$ case is similar.
  \end{proof}
  
Finally, we will briefly outline some basic functions for (de)coding sequences. The functions we introduce here will in fact be representable in the theory $\arith^1$ that we introduce in the next section, which, along with proofs of their basic properties, will be important for the completeness result in Sect.~\ref{sect:completeness}.

  We assume the existence of a simple pairing function in $\bc$ for elements of fixed size: $\pair{k,l}{x}{y}$ identifies the pair $(x \mode k , y \mode l )$.
  An appropriate such function would `interleave' $x$ and $y$, adding delimiters as necessary.
  We assume that $|\pair{k,l}{x}{y}| = k+O(l)$ and $\pair{k,l}{x}{y}$ satisfies the polychecking lemma.
  %
  We will simply write $\pair{l}{x}{y}$ for $\pair{l,l}{x}{y}$.
  
  \begin{lemma}
  	[Coding sequences]
  	\label{lem:sequence-creation}
  	Given a function $f(u , \vec u ; \vec x)$ there is a $\bc(f)$ function $F(l, u , \vec u ; \vec x)
%  	$ such that:
%  	\[
%  	F(l,u,\vec u ; \vec x)
 % 	\quad = \quad
  =
  	\langle \cdots \langle f(0, \vec u ; \vec x) \mode l , f(1, \vec u ; \vec x) \mode l \rangle , \cdots , f(|u|, \vec u ; \vec x) \mode l \rangle
  %	\]
  $
  \end{lemma}
  \begin{proof}
  	We simply define $F$ by safe recursion from $f$:
  	\[
  	\begin{array}{rcl}
  	F(l,0, \vec u ; \vec x) & \dfn & \langle ; f(0) \mode l \rangle \\
  	F(l, \succ i u , \vec u ; \vec x ) & \dfn & \pair{p(u l) , l}{F(l, u , \vec u ; \vec x)}{f( |\succ i u| , \vec u ; \vec x )}
  	\end{array}
  	\]
  	where $p(u l)$ is a sufficiently large polynomial.
  \end{proof}
  
  \begin{lemma}
  	[Decoding sequences]
  	We can define $\beta(l,i;x)$ as $(i\text{th element of x}) \mode l$.	
  \end{lemma}
  \begin{proof}[Proof sketch]
  	First define $\beta (j,i;x)$ as $|j|$th bit of $|i|$th element of $x$, of the form $\bit(p(i,j) ; x)$ for some quasipolynomial $p$,\footnote{A quasipolynomial is just a polynomial that may contain $\smsh$.} then use similar idea to the proof above, concatenating the bits of the $i$th element by a recursion on $j$.
  \end{proof}
  
  %Notice that $\beta (l,i;x)$ satisfies the polychecking lemma.
  