-
-Now for termination:
-
-<pre>
-(\x.w)((\x.xxx)(\x.xxx))
- | \
- | (\x.w)((\x.xxx)(\x.xxx)(\x.xxx))
- | / \
- | / (\x.w)((\x.xxx)(\x.xxx)(\x.xxx)(\x.xxx))
- | / / \
- .----------------- etc.
- |
- w
-</pre>
-
-Here we have a function that discards its argument on the left, and a
-non-terminating term on the right. It's even more evil than Omega,
-because it not only never reduces, it generates more and more work
-with each so-called reduction. If we unluckily adopt the "always
-reduce the rightmost reducible lambda" strategy, we'll spend our days
-relentlessly copying out new copies of \x.xxx. But if we even once
-reduce the leftmost reducible lambda, we'll immediately jump to the
-normal form, `w`.
-
-We can roughly associate the "leftmost always" strategy with call by
-name (normal order), and the "rightmost always" strategy with call by
-value (applicative order). There are fine-grained distinctions among
-these terms of art that we will not pause to untangle here.
-
-If a term has a normal form (a reduction such that no further
-reduction is possible), then a leftmost-always reduction will find it.
-(That's why it's called "normal order": it's the evaluation order that
-guarantees finding a normal form if one exists.)
-
-Preview: if the evaluation of a function has side effects, then the
-choice of an evaluation strategy will make a big difference in which
-side effect occur and in which order.