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.
