= Kleene normal form theorem
{c}
{title2=$f(\mathbf x)=U(\mu s\,[C(\mathbf x,s)=0])$}
For every <partial computable function> $f(\mathbf x)$, there are total <primitive recursive functions> $C,U$ such that
$$
f(\mathbf x)=U(\mu s\,[C(\mathbf x,s)=0]).
$$
Here $C$ is zero exactly on codes of valid halting computation histories for the chosen program and input, and $U$ extracts the final output. Coding finite configurations and finite histories makes checking every local step a bounded primitive recursive operation. If a computation halts, some history code passes and every passing code has the same output; if it does not halt, none passes. This is the usual normal-form version with the program index fixed; a universal predicate can also retain that index as an input.
Back to article page
