X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week8.mdwn;h=d3b5c1b7b283f1133ffd9c603210a5fc4627acc1;hp=e99e223ab91f6bf1d4bbd350355f0f9ecaeed97c;hb=826badc8d42e8fa03f46abf36273d1daadf991e7;hpb=adaf5a4a914b56ca7be6c3fce6da8269e1ed23ca diff --git a/week8.mdwn b/week8.mdwn index e99e223a..d3b5c1b7 100644 --- a/week8.mdwn +++ b/week8.mdwn @@ -11,24 +11,23 @@ positions. The system does not make use of assignment functions or variables. We'll see that from the point of view of our discussion of monads, Jacobson's system is essentially a reader monad in which the assignment function threaded through the computation is limited to at -most one assignment. +most one variable. It will turn out that Jacobson's geach combinator +*g* is exactly our `lift` operator, and her binding combinator *z* is +exactly our `bind` with the arguments reversed! Jacobson's system contains two main combinators, *g* and *z*. She -calls *g* the Geach rule, and *z* effects binding. (There is a third -combinator, *l*, which we'll make use of to adjust function/argument -order to better match English word order; N.B., though, that -Jacobson's name for this combinator is "lift", but it is different -from the monadic lift discussed in some detail below.) Here is a -typical computation (based closely on email from Simon Charlow, with -beta reduction as performed by the on-line evaluator): +calls *g* the Geach rule, and *z* performs binding. Here is a typical +computation. This implementation is based closely on email from Simon +Charlow, with beta reduction as performed by the on-line evaluator:
``` ; Analysis of "Everyone_i thinks he_i left"
let g = \f g x. f (g x) in
let z = \f g x. f (g x) x in
-let everyone = \P. FORALL x (P x) in
let he = \x. x in
-everyone ((z thinks) (g left he))
+let everyone = \P. FORALL x (P x) in
+
+everyone (z thinks (g left he))

~~>  FORALL x (thinks (left x) x)
```
``` everyone (z thinks (g left he))

~~> forall w (thinks (left w) w)

-everyone (z thinks (g (l bill) (g said (g left he))))
+everyone (z thinks (g (t bill) (g said (g left he))))

~~> forall w (thinks (said (left w) bill) w)
```
```+    John believes Mary said he thinks she's cute.
+     |             |         |         |
+     |             |---------|---------|
+     |                       |
+     |-----------------------|
+```
+ +It will be convenient to +have a counterpart to the lift operation that combines a monadic +functor with a non-monadic argument: + +
```+    let g f v = ap (unit f) v;;
+    let g2 u a = ap u (unit a);;
+```
+ +As a first step, we'll bind "she" by "Mary": + +
```+believes (z said (g2 (g thinks (g cute she)) she) mary) john
+
+~~> believes (said (thinks (cute mary) he) mary) john
+```
+ +As usual, there is a trail of *g*'s leading from the pronoun up to the +*z*. Next, we build a trail from the other pronoun ("he") to its +binder ("John"). + +
```+believes
+  said
+    thinks (cute she) he
+    Mary
+  John
+
+believes
+  z said
+    (g2 ((g thinks) (g cute she))) he
+    Mary
+  John
+
+z believes
+  (g2 (g (z said)
+         (g (g2 ((g thinks) (g cute she)))
+            he))
+      Mary)
+  John
+```
+ +In the first interation, we build a chain of *g*'s and *g2*'s from the +pronoun to be bound ("she") out to the level of the first argument of +*said*. + +In the second iteration, we treat the entire structure as ordinary +functions and arguments, without "seeing" the monadic region. Once +again, we build a chain of *g*'s and *g2*'s from the currently +targeted pronoun ("he") out to the level of the first argument of +*believes*. (The new *g*'s and *g2*'s are the three leftmost). + +
```+z believes (g2 (g (z said) (g (g2 ((g thinks) (g cute she))) he)) mary) john
+
+~~> believes (said (thinks (cute mary) john) mary) john
+```
+ +Obviously, we can repeat this strategy for any configuration of pronouns +and binders. + +This binding strategy is strongly reminiscent of the translation from +the lambda calculus into Combinatory Logic that we studied earlier +(see the lecture notes for week 2). Recall that bound pronouns ended +up translating to I, the identity combinator, just like Jacobson's +identity functions for pronouns; abstracts (\a.M) whose body M did not +contain any occurrences of the pronoun to be bound translated as KM, +just like our unit, which you will recognize as an instance of K; and +abstracts of the form (\a.MN) translated to S[\aM][\aN], just like our +ap rule.