author jim Wed, 18 Feb 2015 04:18:26 +0000 (23:18 -0500) committer Linux User Wed, 18 Feb 2015 04:18:26 +0000 (23:18 -0500)

index 5e842eb..5d8d9db 100644 (file)
@@ -242,7 +242,7 @@ Let's say that for any lambda term T, [T] is the equivalent Combinatory
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:
@@ -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 ~~>