[proofplan]
We make the statement precise as an effective construction at the level of codes of register machines. The hypothesis gives a register machine $M$ of arity $k + 1$ with $f_{M, k + 1} = g$. For each value $v \in \mathbb{W}$ of the frozen argument we build a small "loader" machine $M_v$ of arity $k$ that preserves its $k$ inputs in registers $0, \ldots, k - 1$ and writes $v$ as a hard-wired literal into register $k$; concatenating $M_v$ with $M$ yields a machine $M_v \circ M$ that, started on $w \in \mathbb{W}^k$, first loads $(w, v)$ into registers $0, \ldots, k$ and then runs $M$. By the correctness of $M$ this computes $g(w, v)$. It remains to show that $v \mapsto \operatorname{code}(M_v \circ M)$ is a total computable function of $v$, which we do by exhibiting an explicit computable composition of (i) a code-assembly function that writes out the text of $M_v$ as a word over the code alphabet from $v$, and (ii) the code-concatenation operation from the [concatenation lemma](/theorems/1810). The output is then the desired total computable $h$.
[/proofplan]
[step:Fix notation for machine encodings and the universal partial function $f_{M, k}$]
Let $\mathbb{W} = \Sigma^*$ be the fixed word alphabet of the course, with fixed separators $\sharp, |$ and a fixed injective encoding $\operatorname{code}$ of register machines as words of $\mathbb{W}$, as in the proof of [Computability of the Configuration Function](/theorems/1818). For any register machine $N$ of arity $k$, we write $f_{N, k} : \mathbb{W}^k \rightharpoonup \mathbb{W}$ for the partial function computed by $N$: $f_{N, k}(w)$ is the contents of register $0$ at the first moment $N$ reaches its halt state $q_{H, N}$ started on inputs $w_1, \ldots, w_k$ loaded into registers $0, \ldots, k - 1$ with all other registers empty; it is undefined if $N$ never halts on $w$.
The statement to prove is: given a computable partial function
\begin{align*}
g : \mathbb{W}^{k + 1} &\rightharpoonup \mathbb{W},
\end{align*}
there exists a total computable function
\begin{align*}
h : \mathbb{W} &\to \mathbb{W}
\end{align*}
such that for every $v \in \mathbb{W}$ and every $w \in \mathbb{W}^k$,
\begin{align*}
f_{h(v), k}(w) &= g(w, v).
\end{align*}
Since $g$ is computable, fix once and for all a register machine $M$ of arity $k + 1$ such that $f_{M, k + 1} = g$. The word $\operatorname{code}(M)$ is a fixed literal constant of the construction.
[/step]
[step:Define the parametrised loader machine $M_v$ for each frozen argument $v$]
For each $v \in \mathbb{W}$ we define a register machine $M_v$ of arity $k$ with input registers $0, \ldots, k - 1$. Its program has two phases:
(a) *Preserve the $k$ existing inputs.* Registers $0, \ldots, k - 1$ already hold $w_1, \ldots, w_k$ and are left untouched.
(b) *Load $v$ into register $k$.* Register $k$ is initially empty. Write the letters of $v = v_1 v_2 \cdots v_{|v|}$ into register $k$ one by one using $|v|$ "write letter $v_i$ to register $k$" instructions in sequence, then transition to $M_v$'s halt state.
Formally, let $q_{v,0}, q_{v,1}, \ldots, q_{v, |v|} = q_{H, v}$ be $|v| + 1$ fresh state names, one per letter-write step plus a halting state. The instructions of $M_v$ are: at state $q_{v, i - 1}$ for $1 \le i \le |v|$, write $v_i$ to register $k$ and transition to $q_{v, i}$; at state $q_{v, |v|} = q_{H, v}$, halt. The machine's start state is $q_{v, 0}$.
Then, on input $w = (w_1, \ldots, w_k)$, $M_v$ halts after $|v|$ steps with registers $0, \ldots, k - 1, k$ holding $w_1, \ldots, w_k, v$. By the convention that $f_{M_v, k}$ reads register $0$, the function $f_{M_v, k}(w) = w_1$; but our use of $M_v$ is not as a standalone machine — we will immediately concatenate it with $M$, so the value of register $0$ at the halt of $M_v$ is not the relevant quantity. What matters is the *configuration* $(w_1, \ldots, w_k, v)$ of registers $0, \ldots, k$ at the halt of $M_v$, which is exactly the input configuration that $M$ (of arity $k + 1$) expects.
[/step]
[step:Define the composite machine $M_v \circ M$ and verify it computes $w \mapsto g(w, v)$]
Let $M_v \circ M$ be the concatenation of $M_v$ and $M$ in the sense of the [concatenation lemma](/theorems/1810): the two machines' state sets are taken disjoint (by renaming), their instruction sets are unioned, and the halt state $q_{H, v}$ of $M_v$ is re-routed to the start state of $M$. The registers are shared: after $M_v$ halts, the contents of registers $0, \ldots, k$ are handed off to $M$ without copying. The halt state of the composite is the halt state of $M$.
By [concatenation lemma](/theorems/1810), $M_v \circ M$ is a well-defined register machine of arity $k$ (it takes $k$ inputs in registers $0, \ldots, k - 1$), and its computation on input $w \in \mathbb{W}^k$ unfolds as follows:
- $M_v$ runs first: after $|v|$ steps, registers $0, \ldots, k$ hold $(w_1, \ldots, w_k, v)$ and $M_v$ halts.
- Control passes to the start state of $M$. From this configuration, $M$ runs as if started on inputs $(w_1, \ldots, w_k, v) = (w, v)$ loaded into registers $0, \ldots, k$ with all other registers empty (the latter holds because the loader $M_v$ did not touch any register other than $k$, and the initial configuration of the composite has all registers other than the input registers $0, \ldots, k - 1$ empty; register $k$ was empty before $M_v$ ran and is filled with $v$ by $M_v$).
Therefore, for every $w \in \mathbb{W}^k$,
\begin{align*}
f_{M_v \circ M, k}(w) &= f_{M, k + 1}(w, v) = g(w, v),
\end{align*}
with both sides defined or both sides undefined. (Undefined here means the register machine runs forever; the first equality holds because the composite halts iff $M$ halts when started on $(w, v)$, and in that case the register-$0$ contents at the halt of the composite equal the register-$0$ contents at the halt of $M$.)
[/step]
[step:Define $h(v) := \operatorname{code}(M_v \circ M)$ and show $h$ is computable]
Define
\begin{align*}
h : \mathbb{W} &\to \mathbb{W}, \\
v &\mapsto \operatorname{code}(M_v \circ M).
\end{align*}
By the conclusion of Step 3, $f_{h(v), k}(w) = g(w, v)$ for every $v, w$, matching the specification. It remains to show $h$ is total and computable.
*Totality.* $M_v$ is defined for every $v \in \mathbb{W}$ (the construction in Step 2 uses only finite data read off from $v$), and the concatenation with $M$ is defined for every pair of machines. Hence $\operatorname{code}(M_v \circ M)$ is defined for every $v$.
*Computability.* We exhibit a register machine computing $h$ by composing two computable sub-routines.
[claim:The function $\varphi : \mathbb{W} \to \mathbb{W}$, $v \mapsto \operatorname{code}(M_v)$ is computable]
The encoding $\operatorname{code}(M_v)$ is a word over the code alphabet that lists $M_v$'s states and instructions in a fixed format. By the construction of Step 2, $M_v$'s data depend on $v$ only through the letters $v_1, \ldots, v_{|v|}$ and the length $|v|$. Concretely, $\operatorname{code}(M_v)$ has the form
\begin{align*}
\operatorname{code}(M_v) &= A \cdot B(v_1) \cdot B(v_2) \cdots B(v_{|v|}) \cdot C
\end{align*}
where:
- $A$ is a fixed prefix encoding $M_v$'s fixed preamble — the declarations of states $q_{v,0}, q_{v,1}, \ldots$ up to the number of states needed, the fixed arity $k$, and the fixed start state $q_{v, 0}$. Under a fixed encoding convention the state names $q_{v, i}$ can be encoded by a finite template indexed by $i$; the number of states depends on $|v|$, so $A$ actually depends on $|v|$ only through its length (we address this by making the state-declaration block be built letter-by-letter from $v$ below).
- $B(a)$, for each letter $a \in \Sigma$, is the fixed block encoding one instruction "at the next fresh state, write $a$ to register $k$ and transition to the next fresh state". Each $B(a)$ is a fixed finite word depending only on $a$ and on a counter tracking which fresh state to use.
- $C$ is a fixed suffix encoding the halt transition and the end-of-program marker.
Because the dependence on $v$ enters only through its letters and its length, $\operatorname{code}(M_v)$ can be assembled by a register machine $M_\varphi$ that:
(a) Reads $v$ letter-by-letter from its input register. Using the left-to-right reading technique of Step 3 of the proof of [Regular Languages are Computable](/theorems/1814) — reverse $v$ into a scratch register $R_v^*$ using the letter-by-letter reversal routine, then repeatedly pop the last letter of $R_v^*$ — each letter of $v$ is read exactly once.
(b) Maintains two scratch counters: a state-index counter $R_i$ (initialised to $0$, incremented after each letter) and an output register $R_\text{out}$ for the assembled code.
(c) Before reading any letters, writes the preamble $A$ into $R_\text{out}$, where $A$ depends on $|v|$. To handle this cleanly we emit $A$ in a streaming fashion interleaved with the letter-processing: first emit a fixed header (arity, encoding-format markers, start state), then emit state-declaration sub-blocks $D(0), D(1), \ldots, D(|v|)$ one per letter of $v$ (each $D(i)$ is a fixed word possibly parametrised by $i$ via a literal encoding of $i$ derivable from the counter $R_i$ by a fixed word-for-integer routine; under the standard encoding convention, state indices are encoded in unary or shortlex, and the $i$-th state's declaration sub-block is emittable from $R_i$'s contents by a fixed routine).
(d) For each letter $a$ of $v$ read in (a), emits the instruction block $B(a)$ appended to $R_\text{out}$. The block $B(a)$ depends only on the fixed letter $a$ and on the current value of $R_i$ (to reference the correct "fresh" state); both are available to the machine at emission time.
(e) After all letters of $v$ have been processed, emits the suffix $C$ (the halt transition) into $R_\text{out}$.
(f) Copies $R_\text{out}$ into register $0$ and halts.
Each of (a)–(f) is a fixed finite sub-routine plus a loop bounded by $|v|$; at each loop iteration the work is bounded (one letter read, a fixed block emission, one increment of $R_i$). By the composition and primitive-recursion closures of Step 4 (L1) and Step 5 (L2) of the proof of [Recursive Implies Computable](/theorems/1817), or more directly by exhibiting $M_\varphi$ as an explicit register machine as above, $\varphi$ is computable and total. Moreover, because the loop in (a)–(e) runs exactly $|v|$ iterations and every sub-routine halts, $M_\varphi$ halts on every input.
[/claim]
[claim:The function $\psi : \mathbb{W} \to \mathbb{W}$, $c \mapsto \operatorname{code}(N_c \circ M)$ (where $N_c$ is the machine decoded from $c$, and $\circ$ denotes concatenation with the fixed $M$) is computable]
The [concatenation lemma](/theorems/1810) asserts that given codes $c_1, c_2$ of two register machines $N_1, N_2$ with matching arities, the code $\operatorname{code}(N_1 \circ N_2)$ is computable from $(c_1, c_2)$; equivalently, the map $(c_1, c_2) \mapsto \operatorname{code}(N_1 \circ N_2)$ is a (total) computable function of two arguments. Specialising the second argument to the fixed literal $c_2 = \operatorname{code}(M)$ (a finite fixed constant), the map $\psi : c \mapsto \operatorname{code}(N_c \circ M)$ is the composition of $c \mapsto (c, \operatorname{code}(M))$ (prepending a fixed constant — computable by a fixed sequence of "write letter" instructions followed by the identity on the input) with the two-argument concatenation map. By L1 of the proof of [Recursive Implies Computable](/theorems/1817) (closure of computable functions under composition), $\psi$ is computable. Totality of $\psi$ follows from totality of concatenation on well-formed codes (both $c$ and $\operatorname{code}(M)$ are well-formed codes of arity $k$ and $k + 1$ respectively, matching the concatenation rule).
[/claim]
Now $h = \psi \circ \varphi$: for every $v$,
\begin{align*}
h(v) = \operatorname{code}(M_v \circ M) = \psi(\operatorname{code}(M_v)) = \psi(\varphi(v)).
\end{align*}
Both $\varphi$ (Claim 1) and $\psi$ (Claim 2) are total computable, so $h$ is total computable by L1 of the proof of [Recursive Implies Computable](/theorems/1817).
[/step]
[step:Conclude]
The function $h$ is total and computable, and for every $v \in \mathbb{W}$ and $w \in \mathbb{W}^k$,
\begin{align*}
f_{h(v), k}(w) &= f_{M_v \circ M, k}(w) = f_{M, k + 1}(w, v) = g(w, v),
\end{align*}
where the first equality is the definition $h(v) = \operatorname{code}(M_v \circ M)$, the second is the correctness of the concatenation construction (Step 3), and the third is the defining property of $M$ (Step 1). This is the conclusion of the theorem.
[/step]