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

diff --git a/topics/week3_combinatory_logic.mdwn b/topics/week3_combinatory_logic.mdwn
index d54f9f86..c15424f9 100644
--- a/topics/week3_combinatory_logic.mdwn
+++ b/topics/week3_combinatory_logic.mdwn
@@ -220,6 +220,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 +248,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