3
$\begingroup$

The proofs I have so far seen for the undecidability of $\beta$-normalisation all make use of Gödel numbering in order to first prove the more general Scott-Curry theorem. As an exercise, I have tried to write a proof that does not use Gödel numbering and would appreciate some feedback on whether it is sound/complete, and whether there is redundancy or not. (Some trivial facts are left implicit, such as the fact that if $X =_\beta Y$, then $X$ and $Y$ both normalise or they are both unnormalisable.)

Some preliminary conventional definitions: \begin{aligned} \mathbf{I} &\; \equiv (\lambda x.x) \\ \Omega &\; \equiv (\lambda x.xx)(\lambda x.xx) \end{aligned}

Note that I assume the Turing completeness of the $\lambda$-calculus.


Theorem. $\beta$-normalisation is undecidable. That is, there does not exist a combinator $D$ such that $\forall X \in \Lambda$: \begin{aligned} DX =_\beta \mathbf{T} \; &\Longleftrightarrow X \text{ has a } \beta\text{-normal form} \\ DX =_\beta \mathbf{F} \; &\Longleftrightarrow X \text{ has no } \beta\text{-normal form} \end{aligned} with $\mathbf{T}$, $\mathbf{F}$ two distinct $\beta$-nfs.

Proof. Suppose $D$ exists.

According to Böhm's theorem, since $\mathbf{T}$ and $\mathbf{F}$ are distinct $\beta$-nfs, $\exists L_1,\ldots,L_n$ with $n \geq 0$ such that \begin{aligned} \mathbf{T}L_1\ldots L_nAB \; &=_\beta A \\ \mathbf{F}L_1\ldots L_nAB \; &=_\beta B \end{aligned}

Define $\mathbf{P} \equiv (\lambda x.D(xx)L_1 \ldots L_n\Omega \mathbf{I})$.

$\mathbf{PP}$ either has a $\beta$-nf or it does not.

  1. $\mathbf{PP}$ has a $\beta$-nf, i.e. $D(\mathbf{PP}) =_\beta \mathbf{T}$. Then: \begin{aligned} \mathbf{PP} \; &\equiv (\lambda x.D(xx)L_1 \ldots L_n\Omega \mathbf{I}) \mathbf{P} \\ &=_\beta D(\mathbf{PP}) L_1 \ldots L_n \Omega \mathbf{I} \\ &=_\beta \mathbf{T}L_1 \ldots L_n \Omega \mathbf{I} \\ &=_\beta\Omega \end{aligned} Since $\Omega$ has no $\beta$-nf, neither does $\mathbf{PP}$. Contradiction.

  2. $\mathbf{PP}$ has no $\beta$-nf, i.e. $D(\mathbf{PP}) =_\beta \mathbf{F}$. Then: \begin{aligned} \mathbf{PP} \; &\equiv (\lambda x.D(xx)L_1 \ldots L_n\Omega \mathbf{I}) \mathbf{P} \\ &=_\beta D(\mathbf{PP}) L_1 \ldots L_n \Omega \mathbf{I} \\ &=_\beta \mathbf{F}L_1 \ldots L_n \Omega \mathbf{I} \\ &=_\beta\mathbf{I} \end{aligned} Since $\mathbf{I}$ has a $\beta$-nf, so does $\mathbf{PP}$. Contradiction.

Thus there can be no such $D$. $\square$


One particular question:

  1. Can I make assumptions about $\mathbf{T}$ and $\mathbf{F}$ without it affecting the validity of my proof? For example, a decider is usually understood to map each input to $\{0, 1\}$ or $\{True, False\}$. Might I just as well choose $T \equiv (\lambda xy.x)$, $F \equiv (\lambda xy.y)$, $P \equiv (\lambda x. D(xx) \Omega \mathbf{I})$ and thereby drop the dependency on Böhm's theorem altogether?

    To me it seems unsatisfactory, because in that case it might not be clear that the contradiction cannot be avoided by choosing different $\lambda$ representatives for $\mathbf{T}$ and $\mathbf{F}$. Then again, I have seen a proof that explicitly used the Church numerals for 0 and 1 and a different choice for $P$.

Other feedback is very welcome too.

$\endgroup$
2
$\begingroup$

I'm a little late to the party, but I think it might be useful to provide some answer here.

Your theorem is correct, there is no combinator $D$ such that for all $\lambda$-terms $X$, $DX=_\beta\mathbf{T}$ if $X$ has a normal form and $DX=_\beta\mathbf{F}$ otherwise.

Your proof is correct, and you do not need Böhm's theorem: $L_1,\ldots, L_n$ is just the empty list here ($\mathrm{T}AB=A$ for example)! You could replace $\mathrm{T}$ and $\mathrm{F}$ with any other distinct normal forms, and your proof would go through in a similar way, but you would need Böhm's theorem to reduce to the case with $\mathrm{T}$ and $\mathrm{F}$.

The more general remark though, is this:

It is incorrect that the statement of the theorem given in your question is "Normalization of untyped $\lambda$-terms is undecidable."

You've proven something much weaker: it is impossible to decide normalization of a $\lambda$-term using only combinators. But there are much simpler things you already cannot do with combinators! For example, determining whether the head of $X$ is a $\lambda$-abstraction, an application or a variable is already impossible!

What you want to prove is that no such $D$ exists, even if you are given access to the code of $X$. This is equivalent to saying that there is no $D$ such that

$$ D\lceil X\rceil =_\beta\mathbf{T}$$

if $X$ is normalizing and

$$D\lceil X\rceil =_\beta\mathbf{F}$$

otherwise, where $\lceil X\rceil$ is an encoding of $X$ using, e.g. Church numerals.

This is strictly more general than the previous question, since it's always possible to write some $E$ ("eval") combinator such that $E\lceil X\rceil=_\beta X$. It's also possible to answer the syntactic questions I asked above.

The fact that there is no "trick" using the internals of the definition of $X$ to determine whether it terminates is the true undecidability result, and its proof probably cannot be made much simpler than the ones involving the Scott-Curry theorem.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.