> **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**.
> **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.
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,
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.