from
The Free On-line Dictionary of Computing (8 July 2008)
eta conversion
eta abstraction
eta expansion
eta reduction
<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}.