Term that can distinguish beta-equivalent normal forms in the untyped lambda calculus

Question

I'm trying to work through two (non-assessed) class-work questions and am stuck on a question that seems similar to one I could do.

The first question was to prove that there does not exist a $\lambda$-term $f$ that, given two $\lambda$-terms $m$ and $n$, can determine whether or not they are $\beta$-equivalent — i.e. there is no $f$ such that $\lambda\beta \vdash f \ m \ n = \textbf{t}$ if $m \ =_\beta \ n$ and $\lambda\beta \vdash f \ m \ n = \textbf{f}$ if $m \ \neq_\beta \ n$. I think I have done this relatively easily by appealing to the Scott-Curry theorem.

I'm now stuck on proving the same but for $m, n$ being in normal form. If I try to use the Scott-Curry theorem, showing that the set $A = \{ x = m \mid x \mbox{ in normal form} \}$ is inseparable, so that no $g \equiv f \ m$ can exist, then I cannot show that $A$ is closed under $\beta$-equality, which we require to apply the Scott-Curry theorem. So I don't think this is the correct approach.

Could anyone give me some help on how to formally prove this? I've played around with contexts, Böhm's theorem, etc. I feel like the fact $m, n$ are not required to be closed is important?

Answer 1

Let's split it into two parts:

First let $m$ and $n$ be terms that have a normal form (but are not necessarily in normal form). Let \begin{align*} \mathbf{A} &= \{x \;|\; x =_\beta m\} \\ \mathbf{B} &= \{x \;|\; x \neq_\beta m \mbox{ and $x$ has a normal form }\} \end{align*} These sets are nonempty, disjoint and closed under $\beta$-equivalence, so we can apply Scott-Curry theorem and conclude that they're inseparable. So there is no algorithm that can determine if two such terms $m$ and $n$ are equal or not.

For the second part: Intuitively, a lambda term cannot distinguish if its arguments are in normal form or not. Suppose we have $f$ that can determine if two terms in normal form $m$ and $n$ are equal or not. Now let $m'$ and $n'$ be terms that have a normal form. We can use a normalizing reduction strategy to reduce them to their normal forms (which is accomplished in a finite number of steps), apply $f$ and determine if they're equal or not, which contradict the previous part.