Definition:Minimization/Partial Function

From ProofWiki
Jump to navigation Jump to search


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

Let $n = \left({n_1, n_2, \ldots, n_k}\right) \in \N^k$ be fixed.

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

$\mu y \left({f \left({n, y}\right) = 0}\right)$

and is specified as follows:

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

The partial function:

$g \left({n}\right) \approx \mu y \left({f \left({n, y}\right) = 0}\right)$

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


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

We need to insist that $f \left({n, y}\right)$ 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.