[Haskell-cafe] Lambda Calculus question on equivalence

[Francesco Mazzoli]

At Fri, 03 May 2013 16:34:28 +0200,
Andreas Abel wrote:
> The answer to your question is given in Boehm's theorem, and the answer 
> is "no", as you suspect.
> 
> For the untyped lambda-calculus, alpha-equivalence of beta-eta normal 
> forms is the same as observational equivalence.  Or put the other way 
> round, two normal forms which are not alpha-equivalent can be separated 
> by an observation L.

Thanks for the reference, and sorry to Ian for the confusion given by the fact
that I was thinking in types...

However, what is the notion of ‘telling apart’ here exactly?  Is it simply that
the resulting terms will have different denotations in some semantics?  My
initial (wrong) assumption about termination was due to the fact that I thought
that the ultimate test of equivalence was to be done with α-equivalence itself,
on the normal forms.

Francesco