Kleene's Normal Form Theorem

From ProofWiki
Jump to navigation Jump to search


Theorem

For each integer $k \ge 1$, there exists:

such that a partial function $f: \N^k \to \N$ is recursive iff, for some $e \in \N$ and all $\left({n_1, n_2, \ldots, n_k}\right) \in \N^k$:

$f \left({n_1, n_2, \ldots, n_k}\right) \approx U \left({\mu z \ T_k \left({e, n_1, n_2, \ldots, n_k, z}\right)}\right)$


Proof

See the proof of URM Computable Function is Recursive for an explanation of the symbols used here.


Necessary Condition

Suppose $e = \gamma \left({P}\right)$ codes a URM program $P$ which computes $f$.

Suppose the computation using $P$ with input $\left({n_1, n_2, \ldots, n_k}\right)$ halts at stage $t_0$ with output $q$.

Let $t > t_0$, that is, we "wait till after $P$ has finished".

Then $f \left({n_1, n_2, \ldots, n_k}\right) = q$.

Since $P$ has halted at stage $t_0$:

$\left({S_k \left({e, n_1, n_2, \ldots, n_k, t}\right)}\right)_1 > \operatorname{len} \left({e}\right)$

where:

  • $S_k \left({e, n_1, n_2, \ldots, n_k, t}\right)$ is the state code at stage $t$ of the computation of $P$ with input $\left({n_1, n_2, \ldots, n_k}\right)$
  • $\operatorname{len} \left({e}\right)$ is the length of $e$
  • the number $\left({S_k \left({e, n_1, n_2, \ldots, n_k, t}\right)}\right)_1$ is the value of the instruction pointer to the instruction about to be carried out at stage $t$
  • $\left({z}\right)_j$ is the prime exponent function.


Since the output is $q$:

$\left({S_k \left({e, n_1, n_2, \ldots, n_k, t}\right)}\right)_2 = q$

Let us put $z_0 = 2^q 3^{t_0}$.

Then:

$\left({z_0}\right)_2 = t_0$ and $\left({z_0}\right)_1 = q$

Thus:

$\left({S_k \left({e, n_1, n_2, \ldots, n_k, \left({z_0}\right)_2}\right)}\right)_1 > \operatorname{len} \left({e}\right)$

and

$\left({z_0}\right)_1 = \left({S_k \left({e, n_1, n_2, \ldots, n_k, \left({z}\right)_2}\right)}\right)_2$

Now $z_0$ is the smallest integer with these properties, because $\left({z_0}\right)_2 = t_0$ is the stage at which $P$ halts.

Thus we have:

$f \left({n_1, n_2, \ldots, n_k}\right) = q = \left({z_0}\right)_1$.


Now we let $T_k \left({e, n_1, n_2, \ldots, n_k, z}\right)$ be the relation defined as:

\(\ds T_k \left({e, n_1, n_2, \ldots, n_k, z}\right)\) \(\iff\) \(\ds \left({S_k \left({e, n_1, n_2, \ldots, n_k, t}\right)}\right)_1 > \operatorname{len} \left({e}\right)\)
\(\ds \) \(\text { and }\) \(\ds \left({z}\right)_1 = \left({S_k \left({e, n_1, n_2, \ldots, n_k, \left({z}\right)_2}\right)}\right)_2\)

Then $T_k$ is a primitive recursive $k+1$-ary relation.

Also, we can take $U: \N \to \N$ to be the primitive recursive function given by $U \left({z}\right) = \left({z}\right)_1$.

$\Box$


Sufficient Condition

Now let $f$ be a recursive function.

Then by Recursive Function is URM Computable, there exists some URM program which computes $f$.

Let $P$ be the URM program with the smallest code number that computes $f$.

Let $e = \gamma \left({P}\right)$ be the code number of $P$.


Suppose $f \left({n_1, n_2, \ldots, n_k}\right)$ is defined.

Then from the above, we deduce that $\mu z \ T_k \left({e, n_1, n_2, \ldots, n_k, z}\right)$ is defined.

Let $z_0 = \mu z \ T_k \left({e, n_1, n_2, \ldots, n_k, z}\right)$.

Then $\left({z_0}\right)_1 = f \left({n_1, n_2, \ldots, n_k}\right)$.

That is, $U \left({z_0}\right) = f \left({n_1, n_2, \ldots, n_k}\right)$.

Hence $f \left({n_1, n_2, \ldots, n_k}\right) = U \left({\mu z \ T_k \left({e, n_1, n_2, \ldots, n_k, z}\right)}\right)$ as required.


On the other hand, suppose $f \left({n_1, n_2, \ldots, n_k}\right)$ is undefined.

Then the computation using $P$ with input $\left({n_1, n_2, \ldots, n_k}\right)$ does not halt.

So there is no $z$ such that $T_k \left({e, n_1, n_2, \ldots, n_k, z}\right)$.

So $U \left({\mu z \ T_k \left({e, n_1, n_2, \ldots, n_k, z}\right)}\right)$ is undefined.

Thus:

$f \left({n_1, n_2, \ldots, n_k}\right) \approx U \left({\mu z \ T_k \left({e, n_1, n_2, \ldots, n_k, z}\right)}\right)$

as defined in partial function equality.

$\blacksquare$


Source of Name

This entry was named for Stephen Cole Kleene.