Bounded Minimization is Primitive Recursive

From ProofWiki
Jump to navigation Jump to search

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:

$\map g {n_1, n_2, \ldots, n_k, z} = \mu y \le \map z {\map f {n_1, n_2, \ldots, n_k, y} = 0}$

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

is also primitive recursive.


Relation

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


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

$\map g {n_1, n_2, \ldots, n_k, z} = \mu y \le z \RR \tuple {n_1, n_2, \ldots, n_k, y}$

where $\mu y \le z \RR \tuple {n_1, n_2, \ldots, n_k, y}$ is the bounded minimization operation on $\RR$

is also primitive recursive.


Proof

Proof for Function

We can define $g$ as follows:

$(1) \quad \map g {n_1, n_2, \ldots, n_k, 0} = \begin{cases} 0 & : \map f {n_1, n_2, \ldots, n_k, 0} = 0 \\ 1 & : \text{otherwise} \\ \end{cases}$
$(2) \quad \map g {n_1, n_2, \ldots, n_k, z + 1} = \begin{cases} \map g {n_1, n_2, \ldots, n_k, z} & : \map g {n_1, n_2, \ldots, n_k, z} \le z \\ z + 1 & : \map g {n_1, n_2, \ldots, n_k, z} = z + 1 \text{ and } \map f {n_1, n_2, \ldots, n_k, z + 1} = 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 $\map g {n_1, n_2, \ldots, n_k, z} \le z$ then the equation $\map f {n_1, n_2, \ldots, n_k, y} = 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, $\map g {n_1, n_2, \ldots, n_k, z + 1} = \map g {n_1, n_2, \ldots, n_k, z}$.

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

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

But if $\map f {n_1, n_2, \ldots, n_k, z + 1} \ne 0$ then $\map g {n_1, n_2, \ldots, n_k, z + 1} = \paren {z + 1} + 1 = z + 2$.

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

$\map g {n_1, n_2, \ldots, n_k, z} = \mu y \le \map z {\map f {n_1, n_2, \ldots, n_k, y} = 0}$


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 $\map g {n_1, n_2, \ldots, n_k, z}$, $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 $\RR$, we can express $\mu y \le z \RR \tuple {n_1, n_2, \ldots, n_k, y}$ as:

$\mu y \le \map z {\map {\chi_\RR} {n_1, n_2, \ldots, n_k, y} = 1}$

Now we turn $\map {\chi_\RR} {n_1, n_2, \ldots, n_k, y} = 1$ into something of the form $\map f {n_1, n_2, \ldots, n_k, y} = 0$.

We can use signum-bar function:

$\map {\chi_\RR} {n_1, n_2, \ldots, n_k, y} = 1 \iff \map {\overline \sgn} {\map {\chi_\RR} {n_1, n_2, \ldots, n_k, y} } = 0$

Now we define $\map f {n_1, n_2, \ldots, n_k, n_{k + 1} } = \map {\overline \sgn} {\map {\chi_\RR} {n_1, n_2, \ldots, n_k, n_{k + 1} } }$.

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

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

$\blacksquare$