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

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

 The following property follows from \cite{BellantoniThesis, Bellantoni95}]