X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week2.mdwn;h=8de3aab92723df4b58f55c96613be9319b57ead4;hp=54a5ebdfb455d49c969097db4bb695783eb37abc;hb=d2fa64a9e75f27c2d8fdaeae2f25eb29da82e760;hpb=ec88fb91f1b5d87fe9d4636d7a0b29bda7146142

diff --git a/week2.mdwn b/week2.mdwn
index 54a5ebdf..8de3aab9 100644
--- a/week2.mdwn
+++ b/week2.mdwn
@@ -60,7 +60,49 @@ duplicators.
 
 ![test](http://lambda.jimpryor.net/szabolcsi-reflexive.jpg)
 
-![Szabolcsi's analysis of *himself* as the duplicator combinator](szabolcsi-reflexive.jpg)
+Notice that the semantic value of *himself* is exactly W.
+The reflexive pronoun in direct object position combines first with the transitive verb (through compositional magic we won't go into here).  The result is an intransitive verb phrase that takes a subject argument, duplicates that argument, and feeds the two copies to the transitive verb meaning.  
+
+Note that W = S(CI):
+
+      S(CI) = 
+      S((\fxy.fyx)(\x.x)) =
+      S(\xy.(\x.x)yx) =
+      (\fgx.fx(gx))(\xy.yx) =
+      \gx.[\xy.yx]x(gx) =
+      \gx.(gx)x =
+      W
+
+Ok, here comes a shift in thinking.  Instead of defining combinators as equivalent to certain lambda terms,
+we can define combinators by what they do.  If we have the I combinator followed by any expression X, 
+I will take that expression as its argument and return that same expression as the result.  In pictures,
+
+    IX ~~> X
+
+Thinking of this as a reduction rule, we can perform the following computation
+
+    II(IX) ~~> IIX ~~> IX ~~> X
+
+The reduction rule for K is also straigtforward:
+
+    KXY ~~> X
+
+That is, K throws away its second argument.  The reduction rule for S can be constructed by examining 
+the defining lambda term:
+
+    S = \fgx.fx(gx)
+
+S takes three arguments, duplicates the third argument, and feeds one copy to the first argument and the second copy to the second argument.  So:
+
+    SFGX ~~> FX(GX)
+
+If the meaning of a function is nothing more than how it behaves with respect to its arguments, 
+these reduction rules capture the behavior of the combinators S,K, and I completely.
+We can use these rules to compute without resorting to beta reduction.  For instance, we can show how the I combinator is equivalent to a certain crafty combination of S's and K's:
+
+    SKKX ~~> KX(KX) ~~> X
+
+So the combinator SKK is equivalent to the combinator I.
 
 
 These systems are Turing complete. In other words: every computation we know how to describe can be represented in a logical system consisting of only a single primitive operation!