Computing with λ-terms

$\mathsf{succ}\, \overline n \to_\beta \lambda f x.\, f\,(\overline n\, f\, x) \twoheadrightarrow_\beta \lambda f x.\, f\,(f^n(x)) = \overline{n+1}$.

$\mathsf{plus}\, \overline m\, \overline n \twoheadrightarrow_\beta \lambda f x.\, \overline m\, f\,(\overline n\, f\, x) \twoheadrightarrow_\beta \lambda f x.\, f^m(f^n(x)) = \overline{m + n}$.

$\mathsf{mult}\, \overline m\, \overline n \twoheadrightarrow_\beta \lambda f.\, \overline m\,(\overline n\, f)$. Now $\overline n\, f \twoheadrightarrow_\beta \lambda x.\, f^n(x)$, and iterating this function $m$ times gives $\lambda x.\, f^{mn}(x)$ after reduction; so the result is $\lambda f x.\, f^{mn}(x) = \overline{mn}$.

$\mathsf{exp}\, \overline m\, \overline n \twoheadrightarrow_\beta \overline n\,(\mathsf{mult}\, \overline m)\, \overline 1 \twoheadrightarrow_\beta (\mathsf{mult}\, \overline m)^n(\overline 1)$, which reduces to $\overline{m^n}$ by induction on $n$, using the case of multiplication.

The shorter term $\lambda m n.\, n\, m$ also works for $n \geq 1$, but $\overline 0\, \overline m \twoheadrightarrow_\beta \lambda x.\, x$, which is not $\overline 1 = \lambda f x.\, f\, x$ (the two are only η-convertible).

By induction on $n$, $\Phi^n(\mathsf{pair}\, \overline 0\, \overline 0)$ reduces to $\mathsf{pair}\, \overline{n \dotminus 1}\, \overline{n}$: this holds for $n = 0$, and $\Phi$ applied to $\mathsf{pair}\, \overline{a}\, \overline{n}$ reduces to $\mathsf{pair}\, \overline{n}\, \overline{n + 1}$. Since $\overline n\, \Phi\, A \twoheadrightarrow_\beta \Phi^n(A)$, the result follows by taking the first component.

Let $W = \lambda x.\, F\,(x\, x)$. Then $\mathsf{Y}\, F \to_\beta W\, W \to_\beta F\,(W\, W)$, and also $F\,(\mathsf{Y}\, F) \to_\beta F\,(W\, W)$; so both sides reduce to $F\,(W\, W)$. For $\Theta$, let $A = \lambda x y.\, y\,(x\, x\, y)$, so that $\Theta = A\, A$; then $\Theta\, F = A\, A\, F \to_\beta (\lambda y.\, y\,(A\, A\, y))\, F \to_\beta F\,(A\, A\, F) = F\,(\Theta\, F)$.

We first treat the total recursive functions, which is Kleene’s 1936 theorem, and then reduce the partial case to it with the normal form theorem.

Total functions. By Corollary 8.7, every total recursive function has a derivation from the basic functions by composition, primitive recursion and minimization of regular functions, in which all the functions are total. We show by induction on such a derivation that each of its functions $f : \nat^k \to \nat$ is λ-defined by some term $F$; since $f$ is total, this means $F\, \overline{n_1} \cdots \overline{n_k} \twoheadrightarrow_\beta \overline{f(\vec n)}$ for all $\vec n$. Below, $\vec{\overline n}$ stands for $\overline{n_1} \cdots \overline{n_k}$.

Basic functions. $Z$ is λ-defined by $\lambda n.\, \overline 0$, $S$ by $\mathsf{succ}$, and $p^k_i$ by $\lambda x_1 \cdots x_k.\, x_i$.

Composition. If $H, G_1, \dots, G_m$ λ-define $h, g_1, \dots, g_m$, then $F = \lambda \vec x.\, H\,(G_1\, \vec x) \cdots (G_m\, \vec x)$ satisfies $F\, \vec{\overline n} \twoheadrightarrow_\beta H\, \overline{g_1(\vec n)} \cdots \overline{g_m(\vec n)} \twoheadrightarrow_\beta \overline{f(\vec n)}$.

Primitive recursion. If $G$ and $H$ λ-define $g$ and $h$, then $f(\vec x, y)$ is λ-defined by iterating on pairs (counter, value), as for the predecessor:

