\begin{definition}[Definition:Minimization/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.
Category:Definitions/Mathematical Logic
\end{definition}