`λ*a. X`

; 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 `λ*a. X`

; 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.
@@ -318,11 +318,11 @@ requires adding explicit axioms.
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:
@@ -334,23 +334,23 @@ Here's a more elaborate example of the translation. Let's say we want
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 ~~>