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
-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):
+combinator which following Curry and Steedman, I'll call *T*, 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):
<pre>
; 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)
</pre>
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*,
operator that used `unit` to produce a monadic result, if we wanted to.
The monad version of *Everyone_i thinks he_i left*, then (remembering
-that `he = fun x -> x`, and that `l a f = f a`) is
+that `he = fun x -> x`, and letting `t a f = f a`) is
<pre>
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)
</pre>
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.
+