<pre><code>T ≡ (\x. x y) z ≡ (\z. z y) z
</code></pre>
+[Fussy note: the justification for counting `(\x. x y) z` as
+equivalent to `(\z. z y) z` is that when a lambda binds a set of
+occurrences, it doesn't matter which variable serves to carry out the
+binding. Either way, the function does the same thing and means the
+same thing. Look in the standard treatments for discussions of alpha
+equivalence for more detail.]
+
This:
T ~~> z y
> **I** is defined to be `\x x`
-> **K** is defined to be `\x y. x`, That is, it throws away its second argument. So `K x` is a constant function from any (further) argument to `x`. ("K" for "constant".) Compare K to our definition of **true**.
+> **K** is defined to be `\x y. x`, That is, it throws away its
+ second argument. So `K x` is a constant function from any
+ (further) argument to `x`. ("K" for "constant".) Compare K
+ to our definition of **true**.
> **get-first** was our function for extracting the first element of an ordered pair: `\fst snd. fst`. Compare this to **K** and **true** as well.
One can do that with a very spare set of basic combinators. These days the standard base is just three combinators: K and I from above, and also one more, **S**, which behaves the same as the lambda expression `\f g x. f x (g x)`. behaves. But it's possible to be even more minimalistic, and get by with only a single combinator. (And there are different single-combinator bases you can choose.)
+There are some well-known linguistic applications of Combinatory
+Logic, due to Anna Szabolcsi, Mark Steedman, and Pauline Jacobson.
+Szabolcsi supposed that the meanings of certain expressions could be
+insightfully expressed in the form of combinators. A couple more
+combinators:
+
+ **C** is defined to be: `\f x y. f y x` [swap arguments]
+
+ **W** is defined to be: `\f x . f x x` [duplicate argument]
+
+For instance, Szabolcsi argues that reflexive pronouns are argument
+duplicators.
+
+
+
+Notice that the semantic value of *himself* is exactly W.
+The reflexive pronoun in direct object position combines first with the transitive verb (through compositional magic we won't go into here). The result is an intransitive verb phrase that takes a subject argument, duplicates that argument, and feeds the two copies to the transitive verb meaning.
+
+Note that W = S(CI):
+
+ S(CI) =
+ S((\fxy.fyx)(\x.x)) =
+ S(\xy.(\x.x)yx) =
+ (\fgx.fx(gx))(\xy.yx) =
+ \gx.[\xy.yx]x(gx) =
+ \gx.(gx)x =
+ W
+
+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,
+
+ IX ~~> X
+
+Thinking of this as a reduction rule, we can perform the following computation
+
+ II(IX) ~~> IIX ~~> IX ~~> X
+
+The reduction rule for K is also straigtforward:
+
+ KXY ~~> X
+
+That is, K throws away its second argument. The reduction rule for S can be constructed by examining
+the defining lambda term:
+
+ S = \fgx.fx(gx)
+
+S takes three arguments, duplicates the third argument, and feeds one copy to the first argument and the second copy to the second argument. So:
+
+ SFGX ~~> FX(GX)
+
+If the meaning of a function is nothing more than how it behaves with respect to its arguments,
+these reduction rules capture the behavior of the combinators S,K, and I completely.
+We can use these rules to compute without resorting to beta reduction. For instance, we can show how the I combinator is equivalent to a certain crafty combination of S's and K's:
+
+ SKKX ~~> KX(KX) ~~> X
+
+So the combinator SKK is equivalent to the combinator I.
+
+
These systems 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!
-Here's more to read about combinatorial logic:
+Here's more to read about combinatorial logic.
+Surely the most entertaining exposition is Smullyan's [[!wikipedia To_Mock_a_Mockingbird]].
+Other sources include
* [[!wikipedia Combinatory logic]] at Wikipedia
* [Combinatory logic](http://plato.stanford.edu/entries/logic-combinatory/) at the Stanford Encyclopedia of Philosophy