[Haskell-cafe] Lambda Calculus question on equivalence

[Ian Price]

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"