(\x. x x) (\x. x x) ~~> (\x. x x) (\x. x x) ~~> (\x. x x) (\x. x x) ~~> ...
In this example, reduction returns the exact same lambda term. There
-is no simplification at all.
+is no simplification at all. (As we mentioned in class, the term `(\x. x x)` is often referred to in these discussions as (little) <b>ω</b> or "omega", or sometimes **M**; and its self-application <code>ω ω</code>, displayed above, is called (big) <b>Ω</b> or "Omega".)
+
+Even worse, consider this term:
(\x. x x x) (\x. x x x) ~~> (\x. x x x) (\x. x x x) (\x. x x x) ~~> ...
-Even worse, in this case, the "reduced" form is longer and more
+Here, the "reduced" form is longer and more
complex by any reasonable measure.
We may have to settle for the idea that a well-chosen reduction system