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