; 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)) ~~> 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. This is a point we'll return to in later discussions. 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*. 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 in order to emphasize its similarities with Jacboson's geach combinator.) This monad boxed 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. 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. 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 replace the pronouns 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 that `l a f = f a`) is

everyone (z thinks (g left he)) ~~> forall w (thinks (left w) w) everyone (z thinks (g (l 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.