adjust

[lambda.git] / topics / week3_combinatory_logic.mdwn

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