From: Chris Date: Mon, 16 Feb 2015 21:19:29 +0000 (-0500) Subject: adjust X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=6f90fa9381988785d23d45beae679a7acfd3aefa adjust --- 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