> **W** is defined to be: `\f x . f x x`. (So `W f` accepts one argument and gives it to `f` twice. What is the meaning of `W multiply`?) <!-- \x. multiply x x ≡ \x. square x -->
-> **ω** (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) -->
It's possible to build a logical system equally powerful as the Lambda
Logic term. Then we define the [.] mapping as follows.
1. [a] = a
- 2. [\aX] = @a[X]
+ 2. [(\aX)] = @a[X]
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:
6. @a(Xa) = X if a is not in X
7. @a(XY) = S(@aX)(@aY)
-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.
It's easy to understand these rules based on what `S`, `K` and `I` do.
Let's see the translation rules in action. We'll start by translating
the combinator we use to represent false:
- [\t\ff]
- == @t[\ff] rule 2
- == @t(@ff) rule 2
- == @tI rule 4
- == KI rule 5
+ [\y (\n n)]
+ == @y [\n n] rule 2
+ == @y (@n n) rule 2
+ == @y I rule 4
+ == KI rule 5
Let's check that the translation of the `false` boolean behaves as expected by feeding it two arbitrary arguments:
to establish that combinators can reverse order, so we set out to
translate the **T** combinator (`\x y. y x`):
- [\x\y(yx)]
- == @x[\y(yx)]
- == @x(@y[(yx)])
- == @x(@y([y][x]))
- == @x(@y(yx))
- == @x(S(@yy)(@yx))
- == @x(SI(@yx))
- == @x(SI(Kx))
- == S (@x(SI)) (@x(Kx))
- == S (K(SI)) (S (@xK) (@xx))
- == S (K(SI)) (S (KK) I)
+ [\x(\y(yx))]
+ == @x[\y(yx)]
+ == @x(@y[yx])
+ == @x(@y([y][x]))
+ == @x(@y(yx))
+ == @x(S(@yy)(@yx))
+ == @x(S I (@yx))
+ == @x(S I (Kx))
+ == S(@x(SI))(@x(Kx))
+ == S (K(SI))(S(@xK)(@xx))
+ == S (K(SI))(S (KK) I)
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.
-The orginal lambda term lifts its first argument (think of it as reversing the order of its two arguments):
+The original lambda term "lifts" its first argument `x`, in the sense of wrapping it into a "one-tuple" or a package that accepts an operation `y` as a further argument, and then applies `y` to `x`. (Or just think of **T** as reversing the order of its two arguments.)
S (K(SI)) (S(KK)I) X Y ~~>
(K(SI))X ((S(KK)I) X) Y ~~>