-Combinators and Combinatorial Logic
-===================================
+Combinators and Combinatory Logic
+=================================
Combinatory logic is of interest here in part because it provides a
useful computational system that is equivalent to the lambda calculus,
[Fussy notes: if the original lambda term has free variables in it, so will the combinatory logic translation. Feel free to worry about this, though you should be confident that it makes sense. You should also convince 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). One other detail: this translation algorithm builds expressions that combine lambdas with 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 mixes combinators 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 combinatorial
+[Various, slightly differing translation schemes from combinatory
logic to the lambda calculus are also possible. These generate
different metatheoretical correspondences between the two
calculii. Consult Hindley and Seldin for details. Also, note that the
schemas for the combinators. Thsi will become more clear once we have
a theory of types in view.
-Here's more to read about combinatorial logic.
+Here's more to read about combinatory logic.
Surely the most entertaining exposition is Smullyan's [[!wikipedia To_Mock_a_Mockingbird]].
Other sources include