[Haskell-cafe] Lambda Calculus question on equivalence

[Andreas Abel]

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.

Cheers,
Andreas

On 03.05.2013 00:33, Roman Cheplyaka wrote:
> IIRC, Barendregt'84 monography ("The Lambda Calculus: Its Syntax and
> Semantics") has a significant part of it devoted to this question.
>
> * Ian Price <ianprice90 at googlemail.com> [2013-05-02 20:47:07+0100]
>> Hi,
>>
>> I know this isn't perhaps the best forum for this, but maybe you can
>> give me some pointers.
>>
>> Earlier today I was thinking about De Bruijn Indices, and they have the
>> property that two lambda terms that are alpha-equivalent, are expressed
>> in the same way, and I got to wondering if it was possible to find a
>> useful notion of function equality, such that it would be equivalent to
>> structural equality (aside from just defining it this way), though
>> obviously we cannot do this in general.
>>
>> So the question I came up with was:
>>
>> Can two normalised (i.e. no subterm can be beta or eta reduced) lambda
>> terms be "observationally equivalent", but not alpha equivalent?
>>
>> By observationally equivalent, I mean A and B are observationally
>> equivalent if for all lambda terms L: (L A) is equivalent to (L B) and
>> (A L) is equivalent to (B L). The definition is admittedly circular, but
>> I hope it conveys enough to understand what I'm after.
>>
>> My intuition is no, but I am not sure how to prove it, and it seems to
>> me this sort of question has likely been answered before.
>>
>> Cheers
>> --
>> Ian Price -- shift-reset.com
>>
>> "Programming is like pinball. The reward for doing it well is
>> the opportunity to do it again" - from "The Wizardy Compiled"
>>
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/