From: Chris Barker Date: Mon, 8 Nov 2010 19:53:00 +0000 (-0500) Subject: multiple binding with Jacobson X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=ac1241bd46013ce4d552868fae863d1921420eb6 multiple binding with Jacobson --- diff --git a/week8.mdwn b/week8.mdwn index 7f42092d..cd99b421 100644 --- a/week8.mdwn +++ b/week8.mdwn @@ -159,14 +159,95 @@ Jacobson's variable-free semantics is essentially a reader monad. One of Jacobson's main points survives: restricting the reader monad to a single-value environment eliminates the need for variable names. +Binding more than one variable at a time +---------------------------------------- + It requires some cleverness to use the link monad to bind more than one variable at a time. Whereas in the standard reader monad a single environment can record any number of variable assignments, because Jacobson's monad only tracks a single dependency, binding more than -one pronoun requires layering the monad, so that intermediate regions -of the computation will be functors inside of a link monad box inside -another link monad box, and so on. +one pronoun requires layering the monad. (Jacobson provides some +special combinators, but we can make do with the ingredients already +defined.) + +Let's take the following sentence as our target, with the obvious +binding relationships: + +
+    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, K; and abstracts of the form (\a.MN) translated to +S[\aM][\aN], just like our ap rule. -[Give details of the readings of *Everyone said someone thinks that he -likes her*. Jacobson needs to add a variant of g; is it necessary to -write a link swap that reverses the nesting of the monad boxes?]