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

We introduce the polynomial hierarchy and its basic properties, then Bellantoni's characterisation of it based on safe recursion and minimization \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.}

\[

\begin{array}{lcl}

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

	[$\bc$ programs]

	$\bc$ contains the following initial functions:

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

		\(

		\cond(;x,y,z)

		 \dfn 

		\begin{cases}

		y & x = 0\  \mathrm{mod}\  2 \\

		z & x = 1\  \mathrm{mod}\  2

		\end{cases}

		\)

	\medskip

	\noindent

$\bc$ is closed under the following operations:

		\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) ) & 

		so long as the expressions are well-formed. % (i.e.\ in number/sort of arguments).

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:

	$\bc =\fptime$.

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

	[Properties of $\bc$ programs]

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

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

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

Now, in order to characterize $\fph$ and its subclasses $\fphi{i}$ we consider Bellantoni's function algebra $\mubc$, extending $\bc$ by predicative minimization: 

The algebra $\mubc$ is generated from $\bc$ by the following additional operation:

\begin{enumerate}

			\setcounter{enumi}{7}

	\item Predicative minimization. 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 minimization.\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}

$\mubc =\fph$. Furthermore, for $i\geq 1$, $\mubc^{i-1} = \fphi{i}$.

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

 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.

 \subsection{Some properties and extensions of $\bc$ and $\mubc$}

 \anupam{done a pass up to here. Resuming at next section.}

  \anupam{also add $\#$ and $|\cdot|$, for simplicity.}

  \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 \prefix v . A(u,\vec u ; \vec x)$ and $\exists u \prefix v . A(u , \vec u ; \vec x)$ are in $\bc(f_A)$.

  \end{lemma}

  \begin{proof}

  	We give the $\forall$ case, the $\exists$ case being dual.

  	The characteristic function $f(v , \vec u ; \vec x)$ is defined 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}

  	\]

  \end{proof}

\medskip

\noindent

\textbf{Encoding of sequences.}

  Assume the existence of a simple pairing function for elements of fixed size: $\pair{k,l}{x}{y}$ denotes 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}

  	[Creating 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 f(0, \vec u ; \vec x) \mode l , f(1, \vec u ; \vec x) \mode l , \dots , 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{O(|u| l) , l}{F(l, u , \vec u ; \vec x)}{f( |\succ i u| , \vec u ; \vec x )}

  	\end{array}

  	\]

  	where the constants for $O(|u|l)$ are sufficiently large.

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

  	First define $\beta (j,i;x)$ as $j$th bit of $i$th element of $x$, then use similar idea to above, by a recursion on $j$.

  \end{proof}

  Notice that $\beta (l,i;x)$ satisfies the polychecking lemma.

  We define