author Chris Barker Sat, 18 Sep 2010 13:25:25 +0000 (09:25 -0400) committer Chris Barker Sat, 18 Sep 2010 13:25:25 +0000 (09:25 -0400)
 week2.mdwn patch | blob | history

index 77459bf..ac2a7c3 100644 (file)
@@ -6,6 +6,13 @@ Define T to be `(\x. x y) z`. Then T and `(\x. x y) z` are syntactically equal,
<pre><code>T &equiv; (\x. x y) z &equiv; (\z. z y) z
</code></pre>

<pre><code>T &equiv; (\x. x y) z &equiv; (\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
This:

T ~~> z y
@@ -23,21 +30,43 @@ Lambda expressions that have no free variables are known as **combinators**. Her

>      **I** is defined to be `\x x`

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

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

->      **&omega;** is defined to be: `\x. x x`
+>      **&omega;** is defined to be: `\x. x x (\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.

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.)

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.

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.
+
+
+![Szabolcsi's analysis of *himself* as the duplicator combinator](szabolcsi-reflexive.png)
+
+
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!

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!