By Letter: Non-alphabet | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z
  Email this page to a friend


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.





< Previous Terms Terms Containing eta conversion Next Terms >
EstPC
ET
et
ET++
eta abstraction
beta
beta abstraction
beta reduction
eta abstraction
eta conversion
eta expansion
eta reduction
ETB
ETC
e-text


Web Standards & Support:

Link to and support eLook.org Powered by LoadedWeb Web Hosting
Valid XHTML 1.0!Valid CSS!eLook.org FireFox Extensions