資料來源 : Free On-Line Dictionary of Computing

eta conversion
     
         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}.