eta abstraction
eta conversioneta conversion
<theory>
In lambda-calculus, the eta conversion rule states
\ x . f x <--> fprovided 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.
eta expansion
eta conversioneta reduction
eta conversionNearby terms:
et ♦ ET++ ♦ eta abstraction ♦ eta conversion ♦ eta expansion ♦ eta reduction
Try this search on Wikipedia, Wiktionary, Google, OneLook.
Loading
