Y> 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.