-> **ω** (that is, lower-case omega) is defined to be: `\x. x x`. Sometimes this combinator is called **M**. It and `W` both duplicate arguments, just in different ways. <!-- L is \uv.u(vv) -->
+> **ω** (that is, lower-case omega) is defined to be: `\x. x x`. Sometimes this combinator is called **M**. It and `W` both duplicate arguments, just in different ways. <!-- L is \hu.h(uu) -->
3. [(XY)] = ([X][Y])
Wait, what is that `@a ...` business? Well, that's another operation on (a variable and) a CL expression, that we can define like this:
3. [(XY)] = ([X][Y])
Wait, what is that `@a ...` business? Well, that's another operation on (a variable and) a CL expression, that we can define like this:
-Think of `@aX` as a pseudo-lambda abstract. (Hankin and Barendregt write it as <code>λ*a. X</code>; Hindley &anp; Seldin write it as `[a] X`.) It is possible to omit line 6, and some presentations do, but Hindley & Seldin observe that this "enormously increases" the length of "most" translations.
+Think of `@aX` as a pseudo-lambda abstract. (Hankin and Barendregt write it as <code>λ*a. X</code>; Hindley & Seldin write it as `[a] X`.) It is possible to omit line 6, and some presentations do, but Hindley & Seldin observe that this "enormously increases" the length of "most" translations.
Let's see the translation rules in action. We'll start by translating
the combinator we use to represent false:
Let's see the translation rules in action. We'll start by translating
the combinator we use to represent false:
to establish that combinators can reverse order, so we set out to
translate the **T** combinator (`\x y. y x`):
to establish that combinators can reverse order, so we set out to
translate the **T** combinator (`\x y. y x`):
By now, you should realize that all rules (1) through (3) do is sweep
through the lambda term turning lambdas into @'s.
We can test this translation by seeing if it behaves like the original lambda term does.
By now, you should realize that all rules (1) through (3) do is sweep
through the lambda term turning lambdas into @'s.
We can test this translation by seeing if it behaves like the original lambda term does.