<p>Let's split it into two parts:</p>

<p>First let $m$ and $n$ be terms that <em>have a normal form</em> (but are not necessarily <em>in</em> normal form). Let
\begin{align*}
 \mathbf{A} &amp;= \{x \;|\; x =_\beta m\} \\
 \mathbf{B} &amp;= \{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.</p>

<p>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 <em>in</em> normal form $m$ and $n$ are equal or not. Now let $m'$ and $n'$ be terms that <em>have</em> a normal form. We can use <a href="http://mathgate.info/cebrown/notes/barendregt.php#redstratdefs" rel="nofollow">a normalizing reduction strategy</a> 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.</p>

CC BY-SA 3.0
2012-08-14T19:18:04.750Z
2012-08-14T19:18:04.750Z
Petr
<p>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.</p>

<p>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.</p>

<p>I'm now stuck on proving the same but for $m, n$ being in <em>normal form</em>. 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.</p>

<p>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?</p>

CC BY-SA 3.0
2011-12-15T02:05:43.567Z
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.
Ahmed Masud
CC BY-SA 3.0
2011-12-15T16:05:52.933Z
I don't see how this isn't TCS. Perhaps it may not be research-level.
Dave Clarke
CC BY-SA 3.0
2011-12-15T16:43:36.150Z
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.
Dominik Schulz
<lo.logic><computability><pl.programming-languages><lambda-calculus>
Term that can distinguish beta-equivalent normal forms in the untyped lambda calculus
Dominik Schulz
# Term that can distinguish beta-equivalent normal forms in the untyped lambda calculus

(Asked by: username_0 on 2011-12-14)

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?

**Tags:** lo.logic, computability, pl.programming-languages, lambda-calculus

> **Comments:**
> **username_1**: 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.  
> **username_2**: I don't see how this isn't TCS. Perhaps it may not be research-level.  
> **username_0**: 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.  

---

## 1 answers

### Answer by username_3 on 2012-08-14. Score: 4

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](http://mathgate.info/cebrown/notes/barendregt.php#redstratdefs) 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.


---

