## Jacobson's Variable-Free Semantics as a bare-bones Reader Monad

Jacobson's Variable-Free Semantics (e.g., Jacobson 1999, Towards a
Variable-Free
Semantics)
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
assignment function threaded through the computation is limited to at
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* 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 he = \x. x in let everyone = \P. FORALL x (P x) in everyone (z thinks (g left he)) ~~> FORALL x (thinks (left x) x)

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 identity combinator (see additional comments below). We'll return to the idea of pronouns as identity functions in later discussions.

Second, *g* plays the role of transmitting a binding dependency for an
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.)

Last week we saw a Reader monad for tracking variable assignments:

type env = (char * int) list;; type 'a reader = env -> 'a;; let unit x = fun (e : env) -> x;; let bind (u : 'a reader) (f: 'a -> 'b reader) : 'b reader = fun (e : env) -> f (u e) e;; let shift (c : char) (v : int reader) (u : 'a reader) = fun (e : env) -> u ((c, v e) :: e);; let lookup (c : char) : int reader = fun (e : env) -> List.assoc c e;;

(We've used a simplified term for the bind function here in order to emphasize its similarities with Jacboson's geach combinator.)

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 can consider the following monad:

type e = int;; type 'a link = e -> 'a;; let unit (a:'a): 'a link = fun x -> a;; let bind (u: 'a link) (f: 'a -> 'b link) : 'b link = fun (x:e) -> f (u x) x;; let ap (u: ('a -> 'b) link) (v: 'a link) : 'b link = fun (x:e) -> u x (v x);; let lift (f: 'a -> 'b) (u: 'a link): ('b link) = ap (unit f) u;; let g = lift;; let z (f: 'a -> e -> 'b) (u: 'a link) : e -> 'b = fun (x:e) -> f (u x) x;;

I've called this the *link* monad, because it links (exactly one)
pronoun with a binder, but it's a kind of Reader monad. (Prove that
`ap`

, the combinator for applying a linked functor to a linked object,
can be equivalently defined in terms of `bind`

and `unit`

.)

In order to keep the types super simple, I've assumed that the only
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.

In the standard Reader monad, the environment is an assignment function. Here, instead this monad provides a single value. The idea is that this is the value that will be used to replace the pronoun linked to it by the monad.

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.

Furthermore, Jacobson's *z* combinator, which is what she uses to
create binding links, is essentially identical to our reader-monad
`bind`

! Interestingly, the types are different, at least at a
conceptual level. Here they are side by side:

let bind (u: 'a link) (f: 'a -> 'b link) : 'b link = fun (x:e) -> f (u x) x;; let z (f: 'a -> e -> 'b) (u: 'a link) : e -> 'b = fun (x:e) -> f (u x) x;;

`Bind`

takes an `'a link`

, and a function that maps an `'a`

to a ```
'b
link
```

, and returns a `'b link`

, i.e., the result is in the link monad.
*z*, on the other hand, takes the same two arguments (in reverse
order), but returns something that is not in the monad. Rather, it
will be a function from individuals to a computation in which the
pronoun in question is bound to that individual. We could emphasize
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
that `he = fun x -> x`

, and letting `t a f = f a`

) is

everyone (z thinks (g left he)) ~~> forall w (thinks (left w) w) everyone (z thinks (g (t bill) (g said (g left he)))) ~~> forall w (thinks (said (left w) bill) w)

So *g* is exactly `lift`

(a combination of `bind`

and `unit`

), and *z*
is exactly `bind`

with the arguments reversed. It appears that
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. (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, 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.