@@ -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