> **I** is defined to be `\x x`
-> **K** is defined to be `\x y. x`, That is, it throws away its
+> **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**.
+ 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.
+> **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.
-> **get-second** was our function for extracting the second element of an ordered pair: `\fst snd. snd`. Compare this to our definition of **false**.
+> **get-second** was our function for extracting the second element of an ordered pair: `\fst snd. snd`. Compare this to our definition of `false`.
-> **ω** is defined to be: `\x. x x`
+> **B** is defined to be: `\f g x. f (g x)`. (So `B f g` is the composition `\x. f (g x)` of `f` and `g`.)
+
+> **C** is defined to be: `\f x y. f y x`. (So `C f` is a function like `f` except it expects its first two arguments in swapped order.)
+
+> **W** is defined to be: `\f x . f x x`. (So `W f` accepts one argument and gives it to `f` twice. What is the meaning of `W multiply`?)
+
+> **ω** (that is, lower-case omega) is defined to be: `\x. x x`
It's possible to build a logical system equally powerful as the lambda calculus (and readily intertranslatable with it) using just combinators, considered as atomic operations. Such a language doesn't have any variables in it: not just no free variables, but no variables at all.
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]
+insightfully expressed in the form of combinators.
- **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.
+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):
+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
+<pre><code>S(CI) ≡
+S((\fxy.fyx)(\x.x)) ~~>
+S(\xy.(\x.x)yx) ~~>
+S(\xy.yx) ≡
+(\fgx.fx(gx))(\xy.yx) ~~>
+\gx.(\xy.yx)x(gx) ~~>
+\gx.(gx)x ≡
+W</code></pre>
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,
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:
+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 Ss and Ks:
SKKX ~~> KX(KX) ~~> X
-So the combinator SKK is equivalent to the combinator I.
+So the combinator `SKK` is equivalent to the combinator I.
-Combinatory Logic is what you have when you choose a set of combinators and regulate their behavior with a set of reduction rules. The most common system uses S,K, and I as defined here.
+Combinatory Logic is what you have when you choose a set of combinators and regulate their behavior with a set of reduction rules. The most common system uses S, K, and I as defined here.
-*The equivalence of the untyped lambda calculus and combinatory logic*
+###The equivalence of the untyped lambda calculus and combinatory logic###
We've claimed that Combinatory Logic is equivalent to the lambda calculus. If that's so, then S, K, and I must be enough to accomplish any computational task imaginable. Actually, S and K must suffice, since we've just seen that we can simulate I using only S and K. In order to get an intuition about what it takes to be Turing complete, imagine what a text editor does:
it transforms any arbitrary text into any other arbitrary text. The way it does this is by deleting, copying, and reordering characters. We've already seen that K deletes its second argument, so we have deletion covered. S duplicates and reorders, so we have some reason to hope that S and K are enough to define arbitrary functions.