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’. 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. You stumbled upon a subject that generated a great deal of research in the field of type theory [2]. There are various developments focusing on having a ‘better’ equality that identifies more things are equal. Your intuition of ‘observationally’ equal will probably be close to the notion of isomorphism between two sets, and in fact one of the more exciting developments right now concerns a type theory where equality is based on isomorphism [3]—however the computational ‘details’ haven’t been worked out yet :). There are other attempts [4] that fix the instance above (function extensionality) but don’t quite go all the way (not without reasons, since the isomorphism business has far reaching consequences that could be seen as impractical). Francesco [1]: https://en.wikipedia.org/wiki/Extensionality [2]: https://en.wikipedia.org/wiki/Intuitionistic_type_theory#Extensional_versus_... [3]: https://en.wikipedia.org/wiki/Homotopy_type_theory [4]: http://www.cs.nott.ac.uk/~txa/publ/obseqnow.pdf