moved file live

diff --git a/topics/_week3_combinatory_logic.mdwn b/topics/week3_combinatory_logic.mdwn
similarity index 87%
rename from topics/_week3_combinatory_logic.mdwn
rename to topics/week3_combinatory_logic.mdwn
index 5a17657..5981127 100644 (file)
--- a/topics/_week3_combinatory_logic.mdwn
+++ b/topics/week3_combinatory_logic.mdwn
@@ -1,6 +1,15 @@
 Combinators and Combinatorial Logic
 ===================================
 
 Combinators and Combinatorial Logic
 ===================================
 

+Combinatory logic is of interest here in part because it provides a
+useful computational system that is equivalent to the lambda calculus,
+but different from it.  In addition, Combinatory Logic has a number of
+applications in natural language semantics.  Exploring Combinatory
+Logic will involve defining a difference notion of reduction from the
+one we have been using for the lambda calculus.  This will provide us
+with a second parallel example later when we're thinking through
+such topics as evaluation strategies and recursion.
+

 Lambda expressions that have no free variables are known as **combinators**. Here are some common ones:
 
 >      **I** is defined to be `\x x`
 Lambda expressions that have no free variables are known as **combinators**. Here are some common ones:
 
 >      **I** is defined to be `\x x`


@@ -68,6 +77,8 @@ S(\xy.yx) ≡
 \gx.(gx)x ≡
 W</code></pre>
 
 \gx.(gx)x &equiv;
 W</code></pre>
 

+###A different set of reduction rules###
+

 Ok, here comes a shift in thinking.  Instead of defining combinators as equivalent to certain lambda terms,
 we can define combinators by what they do.  If we have the I combinator followed by any expression X, 
 I will take that expression as its argument and return that same expression as the result.  In pictures,
 Ok, here comes a shift in thinking.  Instead of defining combinators as equivalent to certain lambda terms,
 we can define combinators by what they do.  If we have the I combinator followed by any expression X, 
 I will take that expression as its argument and return that same expression as the result.  In pictures,


@@ -107,7 +118,7 @@ Logic as beta reduction and eta reduction, etc., have with respect to
 the lambda calculus: they are purely syntactic rules for transforming
 one sequence of symbols (e.g., a redex) into another (a reduced
 form).  It's worth noting that the reduction rules for Combinatory
 the lambda calculus: they are purely syntactic rules for transforming
 one sequence of symbols (e.g., a redex) into another (a reduced
 form).  It's worth noting that the reduction rules for Combinatory

-Logic are considerably more simple than, say, beta reduction.  Since
+Logic are considerably more simple than, say, beta reduction.  Also, since

 there are no variables in Combiantory Logic, there is no need to worry
 about variable collision.  
 
 there are no variables in Combiantory Logic, there is no need to worry
 about variable collision.  
 


@@ -148,7 +159,7 @@ Assume that for any lambda term T, [T] is the equivalent combinatory logic term.
      1. [a]               a
      2. [(M N)]           ([M][N])
      3. [\a.a]            I
      1. [a]               a
      2. [(M N)]           ([M][N])
      3. [\a.a]            I

-     4. [\a.M]            KM                 assumption: a does not occur free in M
+     4. [\a.M]            K[M]                 assumption: a does not occur free in M

      5. [\a.(M N)]        S[\a.M][\a.N]
      6. [\a\b.M]          [\a[\b.M]]
 
      5. [\a.(M N)]        S[\a.M][\a.N]
      6. [\a\b.M]          [\a[\b.M]]
 


@@ -217,12 +228,14 @@ A philosophical connection: Quine went through a phase in which he developed a v
   Quine, Willard. 1960. "Variables explained away" <cite>Proceedings of the American Philosophical Society</cite>.  Volume 104: 343--347.  Also in W. V. Quine.  1960. <cite>Selected Logical Papers</cite>.  Random House: New
   York.  227--235.
 
   Quine, Willard. 1960. "Variables explained away" <cite>Proceedings of the American Philosophical Society</cite>.  Volume 104: 343--347.  Also in W. V. Quine.  1960. <cite>Selected Logical Papers</cite>.  Random House: New
   York.  227--235.
 

