[Haskell-cafe] Lambda Calculus question on equivalence

Edward Z. Yang ezyang at MIT.EDU
Thu May 2 22:11:17 CEST 2013


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



More information about the Haskell-Cafe mailing list