Combinatory Logic - Undecidability of Combinatorial Calculus

Undecidability of Combinatorial Calculus

A normal form is any combinatory term in which the primitive combinators that occur, if any, are not applied to enough arguments to be simplified. It is undecidable whether a general combinatory term has a normal form; whether two combinatory terms are equivalent, etc. This is equivalent to the undecidability of the corresponding problems for lambda terms. However, a direct proof is as follows:

First, observe that the term

Ω = (S I I (S I I))

has no normal form, because it reduces to itself after three steps, as follows:

(S I I (S I I)) = (I (S I I) (I (S I I))) = (S I I (I (S I I))) = (S I I (S I I))

and clearly no other reduction order can make the expression shorter.

Now, suppose N were a combinator for detecting normal forms, such that

(N x) => T, if x has a normal form F, otherwise.

(Where T and F represent the conventional Church encodings of true and false, λx.λy.x and λx.λy.y, transformed into combinatory logic. The combinatory versions have T = K and F = (K I).)

Now let

Z = (C (C (B N (S I I)) Ω) I)

now consider the term (S I I Z). Does (S I I Z) have a normal form? It does if and only if the following do also:

(S I I Z) = (I Z (I Z)) = (Z (I Z)) = (Z Z) = (C (C (B N (S I I)) Ω) I Z) (definition of Z) = (C (B N (S I I)) Ω Z I) = (B N (S I I) Z Ω I) = (N (S I I Z) Ω I)

Now we need to apply N to (S I I Z). Either (S I I Z) has a normal form, or it does not. If it does have a normal form, then the foregoing reduces as follows:

(N (S I I Z) Ω I) = (K Ω I) (definition of N) = Ω

but Ω does not have a normal form, so we have a contradiction. But if (S I I Z) does not have a normal form, the foregoing reduces as follows:

(N (S I I Z) Ω I) = (K I Ω I) (definition of N) = (I I) I

which means that the normal form of (S I I Z) is simply I, another contradiction. Therefore, the hypothetical normal-form combinator N cannot exist.

The combinatory logic analogue of Rice's theorem says that there is no complete nontrivial predicate. A predicate is a combinator that, when applied, returns either T or F. A predicate N is nontrivial if there are two arguments A and B such that NA=T and NB=F. A combinator N is complete if and only if NM has a normal form for every argument M. The analogue of Rice's theorem then says that every complete predicate is trivial. The proof of this theorem is rather simple.

Proof: By reductio ad absurdum. Suppose there is a complete non trivial predicate, say N.
Because N is supposed to be non trivial there are combinators A and B such that
(N A) = T and
(N B) = F.

Define NEGATION ≡ λx.(if (N x) then B else A) ≡ λx.((N x) B A)
Define ABSURDUM ≡ (Y NEGATION)

Fixed point theorem gives: ABSURDUM = (NEGATION ABSURDUM), for
ABSURDUM ≡ (Y NEGATION) = (NEGATION (Y NEGATION)) ≡ (NEGATION ABSURDUM).

Because N is supposed to be complete either:

1. (N ABSURDUM) = F or
2. (N ABSURDUM) = T

Case 1: F = (N ABSURDUM) = N (NEGATION ABSURDUM) = (N A) = T, a contradiction.
Case 2: T = (N ABSURDUM) = N (NEGATION ABSURDUM) = (N B) = F, again a contradiction.

Hence (N ABSURDUM) is neither T nor F, which contradicts the presupposition that N would be a complete non trivial predicate. QED.

From this undecidability theorem it immediately follows that there is no complete predicate that can discriminate between terms that have a normal form and terms that do not have a normal form. It also follows that there is no complete predicate, say EQUAL, such that:
(EQUAL A B) = T if A = B and
(EQUAL A B) = F if A ≠ B.
If EQUAL would exist, then for all A, λx.(EQUAL x A) would have to be a complete non trivial predicate.