eta conversion
eta abstraction
eta expansion
eta reduction

    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.