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

\section{Preliminaries}

\label{sect:prelims}

%\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{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$.

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

	\end{eqnarray*}

	Then we define $\bit(l;x)$  as follows:

	$$\bit(l;x)=C(;\shorten(pl;x),\epsilon,0,1).$$ 

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

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

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

\begin{enumerate}

			\setcounter{enumi}{7}

	$$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,}

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

 \end{definition}

 A polynomial $q$ satisfying this condition is called a \textit{threshold} for $f$.

 \end{definition}

 One then has:

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

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

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