further refinements

diff --git a/topics/week3_combinatory_logic.mdwn b/topics/week3_combinatory_logic.mdwn
index 5e842eb..5d8d9db 100644 (file)
--- a/topics/week3_combinatory_logic.mdwn
+++ b/topics/week3_combinatory_logic.mdwn
@@ -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
 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:
      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:
 
 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:
 
    
 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`):
 
 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.
 
 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 ~~>
 
     S (K(SI)) (S(KK)I) X Y ~~>
     (K(SI))X ((S(KK)I) X) Y ~~>