-The reason this was important to Quine is similar to the worries that Jim was talking about
-in the first class in which using non-referring expressions such as Santa Claus might commit 
-one to believing in non-existant things.  Quine's slogan was that "to be is to be the value of a variable."
-What this was supposed to mean is that if and only if an object could serve as the value of some variable, we 
-are committed to recognizing the existence of that object in our ontology.
-Obviously, if there ARE no variables, this slogan has to be rethought.
+The reason this was important to Quine is similar to the worry that
+using non-referring expressions such as Santa Claus might commit one
+to believing in non-existant things.  Quine's slogan was that "to be
+is to be the value of a variable."  What this was supposed to mean is
+that if and only if an object could serve as the value of some
+variable, we are committed to recognizing the existence of that object
+in our ontology.  Obviously, if there ARE no variables, this slogan
+has to be rethought.

 
 Quine did not appear to appreciate that Shoenfinkel had already invented combinatory logic, though
 he later wrote an introduction to Shoenfinkel's key paper reprinted in Jean
 
 Quine did not appear to appreciate that Shoenfinkel had already invented combinatory logic, though
 he later wrote an introduction to Shoenfinkel's key paper reprinted in Jean


@@ -232,7 +245,7 @@ Cresswell has also developed a variable-free approach of some philosophical and
 in two books in the 1990's.
 
 A final linguistic application: Steedman's Combinatory Categorial Grammar, where the "Combinatory" is 
 in two books in the 1990's.
 
 A final linguistic application: Steedman's Combinatory Categorial Grammar, where the "Combinatory" is 

-from combinatory logic (see especially his 2000 book, <cite>The Syntactic Processs</cite>).  Steedman attempts to build
+from combinatory logic (see especially his 2012 book, <cite>Taking Scope</cite>).  Steedman attempts to build

 a syntax/semantics interface using a small number of combinators, including T &equiv; `\xy.yx`, B &equiv; `\fxy.f(xy)`,
 and our friend S.  Steedman used Smullyan's fanciful bird 
 names for the combinators, Thrush, Bluebird, and Starling.
 a syntax/semantics interface using a small number of combinators, including T &equiv; `\xy.yx`, B &equiv; `\fxy.f(xy)`,
 and our friend S.  Steedman used Smullyan's fanciful bird 
 names for the combinators, Thrush, Bluebird, and Starling.


@@ -240,6 +253,23 @@ names for the combinators, Thrush, Bluebird, and Starling.
 Many of these combinatory logics, in particular, the SKI system, 
 are Turing complete. In other words: every computation we know how to describe can be represented in a logical system consisting of only a single primitive operation!
 
 Many of these combinatory logics, in particular, the SKI system, 
 are Turing complete. In other words: every computation we know how to describe can be represented in a logical system consisting of only a single primitive operation!
 

+The combinators K and S correspond to two well-known axioms of sentential logic:
+
+###A connection between Combinatory Logic and logic logic###
+
+One way of getting a feel for the power of the SK basis is to note
+that the following two axioms
+
+    AK: A --> (B --> A)
+    AS: (A --> (B --> C)) --> ((A --> B) --> (A --> C))
+
+when combined with modus ponens (from `A` and `A --> B`, conclude `B`)
+are complete for the implicational fragment of intuitionistic logic.
+The way we'll favor for viewing the relationship between these axioms
+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.
 Surely the most entertaining exposition is Smullyan's [[!wikipedia To_Mock_a_Mockingbird]].
 Other sources include
 Here's more to read about combinatorial logic.
 Surely the most entertaining exposition is Smullyan's [[!wikipedia To_Mock_a_Mockingbird]].
 Other sources include