<pre>
((\x.x)((\y.y) z))
/ \
- / \
+ / \
/ \
/ \
((\y.y) z) ((\x.x) z)
first and then head east, you end up in the same place as if you walk
east and then head uptown.
-But which lambda you target has implications for efficiency and for
+But which lambda you target has implications for efficiency and for
termination. (Later in the course, it will have implications for
the order in which side effects occur.)
\ /
\ /
\ /
- w
-</pre>
+ w
+</pre>
If a function discards its argument (as `\x.w` does), it makes sense
to target that function for reduction, rather than wasting effort
(((\y.y) z)((\y.y) z) ((\x.xx) z)
/ | /
/ (((\y.y)z)z) /
- / | /
+ / | /
/ | /
/ | /
- (z ((\y.y)z)) | /
+ (z ((\y.y)z)) | /
\ | /
-----------.---------
|
If we reduce the rightmost lambda first (rightmost branch of the
diagram), the argument is already simplified before we do the
copying. We arrive at the normal form (i.e., the form that cannot be
-further reduced) in two steps.
+further reduced) in two steps.
But if we reduce the rightmost lambda first (the two leftmost branches
of the diagram), we copy the argument before it has been evaluated.