LOOP and WHILE programs

By induction on $P$: assignments are total, composition of total functions is total, and a finite iterate of a total function is total.

Primitive recursive ⇒ LOOP. We show by induction on a derivation of $f : \nat^k \to \nat$ that for all distinct indices $o, i_1, \dots, i_k$ there is a LOOP program, written $X_o \mathbin{:=} f(X_{i_1}, \dots, X_{i_k})$, which, started in any state $\sigma$, sets $X_o$ to $f(\sigma(i_1), \dots, \sigma(i_k))$ and modifies no variable other than $X_o$ and a finite set of auxiliary variables, which may be chosen disjoint from any given finite set of indices.

• Basic functions: $X_o \mathbin{:=} 0$, then $X_o \mathbin{:=} X_{i_1} ; X_o \mathbin{:=} X_o + 1$, and $X_o \mathbin{:=} X_{i_j}$.
• Composition $f = h \circ (g_1, \dots, g_m)$: choose fresh $Y_1, \dots, Y_m$, and run $Y_1 \mathbin{:=} g_1(\vec X) ; \dots ; Y_m \mathbin{:=} g_m(\vec X) ; X_o \mathbin{:=} h(Y_1, \dots, Y_m)$, with auxiliary variables of each subprogram chosen disjoint from $X_o$, $\vec X$, $\vec Y$.
• Primitive recursion, $f(\vec x, 0) = g(\vec x)$, $f(\vec x, y + 1) = h(\vec x, y, f(\vec x, y))$: with fresh $C$, $V$, $N$, run

By induction on the number of iterations, after $j$ iterations $C = j$ and $V = f(\vec x, j)$. For $k = 0$, where $g$ is a constant $a$, the first assignment is $V \mathbin{:=} 0$ followed by $a$ instructions $V \mathbin{:=} V + 1$. The subprograms never rely on the initial values of their auxiliary variables, since each of these is assigned before being read; this is why they can be run repeatedly inside the loop. (Writing $V \mathbin{:=} h(\vec X, C, V)$ is allowed: the program for $h$ reads $V$ and writes into a fresh variable, which is then copied into $V$.)

The function $f$ itself is computed by $X_0 \mathbin{:=} f(X_1, \dots, X_k)$, whose auxiliary variables are chosen distinct from $X_0, \dots, X_k$.

LOOP ⇒ primitive recursive. Let $P$ be a LOOP program computing $f : \nat^k \to \nat$, and let $m$ be larger than $k$ and than the indices of all variables occurring in $P$. Variables of index $\geq m$ are not modified by $P$ and do not influence its effect on the others. We code the relevant part of a state by the sequence code $s = [\sigma(0), \dots, \sigma(m-1)]$ of the lesson Coding finite sequences, and define $F_P(s)$ as the code of the state reached from $s$. We show by induction on subprograms $Q$ of $P$ that $F_Q$ is primitive recursive (on codes of length $m$):

