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.
Nearby terms:
et « ET++ « eta abstraction « eta conversion
» eta expansion » eta reduction » ETB
|
