X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2Fweek3_combinatory_logic.mdwn;h=60cb3da16b757ec3015637401a81a3db6120fa96;hp=5e842ebdd9c71e8289789d28d561cb24989e247f;hb=a4d2693effe839524592f4427465ff8d97625302;hpb=e8fef07715c72bf4fc4995aacdea55f2552ed165

diff --git a/topics/week3_combinatory_logic.mdwn b/topics/week3_combinatory_logic.mdwn
index 5e842ebd..60cb3da1 100644
--- a/topics/week3_combinatory_logic.mdwn
+++ b/topics/week3_combinatory_logic.mdwn
@@ -36,7 +36,7 @@ over the first two arguments.
 
 >   **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
@@ -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 ~~>