Unbounded Minimization

Definition

Unbounded minimization is the operation that, given a function $g:A\to \mathbb{N}\to \mathbb{N}$, returns the least $y\in \mathbb{N}$ such that $g(x,y)=0$, when such a least value exists. It is written $\mu y[g(x,y)=0]$.

Equivalently, one may define

$$\mu g(x)=\min \left\{y\in \mathbb{N}|g(x,y)=0\right\},$$

with the understanding that the computation is undefined if no such $y$ exists.

Properties

Unbounded minimization need not preserve totality: even when $g$ is total, the function $\mu g$ may be partial.

Starting with basic functions and closing under composition, primitive recursion, and unbounded minimization, one obtains the class of partial computable functions, which is equivalent to the class computed by Turing machines.

Related Concepts

Partial Computable Function
Primitive recursion
Turing Machine