Search in: Word
Vietnamese keyboard: Off
Virtual keyboard: Show
Computing (FOLDOC) dictionary
eta conversion
Jump to user comments
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.