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

\section{Preliminaries}

We introduce the polynomial hierarchy and its basic properties, then the Bellantoni characterisation.

\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{eqnarray*}

 \fphi{i+1} &:= & \fptime(\sigp{i}),\\

 \fph &:=& \cup_i  \fphi{i}.

\end{eqnarray*}

One can then check that $ \fphi{i+1} =  \fptime(\pip{i})=  \fptime(\sigp{i}\cup \pip{i})$.

\subsection{Bellantoni's characterisation using predicative minimisation}

(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 completeness   (all polynomial time functions are provably convergent) and the soundness result (all provably total functions are polynomial time) of THEORY. We consider function symbols $f$ over the domain  $\Word$ 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 is the set of functions generated as follows:

	%	\paragraph{Initial functions}

	%	The initial functions are:

	\begin{enumerate}

		\item The constant functions $\epsilon^k$ which takes $k$ arguments and outputs $\epsilon \in \Word$.

		\item The projection functions $\pi^{m,n}_k ( x_1 , \dots , x_m ; x_{m+1} , \dots, x_{m+n} )  := x_k$ for $n,m \in \Word$ and $1 \leq k \leq m+n$.

		\item The successor functions $\succ i ( ; x) := xi$ for $i = 0,1$.

		\item The predecessor function $\pred (; x) := \begin{cases}

		\epsilon &  \mbox{ if }  x = \epsilon \\

		x' &  \mbox{ if }  x = x'i

		\end{cases}$.

		\item The conditional function

		\[

		%\begin{array}{rcl}

		%C (; \epsilon, y_\epsilon , y_0, y_1  ) & = & y_\epsilon \\

		%C(; x0 , y_\epsilon , y_0, y_1) & = & y_0 \\

		%C(; x1 , y_\epsilon , y_0, y_1) & = & y_1

		%\end{array}

		C (; \epsilon, y_\epsilon , y_0, y_1  ) := y_\epsilon

		\quad

		C(; x0 , y_\epsilon , y_0, y_1) := y_0

		\quad

		C(; x1 , y_\epsilon , y_0, y_1) := y_1

		\]

		%		$\cond (;x,y,z) := \begin{cases}

		%		y & \mbox{ if } x=x' 0 \\

		%		z & \text{otherwise}

		%		\end{cases}$.

	\end{enumerate}

	%	One considers the following closure schemes:

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

		f(0, \vec v ; \vec x) & := & g(\vec v ; \vec x) \\

		f (\succ i u , \vec v ; \vec x ) & := & h_i ( u , \vec v ; \vec x , f (u , \vec v ; \vec x) )

		\end{array}

		\]

		for $i = 0,1$,  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 implicitly identify a BC function with the equational specification it induces.

The main property of BC programs is:

\begin{theorem}[\cite{BellantoniCook92}]

	The class of functions representable by BC programs is $\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 functions 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 function, 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$}

	$\bit(l;x)$ returns the $\mode l$th bit of $x$.

	\end{example}

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

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

\begin{definition}[$\mubc$ and $\mubc^i$ programs]

We define:

\begin{itemize}

\item The class $\mubc$ is the set of functions defined as the BC functions, but with the following additional generation rule:

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

$

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

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.

\item For each $i\geq 0$, $\mubc^i$ is the set of $\mubc$ functions obtained by at most $i$ applications of predicative minimization. So $\mubc^0=BC$ and $\mubc =\cup_i \mubc^i$.

\end{itemize}

 \end{definition}

 One then obtains:

 \begin{theorem}[\cite{BellantoniThesis, Bellantoni95}]

 The class of functions representable by $\mubc$ programs is $\fph$, and for each $i\geq 1$ the class representable by $\mubc^{i-1}$ programs is $\fphi{i}$.

 \end{theorem}

 We will also need an intermediary lemma, also proved in \cite{BellantoniThesis}.

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

 \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 Minimization, \cite{BellantoniThesis}]

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$:

 \begin{lemma}[Polychecking Lemma, \cite{BellantoniThesis}]

 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}