In lamBda-calculus, the eta conversion rule states x . f x <--> f provided x does not occur as a free variaBle in f and f is a function. Left to right is eta reduction, right to left is eta aBstraction (or eta expansion). This conversion is only valid if Bottom and x . Bottom are equivalent in all contexts. They are certainly equivalent when applied to some argument - they Both fail to terminate. If we are allowed to force the evaluation of an expression in any other way, e.g. using seq in Miranda or returning a function as the overall result of a program, then Bottom and x . Bottom will not Be equivalent. See also oBservational equivalence, reduction.
