# Definition:Minimization

## Definition

### Function

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

Let $n = \tuple {n_1, n_2, \ldots, n_k} \in \N^k$ be fixed.

Then the **minimization operation on $f$** is written as:

- $\map {\mu y} {\map f {n, y} = 0}$

and is specified as follows:

- $\map {\mu y} {\map f {n, y} = 0} = \begin{cases} \text{the smallest } y \in \N \text{ such that } \map f {n, y} = 0 & : \text{if there exists such a } y \\ \text{undefined} & : \text{otherwise} \end{cases}$

Note that if $f: \N^{k + 1} \to \N$ is a total function, and $g: \N^k \to \N$ is given by:

- $\map g n = \map {\mu y} {\map f {n, y} = 0}$

then, in general, $g$ will be a partial function.

This page has been identified as a candidate for refactoring of basic complexity.In particular: This transclusion is wrongUntil this has been finished, please leave
`{{Refactor}}` in the code.
Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Refactor}}` from the code. |

### Partial Function

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

Let $n = \tuple {n_1, n_2, \ldots, n_k} \in \N^k$ be fixed.

Then the **minimization operation on $f$** is written as:

- $\map {\mu y} {\map f {n, y} = 0}$

and is specified as follows:

- $\map {\mu y} {\map f {n, y} = 0} = \begin{cases} z & : \map f {n, z} = 0 \text { and } \map f {n, y} \text{ defined and } \forall y: 0 \le y < z: \map f {n, y} \ne 0 \\ \text{undefined} & : \text{otherwise} \end{cases}$

The partial function:

- $\map g n \approx \map {\mu y} {\map f {n, y} = 0}$

obtained in this way (see Partial Function Equality) is said to be obtained from $f$ **by minimization**.

## Warning

It is not enough for there to exist $z$ such that $\map f {n, z} = 0$.

We need to insist that $\map f {n, y}$ is actually defined for all $y$ less than $z$.

Otherwise, if we were to try and find $z$ by the recursive technique of trying all $z$ from $0$ up, we would never actually get up as far as $z$ because the undefined value of $f$ for some $y$ is getting in the way.

In the context of URM programs, this is significant, as an undefined output from a function is determined by a non-terminating program.

### Relation

Let $\map \RR {n_1, n_2, \ldots, n_k, y} $ be a $k + 1$-ary relation on $\N^{k + 1}$.

Let $n = \tuple {n_1, n_2, \ldots, n_k} \in \N^k$ be fixed.

Then the **minimization operation on $\RR$** is written as:

- $\mu y \map \RR {n, y}$

and is specified as follows:

- $\mu y \map \RR {n, y} = \begin{cases} \text{the smallest } y \in \N \text{ for which } \map \RR {n, y} \text{ holds} & : \text{if there exists such a } y \\ \text{undefined} & : \text{otherwise} \end{cases}$

We can consider the definition for a function to be a special case of this.

Compare the bounded minimization operation which is always a total function.