6
$\begingroup$

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?

$\endgroup$
  • 1
    $\begingroup$ Not sure if this is theoretical CS ... but here is a hint: "Having a normal form is equivalent to asking whether a program terminates." the question is closed under equality. $\endgroup$ – Ahmed Masud Dec 15 '11 at 2:05
  • 8
    $\begingroup$ I don't see how this isn't TCS. Perhaps it may not be research-level. $\endgroup$ – Dave Clarke Dec 15 '11 at 16:05
  • $\begingroup$ Could you explain how "having a normal form is equivalent to asking whether a program terminates" is relevant to the question? I understand that determining whether a term has a normal form is undecidable, so that if my set A above was for terms x that have a normal form it would be closed under beta-equality. But here my terms are normal forms. $\endgroup$ – Dominik Schulz Dec 15 '11 at 16:43
4
$\begingroup$

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.

$\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.