--- /dev/null
+[[!toc]]
+
+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](http://www.springerlink.com/content/j706674r4w217jj5/))
+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 assignment.
+
+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 adjusts function/argument order when the
+argument precedes its functor, but we'll finesse that here by freely
+reordering the English predicates so that functors always precede
+their arguments.) 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))
+
+~~> FORALL x (thinks (left x) x)
+</pre>
+
+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:
+
+<pre>
+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;;
+</pre>
+
+(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:
+
+<pre>
+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;;
+</pre>
+
+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:
+
+<pre>
+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;;
+</pre>
+
+`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
+
+<pre>
+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)
+</pre>
+
+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.