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

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

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

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

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

 The class of functions representable by $\mubc$ programs is $\fph$, and for each $i$ the class representable by $\mubc^i$ 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}

% \begin{lemma}

% Let $\Phi$ be a class of polymax bounded functions. If $f$ is in $\mubc(\Phi)$

% \end{lemma}

\nb{polychecking lemma still to be added}