typo

[lambda.git] / topics / week3_combinatory_logic.mdwn

diff --git a/topics/week3_combinatory_logic.mdwn b/topics/week3_combinatory_logic.mdwn
index d54f9f8..0ddb446 100644 (file)
--- 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.
 
 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
 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`.
 
 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
 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).
 
 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
 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