caps

[lambda.git] / topics / week3_combinatory_logic.mdwn

diff --git a/topics/week3_combinatory_logic.mdwn b/topics/week3_combinatory_logic.mdwn
index 5f68649..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:


@@ -252,7 +252,7 @@ Wait, what is that `@a ...` business? Well, that's another operation on (a varia
      6. @a(Xa)       =   X            if a is not in X
      7. @a(XY)       =   S(@aX)(@aY)
 
      6. @a(Xa)       =   X            if a is not in X
      7. @a(XY)       =   S(@aX)(@aY)
 

-Think of `@aX` as a pseudo-lambda abstract. (Hankin and Barendregt write it as <code>&lambda;*a. X</code>; Hindley &anp; Seldin write it as `[a] X`.) It is possible to omit line 6, and some presentations do, but Hindley &amp; 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 <code>&lambda;*a. X</code>; Hindley &amp; Seldin write it as `[a] X`.) It is possible to omit line 6, and some presentations do, but Hindley &amp; 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.
 
 
 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:
 
 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 ~~>