eta conversion

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