index e99e223..d3b5c1b 100644 (file)
@@ -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
assignment function threaded through the computation is limited to at
variables.  We'll see that from the point of view of our discussion of
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

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:

<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

<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
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>

~~>  FORALL x (thinks (left x) x)
</pre>
@@ -37,23 +36,22 @@ Several things to notice: First, pronouns denote identity functions.
As Jeremy Kuhn has pointed out, this is related to the fact that in
the mapping from the lambda calculus into combinatory logic that we
discussed earlier in the course, bound variables translated to I, the
As Jeremy Kuhn has pointed out, this is related to the fact that in
the mapping from the lambda calculus into combinatory logic that we
discussed earlier in the course, bound variables translated to I, the
-identity combinator.  This is a point we'll return to in later
-discussions.
+the idea of pronouns as identity functions in later discussions.

Second, *g* plays the role of transmitting a binding dependency for an

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
-another occurrence of (a variant of) *g* in the next most deeply
-embedded clause (*Bill said he left*).
-
-Third, binding is accomplished by applying *z* not to the element that
-will (in some pre-theoretic sense) bind the pronoun, here, *everyone*,
-but by applying *z* instead to the predicate that will take *everyone*
-as an argument, here, *thinks*.  The basic recipe in Jacobson's system
-is that you transmit the dependence of a pronoun upwards through the
-tree using *g* until just before you are about to combine with the
-binder, when you finish off with *z*.
+embedded constituent to a containing constituent.
+
+Third, one of the peculiar aspects of Jacobson's system is that
+binding is accomplished not by applying *z* to the element that will
+(in some pre-theoretic sense) bind the pronoun, here, *everyone*, but
+rather by applying *z* instead to the predicate that will take
+*everyone* as an argument, here, *thinks*.
+
+The basic recipe in Jacobson's system, then, is that you transmit the
+dependence of a pronoun upwards through the tree using *g* until just
+before you are about to combine with the binder, when you finish off
+with *z*.  (There are examples with longer chains of *g*'s below.)

@@ -68,10 +66,10 @@ let shift (c : char) (v : int reader) (u : 'a reader) =
let lookup (c : char) : int reader = fun (e : env) -> List.assoc c e;;
</pre>

let lookup (c : char) : int reader = fun (e : env) -> List.assoc c e;;
</pre>

-(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.)

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.
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.
@@ -100,18 +98,10 @@ kind of value that can be linked into a structure is an individual of
type `e`.  It is easy to make the monad polymorphic in the type of the
linked value, which will be necessary to handle, e.g., paycheck pronouns.

type `e`.  It is easy to make the monad polymorphic in the type of the
linked value, which will be necessary to handle, e.g., paycheck pronouns.

-Note that in addition to `unit` being Curry's K combinator, this `ap`
-is the S combinator.  Not coincidentally, recall that the rule for
-converting an arbitrary application `M N` into Combinatory Logic is `S
-[M] [N]`, where `[M]` is the CL translation of `M` and `[N]` is the CL
-translation of `N`.  There, as here, the job of `ap` is to take an
-argument and make it available for any pronouns (variables) in the two
-components of the application.
-
-is that this is the value that will replace the pronouns linked to it
+is that this is the value that will be used to replace the pronoun

Jacobson's *g* combinator is exactly our `lift` operator: it takes a
functor and lifts it into the monad.  Surely this is more than a coincidence.

Jacobson's *g* combinator is exactly our `lift` operator: it takes a
functor and lifts it into the monad.  Surely this is more than a coincidence.
@@ -136,14 +126,14 @@ the parallel with the reader monad even more by writing a `shift`
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
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)

<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>

~~> forall w (thinks (said (left w) bill) w)
</pre>
@@ -154,3 +144,96 @@ Jacobson's variable-free semantics is essentially a reader monad.

to a single-value environment eliminates the need for variable names.

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
+
+<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, 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.