At Fri, 03 May 2013 16:34:28 +0200, Andreas Abel wrote: > The answer to your question is given in Boehm's theorem, and the answer > is "no", as you suspect. > > For the untyped lambda-calculus, alpha-equivalence of beta-eta normal > forms is the same as observational equivalence. Or put the other way > round, two normal forms which are not alpha-equivalent can be separated > by an observation L.
Thanks for the reference, and sorry to Ian for the confusion given by the fact that I was thinking in types... However, what is the notion of ‘telling apart’ here exactly? Is it simply that the resulting terms will have different denotations in some semantics? My initial (wrong) assumption about termination was due to the fact that I thought that the ultimate test of equivalence was to be done with α-equivalence itself, on the normal forms. Francesco _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
