push (old version of) q&a on fixed points

[lambda.git] / topics / week3_combinatory_logic.mdwn

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


@@ -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 ~~>