|
|
The eta rewrite rule |
An eta conversion lifts certain function calls out of a lambda convolute |
|
(lambda(x) (e x)) <=> e provided that x is not free in the expression e |
Legal conversion: |
| An example of an eta rewriting. |
Illegal conversion: |
| An example of an illegal eta conversion. The eta conversion rule says in general how 'e' is lifted out of the
lambda expressions. In this example, e corresponds to the emphasized inner lambda expression (which is blue on a color medium.) However,
x is a free name in the inner lambda expression, and therefore the application of the eta rewrite rule
is illegal. |