# Bounded Minimization is Primitive Recursive

## Theorem

### Function

Let $f: \N^{k+1} \to \N$ be a primitive recursive function.

Then the function $g: \N^{k+1} \to \N$ defined as:

$g \left({n_1, n_2, \ldots, n_k, z}\right) = \mu y \le z \left({f \left({n_1, n_2, \ldots, n_k, y}\right) = 0}\right)$

where $\mu y \le z \left({f \left({n_1, n_2, \ldots, n_k, y}\right) = 0}\right)$ is the bounded minimization operation on $f$

is also primitive recursive.

### Relation

Let $\mathcal R$ be a primitive recursive $k+1$-ary relation on $\N^{k+1}$.

Then the function $g: \N^{k+1} \to \N$ defined as:

$g \left({n_1, n_2, \ldots, n_k, z}\right) = \mu y \le z \mathcal R \left({n_1, n_2, \ldots, n_k, y}\right)$

where $\mu y \le z \mathcal R \left({n_1, n_2, \ldots, n_k, y}\right)$ is the bounded minimization operation on $\mathcal R$

is also primitive recursive.

## Proof

### Proof for Function

We can define $g$ as follows:

$(1) \quad g \left({n_1, n_2, \ldots, n_k, 0}\right) = \begin{cases} 0 & : f \left({n_1, n_2, \ldots, n_k, 0}\right) = 0 \\ 1 & : \text{otherwise} \\ \end{cases}$
$(2) \quad g \left({n_1, n_2, \ldots, n_k, z + 1}\right) = \begin{cases} g \left({n_1, n_2, \ldots, n_k, z}\right) & : g \left({n_1, n_2, \ldots, n_k, z}\right) \le z \\ z + 1 & : g \left({n_1, n_2, \ldots, n_k, z}\right) = z + 1 \text{ and } f \left({n_1, n_2, \ldots, n_k, z + 1}\right) = 0 \\ z + 2 & : \text{otherwise} \\ \end{cases}$

The fact that $(1)$ is true is clear.

Hence by Definition by Cases is Primitive Recursive, the function defined in $(1)$ is primitive recursive.

Now we investigate $(2)$.

Note that if $g \left({n_1, n_2, \ldots, n_k, z}\right) \le z$ then the equation $f \left({n_1, n_2, \ldots, n_k, y}\right) = 0$ has a solution for some $y \le z$.

Then the smallest $y \le z$ which solves this equation is also the smallest value of $y \le z + 1$ which solves this equation.

So in this case, $g \left({n_1, n_2, \ldots, n_k, z + 1}\right) = g \left({n_1, n_2, \ldots, n_k, z}\right)$.

Otherwise there is no such $y \le z$ that solves the equation.

Then the value $g \left({n_1, n_2, \ldots, n_k, z + 1}\right)$ is $z + 1$ if $f \left({n_1, n_2, \ldots, n_k, z + 1}\right) = 0$.

But if $f \left({n_1, n_2, \ldots, n_k, z + 1}\right) \ne 0$ then $g \left({n_1, n_2, \ldots, n_k, z + 1}\right) = \left({z + 1}\right) + 1 = z + 2$.

Thus $g$ as defined in $(1)$ and $(2)$ are an appropriate definition of:

$g \left({n_1, n_2, \ldots, n_k, z}\right) = \mu y \le z \left({f \left({n_1, n_2, \ldots, n_k, y}\right) = 0}\right)$.

Now to show that the function defined in $(2)$ is primitive recursive.

By the corollary to Definition by Cases is Primitive Recursive, the relations defining the cases are primitive recursive.

Then we have that $g \left({n_1, n_2, \ldots, n_k, z}\right)$, $z + 1$ and $z + 2$ are expressed in terms of:

So all these functions are primitive recursive.

Hence by Definition by Cases is Primitive Recursive, the function defined in $(2)$ is primitive recursive.

Therefore $g$ is defined by primitive recursion from functions which we have proved to be primitive recursive.

The result follows.

$\blacksquare$

### Proof for Relation

We can mimic the proof for the function.

Or we can do it this way.

From the definition of the characteristic function for $\mathcal R$, we can express $\mu y \le z \mathcal R \left({n_1, n_2, \ldots, n_k, y}\right)$ as:

$\mu y \le z \left({\chi_\mathcal R \left({n_1, n_2, \ldots, n_k, y}\right) = 1}\right)$.

Now we turn $\chi_\mathcal R \left({n_1, n_2, \ldots, n_k, y}\right) = 1$ into something of the form $f \left({n_1, n_2, \ldots, n_k, y}\right) = 0$.

We can use signum-bar function:

$\chi_\mathcal R \left({n_1, n_2, \ldots, n_k, y}\right) = 1 \iff \overline{\operatorname{sgn}} \left({\chi_\mathcal R \left({n_1, n_2, \ldots, n_k, y}\right)}\right) = 0$

Now we define $f \left({n_1, n_2, \ldots, n_k, n_{k+1}}\right) = \overline{\operatorname{sgn}} \left({\chi_\mathcal R \left({n_1, n_2, \ldots, n_k, n_{k+1}}\right)}\right)$.

This is primitive recursive because it is defined by substitution from:

Hence from Definition by Cases is Primitive Recursive, $g$ is primitive recursive.

$\blacksquare$