[Haskell-cafe] Lambda Calculus question on equivalence

Francesco Mazzoli f at mazzo.li
Thu May 2 22:42:54 CEST 2013


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_intensional
[3]: https://en.wikipedia.org/wiki/Homotopy_type_theory
[4]: http://www.cs.nott.ac.uk/~txa/publ/obseqnow.pdf



More information about the Haskell-Cafe mailing list