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