• assignments: $F_{X_i := 0}(s) = \mathrm{set}(s, i, 0)$, $F_{X_i := X_i + 1}(s) = \mathrm{set}(s, i, (s)'_i + 1)$, $F_{X_i := X_j}(s) = \mathrm{set}(s, i, (s)'_j)$;
• sequence: $F_{Q ; R} = F_R \circ F_Q$;
• loop: $F_{\mathtt{LOOP}\ X_i\ \mathtt{DO}\ Q\ \mathtt{END}}(s) = G(s, (s)'_i)$ where $G(s, 0) = s$ and $G(s, n + 1) = F_Q(G(s, n))$, a primitive recursion.

Finally $f(\vec x) = \big(F_P([0, x_1, \dots, x_k, 0, \dots, 0])\big)'_0$, with $m$ entries in the code, is primitive recursive.

Partial recursive ⇒ WHILE. We extend the first part of the previous proof. The constructions for composition and primitive recursion are unchanged; with partial functions, the program simply does not terminate when one of the subprograms does not, which matches the conventions for partial functions. For minimization, $f(\vec x) \simeq \mu y\, [g(\vec x, y) = 0]$, with fresh $Y$ and $T$:

This program evaluates $g(\vec x, 0), g(\vec x, 1), \dots$ in order and stops at the first zero; it does not terminate if one of these computations does not, or if there is no zero. This is exactly the definition of minimization.

WHILE ⇒ partial recursive. As in the LOOP case, define for each subprogram $Q$ the partial function $F_Q$ on codes of states, and show by induction that it is partial recursive. Assignments, sequences and $\mathtt{LOOP}$ instructions are handled as before, now with partial functions (the iteration $G$ is defined by primitive recursion for partial functions). For $W = \mathtt{WHILE}\ X_i \neq 0\ \mathtt{DO}\ Q\ \mathtt{END}$, let $G(s, 0) \simeq s$ and $G(s, n + 1) \simeq F_Q(G(s, n))$. Then

By the definition of minimization, the search succeeds at $n$ exactly when $G(s, m)$ is defined with $X_i \neq 0$ for $m < n$, and $G(s, n)$ is defined with $X_i = 0$: this matches the semantics of the $\mathtt{WHILE}$ instruction.

The function computed by the program is partial recursive. By Kleene’s normal form (Theorem 8.6, proved in the lesson Equivalence of the models without using this corollary), it can be written $U(\mu s\, T_k(e, \vec x, s))$ with $U$ and $T_k$ primitive recursive. By Theorem 9.5, $U$ and $\chi_{T_k}$ are computed by LOOP programs, and the construction above for the minimization uses one $\mathtt{WHILE}$ instruction.

Let $P$ compute $f : \nat^k \rightharpoonup \nat$, and let $m$ be larger than $k$ and than the indices of all variables of $P$. The variable $X_i$, for $i < m$, is represented by the register $R_{i+2}$; the register $R_1$ is kept equal to $0$ and serves for unconditional jumps $J(1, 1, q)$ and for tests against $0$. Each occurrence of a $\mathtt{LOOP}$ instruction in $P$ receives two registers $R_a, R_b$ of its own, with indices larger than $m + 1$. For each subprogram $Q$ of $P$ we define a URM program $Q^*$ in standard form, by induction on $Q$; let $t$ denote the length of the translation of the body.

• $(X_i \mathbin{:=} 0)^* = Z(i+2)$, $(X_i \mathbin{:=} X_i + 1)^* = S(i+2)$, $(X_i \mathbin{:=} X_j)^* = T(j+2, i+2)$.
• $(Q ; Q')^*$ is the concatenation $Q^* Q'^*$ of Definition 4.7.
• $(\mathtt{WHILE}\ X_i \neq 0\ \mathtt{DO}\ Q\ \mathtt{END})^*$ is $J(i+2, 1, t+3)$, followed by $Q^*$ with all jump targets increased by $1$, followed by $J(1, 1, 1)$.
• $(\mathtt{LOOP}\ X_i\ \mathtt{DO}\ Q\ \mathtt{END})^*$, with the registers $R_a, R_b$ of this occurrence, is $T(i+2, a)$, $Z(b)$, $J(a, b, t+6)$, followed by $Q^*$ with all jump targets increased by $3$, followed by $S(b)$, $J(1, 1, 3)$.

In each case the jump targets are at most the length plus one, so $Q^*$ is in standard form. We show by induction on $Q$: if $Q^*$ is started at its first instruction in a register state $r$ with $r(1) = 0$ and $r(i+2) = \sigma(i)$ for all $i < m$, then $Q^*$ halts if and only if $[\![Q]\!](\sigma)\converge$, and in that case it halts in a state $r'$ with $r'(1) = 0$ and $r'(i+2) = [\![Q]\!](\sigma)(i)$ for all $i < m$. Assignments are immediate, and sequences follow from Lemma 4.8. For a $\mathtt{WHILE}$ instruction, by induction on $n$, the program reaches its first instruction for the $(n+1)$-th time if and only if $[\![Q]\!]^n(\sigma)\converge$ and $[\![Q]\!]^j(\sigma)(i) \neq 0$ for all $j < n$, and then the registers represent $[\![Q]\!]^n(\sigma)$; since $R_1 = 0$, the first jump exits exactly when the represented value of $X_i$ is $0$, as in Definition 9.2. For a $\mathtt{LOOP}$ instruction, $R_a$ holds the value of $X_i$ on entry and is not modified by $Q^*$, which only uses the registers of the occurrences inside $Q$; by induction on $j$, the test $J(a, b, \cdot)$ is reached for the $(j+1)$-th time with $R_b = j$ and the registers representing $[\![Q]\!]^j(\sigma)$, so the program exits after $\sigma(i)$ iterations.

The program for $f$ consists of $T(k, k+2), T(k-1, k+1), \dots, T(1, 3)$, which move the input to the registers of $X_1, \dots, X_k$ (in decreasing order, so that no input is overwritten before it is copied), then $Z(1)$, $Z(2)$, then $P^*$, then $T(2, 1)$. After the first part, $R_1 = 0$ and $R_{i+2}$ holds $\sigma_{\vec x}(i)$ for every $i < m$, and the registers of the $\mathtt{LOOP}$ occurrences hold $0$ (they are not used before being set anyway). By the claim, the program halts if and only if $f(\vec x)\converge$, and then $R_1$ contains $[\![P]\!](\sigma_{\vec x})(0) = f(\vec x)$.