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`
\gx.(gx)x ≡
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,
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.
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]]
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
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 ≡ `\xy.yx`, B ≡ `\fxy.f(xy)`,
and our friend S. Steedman used Smullyan's fanciful bird
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!
+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