X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week8.mdwn;h=e285451add14ef6b1fb8d0d9900e93a2a9ed1d28;hp=1a0b55bbbc60108bb29d1500ca5576b3502296b8;hb=aab06ee4eafe7ac322521e4cef1b1704a9258900;hpb=b7a09b298589d5965edea1fd051c22fb69b42b62 diff --git a/week8.mdwn b/week8.mdwn index 1a0b55bb..e285451a 100644 --- a/week8.mdwn +++ b/week8.mdwn @@ -9,26 +9,25 @@ Semantics](http://www.springerlink.com/content/j706674r4w217jj5/)) uses combinators to impose binding relationships between argument 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 +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 adjusts function/argument order when the -argument precedes its functor, but we'll finesse that here by freely -reordering the English predicates so that functors always precede -their arguments.) 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)
```
``` type env = (char * int) list;;
@@ -68,15 +66,15 @@ let shift (c : char) (v : int reader) (u : 'a reader) =
let lookup (c : char) : int reader = fun (e : env) -> List.assoc c e;;
```
-(We've used a simplified term for the bind function in order to +(We've used a simplified term for the bind function here in order to emphasize its similarities with Jacboson's geach combinator.) -This monad boxed up a value along with an assignment function, where +This monad boxes up a value along with an assignment function, where an assignemnt function was implemented as a list of `char * int`. The idea is that a list like `[('a', 2); ('b',5)]` associates the variable `'a'` with the value 2, and the variable `'b'` with the value 5. -Combining this reader monad with ideas from Jacobson's approach, we +Combining this Reader monad with ideas from Jacobson's approach, we can consider the following monad:
```@@ -91,7 +89,7 @@ let z (f: 'a -> e -> 'b) (u: 'a link) : e -> 'b = fun (x:e) -> f (u 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.