On 05/02/2013 10:42 PM, Francesco Mazzoli wrote:
At Thu, 02 May 2013 20:47:07 +0100,
Ian Price wrote:
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.
Yes, they can. Take ‘f = λ x : ℕ → x + x’ and ‘g = λ x : ℕ → 2 * x’.
Those are not lambda terms.
Furthermore, if those terms are rewritten to operate on church numerals,
they have the same unique normal form, namely λλλ 3 2 (3 2 1).
These terms are not ‘definitionally’ equal (which could be the α-equivalence
you cite
but can be extended to fancier checks on the term structure). However, for all
(well typed) inputs the result of those two functions are the same: they are
‘extensionally’ equal [1]. The first part (...(L A) is equivalent to (L B)...)
holds: the same function will always produce the same output given
definitionally equal arguments.
...
(I guess the question is about untyped lambda calculus.)
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