Let $\Psi$ be the term $\lambda p.\, \cdots$ above with $\vec{\overline n}$ substituted for $\vec x$. By induction on $j$, $\Psi^j(\mathsf{pair}\, \overline 0\,(G\, \vec{\overline n}))$ reduces to $\mathsf{pair}\, \overline j\, \overline{f(\vec n, j)}$: for $j = 0$ because $G\, \vec{\overline n} \twoheadrightarrow_\beta \overline{g(\vec n)}$, and for $j + 1$ because $\Psi\,(\mathsf{pair}\, \overline j\, \overline v) \twoheadrightarrow_\beta \mathsf{pair}\, \overline{j + 1}\, \overline{h(\vec n, j, v)}$. Since $\overline y\, \Psi\, A \twoheadrightarrow_\beta \Psi^y(A)$, taking the second component gives $F\, \vec{\overline n}\, \overline y \twoheadrightarrow_\beta \overline{f(\vec n, y)}$. (For $k = 0$, $G\, \vec x$ is replaced by the numeral of the constant.)

Regular minimization. Let $f(\vec x) = \mu z\, [g(\vec x, z) = 0]$ with $g$ total and regular, λ-defined by $G$. With Turing’s combinator, let

By Theorem 11.6, $\mathsf{search}\, \vec{\overline n}\, \overline z \twoheadrightarrow_\beta (\mathsf{iszero}\,(G\, \vec{\overline n}\, \overline z))\; \overline z\; (\mathsf{search}\, \vec{\overline n}\,(\mathsf{succ}\, \overline z))$. If $g(\vec n, z) = 0$, this reduces to $\overline z$; otherwise it reduces to $\mathsf{search}\, \vec{\overline n}\,(\mathsf{succ}\, \overline z)$, hence to $\mathsf{search}\, \vec{\overline n}\, \overline{z + 1}$. By induction, $F\, \vec{\overline n} \twoheadrightarrow_\beta \mathsf{search}\, \vec{\overline n}\, \overline z$ for every $z \leq z_0 = f(\vec n)$, which exists by regularity, and finally $F\, \vec{\overline n} \twoheadrightarrow_\beta \overline{z_0}$.

Partial functions. For partial functions the constructions above are not adequate as they stand. For instance, the term for composition may have a normal form even if some $g_i(\vec x)$ diverges, when $H$ discards its argument — whereas $f(\vec x)$ must then be undefined. The normal form theorem avoids this problem: by Theorem 8.6, proved in the lesson Equivalence of the models by arithmetization of Turing machines (without using the λ-calculus), $f(\vec x) \simeq U(\mu s\, [g(\vec x, s) = 0])$ where $g(\vec x, s) = \overline{\mathrm{sg}}(\chi_{T_k}(e, \vec x, s))$ and $U$ are primitive recursive. Let $G$ and $U'$ λ-define $g$ and $U$, let $\mathsf{search}$ be built from $G$ as above, and let

If $f(\vec n)\converge$, the search succeeds at some $s_0$: then $\mathsf{search}\, \vec{\overline n}\, \overline 0 \twoheadrightarrow_\beta \overline{s_0}$ as in the total case, $\overline{s_0}\, \mathsf I\, \mathsf I \twoheadrightarrow_\beta \mathsf I^{s_0}(\mathsf I) \twoheadrightarrow_\beta \mathsf I$, and $F\, \vec{\overline n} \twoheadrightarrow_\beta \mathsf I\,\big(U'\, \overline{s_0}\big) \twoheadrightarrow_\beta \overline{U(s_0)} = \overline{f(\vec n)}$. If $f(\vec n)\diverge$, it remains to show that $F\, \vec{\overline n}$ has no normal form; by confluence, it suffices to show this for its reduct $(\mathsf{search}\, \vec{\overline n}\, \overline 0)\, \mathsf I\, \mathsf I\, (U'\,(\mathsf{search}\, \vec{\overline n}\, \overline 0))$. Here $\mathsf{search}\, \vec{\overline n}\, \overline 0$ reduces to $\mathsf{search}\, \vec{\overline n}\, \overline z$ for every $z$, and one shows that it has no head normal form: it reduces to no term of the form $\lambda y_1 \cdots y_j.\, y\, M_1 \cdots M_r$ (one says that it is unsolvable). Moreover, if $M$ has no head normal form, then neither has $M\, P_1 \cdots P_r$, which therefore has no normal form. We admit these two facts about head normal forms; they are proved in Barendregt’s monograph, in the chapters on solvability and on the representation of computable functions, where this construction is carried out in detail.

Code λ-terms by integers, for instance using de Bruijn indices to avoid α-equivalence issues and the sequence coding of the lesson Coding finite sequences. The following are primitive recursive on codes (we omit the routine verifications): substitution, the predicate ”$M$ is in normal form”, the function computing the result of one normal order step, its $t$-th iterate $N(M, t)$, the code of $\overline n$ as a function of $n$, and the predicate ”$M$ is a numeral” together with the extraction of its value. If $F$ λ-defines $f$, let $M_{\vec n}$ be the code of $F\, \overline{n_1} \cdots \overline{n_k}$; then

By Theorem 10.9, the search terminates exactly when $F\, \overline{n_1} \cdots \overline{n_k}$ has a normal form, which is then $\overline{f(\vec n)}$.