typos

[lambda.git] / topics / week3_combinatory_logic.mdwn

diff --git a/topics/week3_combinatory_logic.mdwn b/topics/week3_combinatory_logic.mdwn
index 5e842eb..60cb3da 100644 (file)
--- 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 -->
 
 
 >   **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
 
 
 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
 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 ~~>