X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week2.mdwn;h=371435d4c35369d0e959d57a2cf7a4035ccc1465;hp=77459bfda891dc264e5619162878263015ef5706;hb=846488bfeb5f20947b983de2c3a1faca00d63b3a;hpb=c359efaee71b34e8db4e7527c75766fde6c0e8fa diff --git a/week2.mdwn b/week2.mdwn index 77459bfd..371435d4 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,21 +30,116 @@ 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. + +> **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. +> **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`.) -> **get-second** was our function for extracting the second element of an ordered pair: `\fst snd. snd`. Compare this to our definition of **false**. +> **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.) -> **ω** is defined to be: `\x. x x` +> **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. 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. + + +For instance, Szabolcsi argues that reflexive pronouns are argument +duplicators. + +![reflexive](http://lambda.jimpryor.net/szabolcsi-reflexive.jpg) + +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) ~~>
+S(\xy.yx) ≡
+(\fgx.fx(gx))(\xy.yx) ~~>
+\gx.(\xy.yx)x(gx) ~~>
+\gx.(gx)x ≡
+W``````