X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2Fweek3_combinatory_logic.mdwn;h=60cb3da16b757ec3015637401a81a3db6120fa96;hp=5f68649927cee76e67219035d0671f22aee601c3;hb=5c234a526ad9ecc96ae9d17b6f74de53a0354444;hpb=c9c1e5ed5107559f98721ae87f0a9f5ef1e4413f 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 ~~>