[Haskell-cafe] Lambda Calculus question on equivalence

[Timon Gehr]

On 05/02/2013 10:42 PM, Francesco Mazzoli wrote:
> At Thu, 02 May 2013 20:47:07 +0100,
> Ian Price wrote:
>> 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.
>
> Yes, they can.  Take ‘f = λ x : ℕ → x + x’ and ‘g = λ x : ℕ → 2 * x’.

Those are not lambda terms.
Furthermore, if those terms are rewritten to operate on church numerals, 
they have the same unique normal form, namely λλλ 3 2 (3 2 1).

> These terms are not ‘definitionally’ equal (which could be the α-equivalence you cite
> but can be extended to fancier checks on the term structure).  However, for all
> (well typed)  inputs the result of those two functions are the same: they are
> ‘extensionally’ equal [1].  The first part (...(L A) is equivalent to (L B)...)
> holds: the same function will always produce the same output given
> definitionally equal arguments.
> ...

(I guess the question is about untyped lambda calculus.)