[Haskell-cafe] Lambda Calculus question on equivalence

[Roman Cheplyaka]

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

* Ian Price <ianprice90 at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe