X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2Fweek3_combinatory_logic.mdwn;h=0ddb4469254d3c4faeae7ce1cb02d249eac0c2a8;hp=d54f9f86525724d1501cde9c7097cc9a0c950702;hb=82981fcd3e99f6f2927c2a958340800fbd842d9c;hpb=39db6d0abfc0f9606c1b38b3b21b4232cad3a6e2

diff --git a/topics/week3_combinatory_logic.mdwn b/topics/week3_combinatory_logic.mdwn
index d54f9f86..0ddb4469 100644
--- a/topics/week3_combinatory_logic.mdwn
+++ b/topics/week3_combinatory_logic.mdwn
@@ -175,6 +175,17 @@ used to establish a correspondence between two natural language grammars, one
 of which is based on lambda-like abstraction, the other of which is based on
 Combinatory Logic-like manipulations.
 
+[WARNING: the mapping from the lambda calculus to Combinatory Logic
+has been changed since the class in which it was presented.  It now
+matches the presentation in Barendregt.  The revised version is
+cleaner, and more elegant.  If you spent a lot of time working to
+understand the original version, there's good news and bad news.  The
+bad news is that things have changed.  The good news is that the new
+version described the same mapping as before, but does it in a cleaner
+way.  That is, the CL term that a given lambda term maps onto hasn't
+changed, only the details of how that CL term gets computed.  Sorry if
+the changeup causes any distress!]
+
 In order to establish the correspondence, we need to get a bit more
 official about what counts as an expression in CL.  We'll endow CL
 with an infinite stock of variable symbols, just like the lambda
@@ -220,6 +231,9 @@ temporary psuedo-lambda built from `@` and the original variable.
 Rule (3) says that the translation of an application of `X` to `Y` is
 the application of the transtlation of `X` to the translation of `Y`.
 
+As we'll see, the first three rules sweep through the lambda term,
+changing each lambda to an @.
+
 Rules (4) through (6) tell us how to eliminate all the `@`'s.
 
 In rule (4), if we have `@aa`, we need a CL expression that behaves
@@ -245,8 +259,6 @@ Persuade yourself that if the original lambda term contains no free
 variables --- i.e., is a combinator --- then the translation will
 consist only of `S`, `K`, and `I` (plus parentheses).
 
-(Fussy note: this translation algorithm builds intermediate expressions that combine lambdas with primitive combinators.  For instance, the translation of our boolean `false` (`\x y. y`) is `[\x [\y. y]] = [\x. I] = KI`.  In the intermediate stage, we have `\x. I`, which has a combinator in the body of a lambda abstract.  It's possible to avoid this if you want to,  but it takes some careful thought.  See, e.g., Barendregt 1984, page 156.)
-
 Various, slightly differing translation schemes from Combinatory Logic to the
 Lambda Calculus are also possible. These generate different metatheoretical
 correspondences between the two calculi. Consult Hindley and Seldin for