> I thought this inequality was one of the distinguishing characteristics of
> lazy functional programming relative to the standard lambda-calculus. To
> quote from Abramsky's contribution to "Research Topics in Functional
> Programming", Addison-Wesley 1990:
>
> Let O == (\x.xx)(\x.xx) be the standard unsolvable term. Then
>
> \x.O = O
>
> in the standard theory, since \x.O is also unsolvable; but \x.O is in
> weak head normal form and hence should be distinguished from O in our
> "lazy" theory.
Yes, internally \x.O != O, but since the only thing you can
do with a function is to apply it these two are observationally
equivalent. Adding seq (or strict constructors) would constitute
another way of using function (checking for _|_) and would
thus distinguish them.
I think this is all right, but it makes eta conversion invalid.
-- Lennart
