X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2Fweek3_combinatory_logic.mdwn;fp=topics%2Fweek3_combinatory_logic.mdwn;h=f0b28cd7d9e394ee84229f0a0b8a8d2ffbd623fb;hp=761bc775e387213110ccc5fa258bc54060d361f5;hb=ee79965dbd07b39cd3ab7d489ba87b8cc5e2b68b;hpb=8d11f56b4dd370271a919f2cc037c399851d4bc8

diff --git a/topics/week3_combinatory_logic.mdwn b/topics/week3_combinatory_logic.mdwn
index 761bc775..f0b28cd7 100644
--- a/topics/week3_combinatory_logic.mdwn
+++ b/topics/week3_combinatory_logic.mdwn
@@ -1,5 +1,5 @@
-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,
@@ -173,7 +173,7 @@ The fifth rule deals with an abstract whose body is an application: the S combin
 
 [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
@@ -271,7 +271,7 @@ and the S and K combinators is that the axioms correspond to type
 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