IIRC, Barendregt'84 monography ("The Lambda Calculus: Its Syntax and Semantics") has a significant part of it devoted to this question.

* Ian Price <ianpric...@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@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe