[Haskell-cafe] Lambda Calculus question on equivalence

[Jon Fairbairn]

Francesco Mazzoli <f at mazzo.li> writes:

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

α-equivalence on the Böhm trees — normal forms extended to
infinity. I suppose that counts as “some semantics” but its very
direct.

-- 
Jón Fairbairn                                 Jon.Fairbairn at cl.cam.ac.uk