The notion of equivalence you are talking about (normally L is referred to as a "context") is 'extensional equality'; that is, functions f and g are equal if forall x, f x = g x. It's pretty easy to give a pair of functions which are not alpha equivalent but are observationally equivalent: if collatz_conjecture then true else bottom true / bottom (Depending on whether or not you think the collatz conjecture is true...) Cheers, Edward Excerpts from Ian Price's message of Thu May 02 12:47:07 -0700 2013:
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