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