->combinatory

diff --git a/_what_is_functional.mdwn b/_what_is_functional.mdwn
index c17da57..ff9be6a 100644 (file)
--- a/_what_is_functional.mdwn
+++ b/_what_is_functional.mdwn
@@ -89,7 +89,7 @@ Scheme (imperative part)<br>
 OCaml (imperative part)</td>
 <tr>
 <td width=30%>untyped lambda calculus<br>
 OCaml (imperative part)</td>
 <tr>
 <td width=30%>untyped lambda calculus<br>

-combinatorial logic</td>
+combinatory logic</td>

 <tr>
 <td colspan=3 align=center>--------------------------------------------------- Turing complete ---------------------------------------------------</td>
 <tr>
 <tr>
 <td colspan=3 align=center>--------------------------------------------------- Turing complete ---------------------------------------------------</td>
 <tr>


@@ -191,7 +191,7 @@ Scheme (imperative part)<br>
 OCaml (imperative part)</td>
 <tr>
 <td width=30%>untyped lambda calculus<br>
 OCaml (imperative part)</td>
 <tr>
 <td width=30%>untyped lambda calculus<br>

-combinatorial logic</td>
+combinatory logic</td>

 <tr>
 <td colspan=3 align=center>--------------------------------------------------- Turing complete ---------------------------------------------------</td>
 <tr>
 <tr>
 <td colspan=3 align=center>--------------------------------------------------- Turing complete ---------------------------------------------------</td>
 <tr>

diff --git a/content.mdwn b/content.mdwn
index d725c61..aaab7a5 100644 (file)
--- a/content.mdwn
+++ b/content.mdwn
@@ -57,7 +57,7 @@ Week 3:
 
 *   More on Lists
 Introduces list comprehensions, discusses how to get the `tail` of lists in the Lambda Calculus
 
 *   More on Lists
 Introduces list comprehensions, discusses how to get the `tail` of lists in the Lambda Calculus

-*   [[Combinatorial Logic|topics/week3 combinatory logic]]
+*   [[Combinatory Logic|topics/week3 combinatory logic]]

 *   Reduction Strategies and Normal Forms
 *   Homework for week 3
 
 *   Reduction Strategies and Normal Forms
 *   Homework for week 3
 

diff --git a/exercises/assignment3.mdwn b/exercises/assignment3.mdwn
index 674cf40..9545021 100644 (file)
--- a/exercises/assignment3.mdwn
+++ b/exercises/assignment3.mdwn
@@ -40,7 +40,7 @@ where `one` abbreviates `succ zero`, and `two` abbreviates `succ (succ zero)`.
 
     You'll need to make use of the predecessor function, but it's not essential to understanding this problem that you have successfully implemented it yet. You can treat it as a black box.
 
 
     You'll need to make use of the predecessor function, but it's not essential to understanding this problem that you have successfully implemented it yet. You can treat it as a black box.
 

-## Combinatorial Logic
+## Combinatory Logic

 
 Reduce the following forms, if possible:
 
 
 Reduce the following forms, if possible:
 


@@ -53,7 +53,7 @@ Reduce the following forms, if possible:
 
 <!-- -->
 
 
 <!-- -->
 

-16. Give Combinatorial Logic combinators (that is, expressed in terms of `S`, `K`, and `I`) that behave like our boolean functions. You'll need combinators for `true`, `false`, `neg`, `and`, `or`, and `xor`.
+16. Give Combinatory Logic combinators (that is, expressed in terms of `S`, `K`, and `I`) that behave like our boolean functions. You'll need combinators for `true`, `false`, `neg`, `and`, `or`, and `xor`.

 
 Using the mapping specified in this week's notes, translate the following lambda terms into combinatory logic:
 
 
 Using the mapping specified in this week's notes, translate the following lambda terms into combinatory logic:
 

diff --git a/index.mdwn b/index.mdwn
index 5bddb85..9fd9d69 100644 (file)
--- a/index.mdwn
+++ b/index.mdwn
@@ -103,7 +103,7 @@ The [[differences between our made-up language and Scheme, OCaml, and Haskell|ro
 (**Week 3**) Thursday 12 February 2015
 > Topics:
 More on Lists (in progress);
 (**Week 3**) Thursday 12 February 2015
 > Topics:
 More on Lists (in progress);

-Combinatorial Logic (in progress);
+Combinatory Logic (in progress);

 Reduction Strategies and Normal Forms (in progress);
 Homework (in progress)
 
 Reduction Strategies and Normal Forms (in progress);
 Homework (in progress)
 

diff --git a/overview.mdwn b/overview.mdwn
index d390964..d90768a 100644 (file)
--- a/overview.mdwn
+++ b/overview.mdwn
@@ -5,7 +5,7 @@ This page aims to summarize the major "topics" (bits of conceptual technology) t
 * Basics of (especially "functional"-style) programming: including pattern matching, recursive definitions, abstract datatypes, **modularity, separating interfaces from implementation**
 * The syntax and proof theory of the untyped lambda calculus; at least some discussion of its semantics
 * Different **evaluation-order strategies** for formal systems, different "normalizing" properties
 * Basics of (especially "functional"-style) programming: including pattern matching, recursive definitions, abstract datatypes, **modularity, separating interfaces from implementation**
 * The syntax and proof theory of the untyped lambda calculus; at least some discussion of its semantics
 * Different **evaluation-order strategies** for formal systems, different "normalizing" properties

-* Combinatorial logic, or the dispensability of variables
+* Combinatory logic, or the dispensability of variables

 * Recursive definitions and recursive types, fixed-point combinators
 * Other **type sophistication**: abstract datatypes, polymorphic types, perhaps dependent types
 * **Mutation** and imperative/iterative idioms
 * Recursive definitions and recursive types, fixed-point combinators
 * Other **type sophistication**: abstract datatypes, polymorphic types, perhaps dependent types
 * **Mutation** and imperative/iterative idioms


@@ -45,7 +45,7 @@ discussing this in much more detail as the course proceeds.
 The logical systems we'll be looking at include:
 
 * the so-called "pure" or untyped (monotyped?) lambda calculus
 The logical systems we'll be looking at include:
 
 * the so-called "pure" or untyped (monotyped?) lambda calculus

-* combinatorial logic
+* combinatory logic

 * the simply-typed lambda calculus
 * polymorphic types with System F
 
 * the simply-typed lambda calculus
 * polymorphic types with System F
 

diff --git a/topics/week3_combinatory_logic.mdwn b/topics/week3_combinatory_logic.mdwn
index 761bc77..f0b28cd 100644 (file)
--- 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,
 
 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.]
 
 
 [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
 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.
 
 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
 
 Surely the most entertaining exposition is Smullyan's [[!wikipedia To_Mock_a_Mockingbird]].
 Other sources include