Francesco Mazzoli
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.Fairbairn@cl.cam.ac.uk