Francesco Mazzoli <f...@mazzo.li> writes: > 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.
α-equivalence on the Böhm trees — normal forms extended to infinity. I suppose that counts as “some semantics” but its very direct. -- Jón Fairbairn jon.fairba...@cl.cam.ac.uk _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
