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