Lecture overview -- Keyboard shortcut: 'u'  Previous page: The beta rewrite rule -- Keyboard shortcut: 'p'  Next page: Normal forms -- Keyboard shortcut: 'n'  Lecture notes - all slides together  Annotated slide -- Keyboard shortcut: 't'  Alphabetic index  Help page about these notes  Course home    Evaluation Order and Infinite Lists - slide 12 : 27

The eta rewrite rule
An eta conversion lifts certain functions out of a "redundant lambda convolute"

A function f, which only passes its parameters on to another function e, can be substituted by e

(lambda(x) (e x)) <=> e   provided that x is not free in the expression e
Legal conversion:
Expression

 Converted Expression

(lambda (x) (square x))
 
square
(lambda (x) ((lambda(y) (* y y)) x))
 
(lambda(y) (* y y))
Illegal conversion:
Expression

 Converted Expression

(lambda(x) ((lambda(y) (f x y)) x))
 
(lambda(y) (f x y))