[proofplan] We choose a standard register-machine model for partial computable functions and encode finite computation histories by natural numbers. The predicate $T_k$ says that a number $t$ codes a valid halting computation history for program $e$ on input $(x_1,\dots,x_k)$: the first configuration is the prescribed initial configuration, each next configuration follows by one instruction of program $e$, and the last configuration is halting. Because all checks inspect only bounded parts of the finite code $t$, they are primitive recursive. The output function $C$ extracts the output register from the final configuration, and minimising over $t$ selects a halting history exactly when the computation halts. [/proofplan] [step:Fix a primitive recursive coding of finite configurations and histories] Use a register-machine model with instructions of the following forms: increment register $i$ and go to label $q$, decrement register $i$ if nonzero and go to label $q_1$, otherwise go to label $q_0$, and halt. A program is a finite list of such instructions, encoded by a natural number $e \in \mathbb{N}$. Fix primitive recursive coding functions for finite tuples. Thus there are primitive recursive maps \begin{align*} \operatorname{len}: \mathbb{N} &\to \mathbb{N},\\ \operatorname{entry}: \mathbb{N} \times \mathbb{N} &\to \mathbb{N} \end{align*} such that, when $a$ codes a finite sequence, $\operatorname{len}(a)$ is its length and $\operatorname{entry}(a,i)$ is its $i$-th entry for $0 \leq i < \operatorname{len}(a)$. Outside this range, define $\operatorname{entry}(a,i)=0$. A machine configuration is a finite tuple consisting of a program label and finitely many register values. Let \begin{align*} \operatorname{label}: \mathbb{N} &\to \mathbb{N},\\ \operatorname{reg}: \mathbb{N} \times \mathbb{N} &\to \mathbb{N} \end{align*} be the primitive recursive decoding maps sending a configuration code $c$ to its current label and to the value of register $i$. A computation history is a finite sequence of configuration codes, so a number $t \in \mathbb{N}$ is read as such a sequence through $\operatorname{len}(t)$ and $\operatorname{entry}(t,j)$. [/step] [step:Express the one-step transition relation by a primitive recursive predicate] Define the predicate \begin{align*} \operatorname{Step}: \mathbb{N}^3 &\to \{0,1\} \end{align*} by declaring $\operatorname{Step}(e,c,d)=1$ exactly when $d$ is the configuration obtained from configuration $c$ by executing the instruction of program $e$ at label $\operatorname{label}(c)$. The instruction at a given label of the program coded by $e$ is obtained by bounded tuple decoding from $e$. Each instruction check is a finite combination of equalities, comparisons, register projections, and successor/predecessor operations. Therefore $\operatorname{Step}$ is primitive recursive. Likewise define \begin{align*} \operatorname{Halt}: \mathbb{N}^2 &\to \{0,1\} \end{align*} by $\operatorname{Halt}(e,c)=1$ exactly when the label of $c$ is a halting label for the program coded by $e$. This predicate is primitive recursive because it is again a bounded inspection of the code $e$ and the label component of $c$. [guided] We now isolate the only machine-dependent part of the argument. The predicate $\operatorname{Step}(e,c,d)$ asks whether one legal machine move takes the configuration coded by $c$ to the configuration coded by $d$ when the program code is $e$. This check is primitive recursive because the machine has only finitely many instruction types. If the decoded instruction says “increment register $i$ and go to label $q$,” then the check requires: \begin{align*} \operatorname{label}(d) &= q,\\ \operatorname{reg}(d,i) &= \operatorname{reg}(c,i)+1,\\ \operatorname{reg}(d,j) &= \operatorname{reg}(c,j) \quad \text{for each relevant } j \neq i. \end{align*} The phrase “relevant $j$” is bounded by the finite amount of register data appearing in the coded configurations and the program code, so the universal comparison over these $j$ is a bounded finite check. If the decoded instruction says “decrement register $i$ if nonzero, otherwise branch,” the check splits into two primitive recursive cases: \begin{align*} \operatorname{reg}(c,i) &> 0 \end{align*} with register $i$ decreased by $1$, or \begin{align*} \operatorname{reg}(c,i) &= 0 \end{align*} with the zero-branch label chosen and all register values unchanged. Equalities, order comparisons, addition by $1$, truncated subtraction by $1$, finite disjunctions, and bounded conjunctions are primitive recursive. Hence the full transition predicate $\operatorname{Step}: \mathbb{N}^3 \to \{0,1\}$ is primitive recursive. The halting predicate $\operatorname{Halt}: \mathbb{N}^2 \to \{0,1\}$ is simpler: it only checks whether the current label decoded from $c$ is a halting label in the finite program decoded from $e$. This is also a bounded inspection of finite tuple codes, so it is primitive recursive. [/guided] [/step] [step:Define the primitive recursive history predicate $T_k$] For $e,t,x_1,\dots,x_k \in \mathbb{N}$, let $\operatorname{Init}_k(e,x_1,\dots,x_k,c)=1$ mean that $c$ is the initial configuration of program $e$ on input $(x_1,\dots,x_k)$: the initial label is the starting label, registers $1,\dots,k$ contain $x_1,\dots,x_k$, and every other register represented in $c$ is $0$. This is a primitive recursive predicate \begin{align*} \operatorname{Init}_k: \mathbb{N}^{k+2} &\to \{0,1\}. \end{align*} Define \begin{align*} T_k: \mathbb{N}^{k+2} &\to \{0,1\} \end{align*} by setting $T_k(e,x_1,\dots,x_k,t)=1$ exactly when all of the following conditions hold: \begin{align*} \operatorname{len}(t) &\geq 1,\\ \operatorname{Init}_k(e,x_1,\dots,x_k,\operatorname{entry}(t,0)) &= 1,\\ \operatorname{Step}(e,\operatorname{entry}(t,j),\operatorname{entry}(t,j+1)) &= 1 \quad \text{for every } j < \operatorname{len}(t)-1,\\ \operatorname{Halt}(e,\operatorname{entry}(t,\operatorname{len}(t)-1)) &= 1. \end{align*} The universal quantifier over $j$ is bounded by $\operatorname{len}(t)$. Bounded conjunctions of primitive recursive predicates are primitive recursive, so $T_k$ is primitive recursive. [/step] [step:Define the primitive recursive output extractor $C$] Define \begin{align*} C: \mathbb{N} &\to \mathbb{N} \end{align*} by letting $C(t)$ be the value of register $0$ in the last configuration coded by $t$ when $\operatorname{len}(t)\geq 1$, and $C(t)=0$ when $\operatorname{len}(t)=0$. In formulas, \begin{align*} C(t) = \begin{cases} \operatorname{reg}(\operatorname{entry}(t,\operatorname{len}(t)-1),0), & \operatorname{len}(t)\geq 1,\\ 0, & \operatorname{len}(t)=0. \end{cases} \end{align*} Since $\operatorname{len}$, $\operatorname{entry}$, predecessor, case distinction by zero, and $\operatorname{reg}$ are primitive recursive, the function $C$ is primitive recursive. [/step] [step:Show that minimisation over $T_k$ recovers exactly the computation of program $e$] Fix $e \in \mathbb{N}$ and $(x_1,\dots,x_k) \in \mathbb{N}^k$. Suppose first that the computation of program $e$ on input $(x_1,\dots,x_k)$ halts with output $y \in \mathbb{N}$. Let \begin{align*} c_0,c_1,\dots,c_n \end{align*} be the finite sequence of configurations produced by the computation, with $c_0$ the initial configuration, $c_n$ halting, and register $0$ of $c_n$ equal to $y$. Let $h \in \mathbb{N}$ be the code of this finite sequence. Then $T_k(e,x_1,\dots,x_k,h)=1$, so the least witness \begin{align*} s = \mu t\,\bigl[T_k(e,x_1,\dots,x_k,t)=1\bigr] \end{align*} exists. Since $T_k(e,x_1,\dots,x_k,s)=1$, the number $s$ codes a valid halting computation history for the same deterministic program and the same input. Determinism of the transition relation implies that every valid history beginning with the initial configuration is an initial segment of the unique computation of program $e$ on this input. Since the final configuration of $s$ is halting, it must be the actual halting configuration, and therefore \begin{align*} C(s) = y. \end{align*} Conversely, suppose there exists $t \in \mathbb{N}$ such that $T_k(e,x_1,\dots,x_k,t)=1$. Then $t$ codes a finite sequence beginning with the initial configuration, following the program transition relation at every successive step, and ending in a halting configuration. Hence the computation of program $e$ on input $(x_1,\dots,x_k)$ halts. If no such $t$ exists, then no finite halting computation history exists, so the computation does not halt and the minimisation expression is undefined. Thus, for every $e \in \mathbb{N}$ and every $(x_1,\dots,x_k) \in \mathbb{N}^k$, \begin{align*} \varphi_{e,k}(x_1,\dots,x_k) \simeq C\bigl(\mu t\, [T_k(e,x_1,\dots,x_k,t)=1]\bigr). \end{align*} This is the desired normal form. [/step]