X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?a=blobdiff_plain;f=topics%2Fweek3_combinatory_logic.mdwn;h=60cb3da16b757ec3015637401a81a3db6120fa96;hb=7acee0fbdbcefcac2ebf8e27e8b0312767dc575e;hp=5f68649927cee76e67219035d0671f22aee601c3;hpb=c9c1e5ed5107559f98721ae87f0a9f5ef1e4413f;p=lambda.git
diff --git a/topics/week3_combinatory_logic.mdwn b/topics/week3_combinatory_logic.mdwn
index 5f686499..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`?)
-> **Ï** (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.
+> **Ï** (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.
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:
@@ -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)
-Think of `@aX` as a pseudo-lambda abstract. (Hankin and Barendregt write it as λ*a. X
; Hindley &anp; Seldin write it as `[a] X`.) It is possible to omit line 6, and some presentations do, but Hindley & 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 λ*a. X
; Hindley & Seldin write it as `[a] X`.) It is possible to omit line 6, and some presentations do, but Hindley & 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.
@@ -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 ~~>