How to define halting status in combinatory logic

Question

We all know that combinatory logic can be used to express programs, for example:

$S(K(SI))K\alpha\beta \rightarrow K(SI)\alpha(K\alpha)\beta \rightarrow SI(K\alpha)\beta \rightarrow I\beta(K\alpha\beta) \rightarrow I\beta\alpha \rightarrow \beta\alpha$

This program can reverse the order of two terms.

When considering the halting problem, I am confused how to define a halting status in any reduction process.

Maybe we can define it as a status in a reduction process to reach the least length of terms. But it is not easy to judge it already reaches the least length or not.

Could anybody give the answer or some references? thanks.

Answer 1

The combinatory logic analogue of a halting program is a term with a normal form. You suggested “Maybe we can define it as a status in a reduction process to reach the least length of terms”. But remember that if a term has a normal form, the normal form is unique. (This is the Church-Rosser property.) So there is no need to ask which normal form has the least length, because there is only one normal form.

When discussing algorithms we can ask if some program $P$ halts when given some input $i$; $P$ might or might not halt depending on what $i$ is. The combinatory logic analogue of this is that you might have a term $T$ where $T x$ reduces to a normal form, or doesn't, depending on what $x$ is.

The proof that halting is undecidable turns into a proof that there is no term $H$ such that $H x = K$ precisely when $x$ has a normal form and $H x = K I$ precisely when it doesn't. (Recall that $K$ and $K I$ are the conventional encodings of true and false and that $K a b = a$ and $K I a b = b$.)

The proof that there is no such $H$ is entirely analogous to the same proof for Turing machines, and goes like this: Suppose there is such an $H$, and let $$Z = (C (C (B H (S I I)) \omega) I).$$ ($\omega$ is an abbreviation for some term with no normal form, such as $(S I I (S I I))$.) This looks mysterious but it is simply the combinatory translation of $$\lambda x. \text{if } (H (x x)) \text{ then } \omega \text{ else } I$$ Then consider $S I I Z$, which reduces as follows:

$$\begin{align} & S I I Z \\ & I Z (I Z) \\ & Z Z \\ & (C (C (B H (S I I)) \omega) I) Z \\ & (C (B H (S I I)) \omega) Z I \\ & (B H (S I I)) Z \omega I \\ & H (S I I Z) \omega I \end{align}$$

(Recall $B x y z \Rightarrow x (y z)$ and $C x y z \Rightarrow x z y$.)

Now by hypothesis $H (S I I Z)$ reduces to either $K$ or to $K I$.

• If $H(S I I Z)\Rightarrow K$ we continue $H (S I I Z) \omega I\Rightarrow K\omega I\Rightarrow \omega$, which shows that $(S I I Z)$ reduces to $\omega$ and so has no normal form. But then $H$ has failed to do what we wanted, because $H (S I I Z)$ should have yielded $K I$.
• But if $H(S I I Z)\Rightarrow K I$ then we continue $H (S I I Z) \omega I\Rightarrow K I\omega I \Rightarrow I I \Rightarrow I$ and $H$ has still failed, since $S I I Z$ has the normal form $I$ and $H (S I I Z)$ was supposed to reduce to $K$.

The standard reference is Henk Barendregt The Lambda Calculus, Its Syntax and Semantics which certainly discusses this.