X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week2.mdwn;h=720ac1d81faaef9f9b6cfbf518bd730b0f62d05c;hp=992c8c8975efd62467f72b8e7c6458460f004135;hb=43e6cb0a08452826d9b0757f16e30e117df894b8;hpb=600b9e54be61643b0d85021bfbfbd575f47b0d17 diff --git a/week2.mdwn b/week2.mdwn index 992c8c89..720ac1d8 100644 --- a/week2.mdwn +++ b/week2.mdwn @@ -6,6 +6,13 @@ Define T to be `(\x. x y) z`. Then T and `(\x. x y) z` are syntactically equal,
T ≡ (\x. x y) z ≡ (\z. z y) z
+[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
@@ -23,7 +30,10 @@ Lambda expressions that have no free variables are known as **combinators**. Her
> **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.
@@ -35,9 +45,29 @@ It's possible to build a logical system equally powerful as the lambda calculus
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.
+
+![test](./szabolcsi-reflexive.jpg)
+
+![Szabolcsi's analysis of *himself* as the duplicator combinator](szabolcsi-reflexive.jpg)
+
+
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
@@ -161,7 +191,8 @@ One important advantage of normal-order evaluation in particular is that it can
Indeed, it's provable that if there's *any* reduction path that delivers a value for a given expression, the normal-order evalutation strategy will terminate with that value.
-An expression is said to be in **normal form** when it's not possible to perform any more reductions. (EVEN INSIDE ABSTRACTS?) There's a sense in which you *can't get anything more out of* ω ω
, but it's not in normal form because it still has the form of a redex.
+An expression is said to be in **normal form** when it's not possible to perform any more reductions (not even inside abstracts).
+There's a sense in which you *can't get anything more out of* ω ω
, but it's not in normal form because it still has the form of a redex.
A computational system is said to be **confluent**, or to have the **Church-Rosser** or **diamond** property, if, whenever there are multiple possible evaluation paths, those that terminate always terminate in the same value. In such a system, the choice of which sub-expressions to evaluate first will only matter if some of them but not others might lead down a non-terminating path.