multiple binding with Jacobson

[lambda.git] / week8.mdwn

diff --git a/week8.mdwn b/week8.mdwn
index 27308c9..cd99b42 100644 (file)
--- a/week8.mdwn
+++ b/week8.mdwn
@@ -11,7 +11,9 @@ 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
 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 assignment.  More specifically, 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
 
 Jacobson's system contains two main combinators, *g* and *z*.  She
 calls *g* the Geach rule, and *z* effects binding.  (There is a third


@@ -46,8 +48,8 @@ Second, *g* plays the role of transmitting a binding dependency for an
 embedded constituent to a containing constituent.  If the sentence had
 been *Everyone_i thinks Bill said he_i left*, there would be an
 occurrence of *g* in the most deeply embedded clause (*he left*), and
 embedded constituent to a containing constituent.  If the sentence had
 been *Everyone_i thinks Bill said he_i left*, there would be an
 occurrence of *g* in the most deeply embedded clause (*he left*), and

-another occurrence of (a variant of) *g* in the next most deeply
-embedded clause (*Bill said he left*).
+another occurrence of *g* in the next most deeply
+embedded constituent (*said he left*), and so on (see below).

 
 Third, binding is accomplished by applying *z* not to the element that
 will (in some pre-theoretic sense) bind the pronoun, here, *everyone*,
 
 Third, binding is accomplished by applying *z* not to the element that
 will (in some pre-theoretic sense) bind the pronoun, here, *everyone*,


@@ -156,3 +158,96 @@ 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.
 
 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.  (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:
+
+<pre>
+    John believes Mary said he thinks she's cute.
+     |             |         |         |
+     |             |---------|---------|
+     |                       |
+     |-----------------------|
+</pre>
+
+It will be convenient to
+have a counterpart to the lift operation that combines a monadic
+functor with a non-monadic argument:
+
+<pre>
+    let g f v = ap (unit f) v;;
+    let g2 u a = ap u (unit a);;
+</pre>
+
+As a first step, we'll bind "she" by "Mary":
+
+<pre>
+believes (z said (g2 (g thinks (g cute she)) she) mary) john
+
+~~> believes (said (thinks (cute mary) he) mary) john
+</pre>
+
+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").  
+
+<pre>
+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
+</pre>
+
+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).
+
+<pre>
+z believes (g2 (g (z said) (g (g2 ((g thinks) (g cute she))) he)) mary) john
+
+~~> believes (said (thinks (cute mary) john) mary) john
+</pre>
+
+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.
+