3 Jacobson's Variable-Free Semantics as a bare-bones Reader Monad
4 ---------------------------------------------------------------
6 Jacobson's Variable-Free Semantics (e.g., Jacobson 1999, [Towards a
8 Semantics](http://www.springerlink.com/content/j706674r4w217jj5/))
9 uses combinators to impose binding relationships between argument
10 positions. The system does not make use of assignment functions or
11 variables. We'll see that from the point of view of our discussion of
12 monads, Jacobson's system is essentially a reader monad in which the
13 assignment function threaded through the computation is limited to at
14 most one assignment. More specifically, Jacobson's geach combinator
15 *g* is exactly our `lift` operator, and her binding combinator *z* is
16 exactly our `bind` with the arguments reversed!
18 Jacobson's system contains two main combinators, *g* and *z*. She
19 calls *g* the Geach rule, and *z* effects binding. (There is a third
20 combinator which following Curry and Steedman, I'll call *T*, which
21 we'll make use of to adjust function/argument order to better match
22 English word order; N.B., though, that Jacobson's name for this
23 combinator is "lift", but it is different from the monadic lift
24 discussed in some detail below.) Here is a typical computation (based
25 closely on email from Simon Charlow, with beta reduction as performed
26 by the on-line evaluator):
29 ; Analysis of "Everyone_i thinks he_i left"
30 let g = \f g x. f (g x) in
31 let z = \f g x. f (g x) x in
33 let everyone = \P. FORALL x (P x) in
35 everyone (z thinks (g left he))
37 ~~> FORALL x (thinks (left x) x)
40 Several things to notice: First, pronouns denote identity functions.
41 As Jeremy Kuhn has pointed out, this is related to the fact that in
42 the mapping from the lambda calculus into combinatory logic that we
43 discussed earlier in the course, bound variables translated to I, the
44 identity combinator. This is a point we'll return to in later
47 Second, *g* plays the role of transmitting a binding dependency for an
48 embedded constituent to a containing constituent. If the sentence had
49 been *Everyone_i thinks Bill said he_i left*, there would be an
50 occurrence of *g* in the most deeply embedded clause (*he left*), and
51 another occurrence of *g* in the next most deeply
52 embedded constituent (*said he left*), and so on (see below).
54 Third, binding is accomplished by applying *z* not to the element that
55 will (in some pre-theoretic sense) bind the pronoun, here, *everyone*,
56 but by applying *z* instead to the predicate that will take *everyone*
57 as an argument, here, *thinks*. The basic recipe in Jacobson's system
58 is that you transmit the dependence of a pronoun upwards through the
59 tree using *g* until just before you are about to combine with the
60 binder, when you finish off with *z*.
62 Last week we saw a reader monad for tracking variable assignments:
65 type env = (char * int) list;;
66 type 'a reader = env -> 'a;;
67 let unit x = fun (e : env) -> x;;
68 let bind (u : 'a reader) (f: 'a -> 'b reader) : 'b reader =
69 fun (e : env) -> f (u e) e;;
70 let shift (c : char) (v : int reader) (u : 'a reader) =
71 fun (e : env) -> u ((c, v e) :: e);;
72 let lookup (c : char) : int reader = fun (e : env) -> List.assoc c e;;
75 (We've used a simplified term for the bind function in order to
76 emphasize its similarities with Jacboson's geach combinator.)
78 This monad boxed up a value along with an assignment function, where
79 an assignemnt function was implemented as a list of `char * int`. The
80 idea is that a list like `[('a', 2); ('b',5)]` associates the variable
81 `'a'` with the value 2, and the variable `'b'` with the value 5.
83 Combining this reader monad with ideas from Jacobson's approach, we
84 can consider the following monad:
88 type 'a link = e -> 'a;;
89 let unit (a:'a): 'a link = fun x -> a;;
90 let bind (u: 'a link) (f: 'a -> 'b link) : 'b link = fun (x:e) -> f (u x) x;;
91 let ap (u: ('a -> 'b) link) (v: 'a link) : 'b link = fun (x:e) -> u x (v x);;
92 let lift (f: 'a -> 'b) (u: 'a link): ('b link) = ap (unit f) u;;
94 let z (f: 'a -> e -> 'b) (u: 'a link) : e -> 'b = fun (x:e) -> f (u x) x;;
97 I've called this the *link* monad, because it links (exactly one)
98 pronoun with a binder, but it's a kind of reader monad. (Prove that
99 `ap`, the combinator for applying a linked functor to a linked object,
100 can be equivalently defined in terms of `bind` and `unit`.)
102 In order to keep the types super simple, I've assumed that the only
103 kind of value that can be linked into a structure is an individual of
104 type `e`. It is easy to make the monad polymorphic in the type of the
105 linked value, which will be necessary to handle, e.g., paycheck pronouns.
107 Note that in addition to `unit` being Curry's K combinator, this `ap`
108 is the S combinator. Not coincidentally, recall that the rule for
109 converting an arbitrary application `M N` into Combinatory Logic is `S
110 [M] [N]`, where `[M]` is the CL translation of `M` and `[N]` is the CL
111 translation of `N`. There, as here, the job of `ap` is to take an
112 argument and make it available for any pronouns (variables) in the two
113 components of the application.
115 In the standard reader monad, the environment is an assignment
116 function. Here, instead this monad provides a single value. The idea
117 is that this is the value that will replace the pronouns linked to it
120 Jacobson's *g* combinator is exactly our `lift` operator: it takes a
121 functor and lifts it into the monad. Surely this is more than a coincidence.
123 Furthermore, Jacobson's *z* combinator, which is what she uses to
124 create binding links, is essentially identical to our reader-monad
125 `bind`! Interestingly, the types are different, at least at a
126 conceptual level. Here they are side by side:
129 let bind (u: 'a link) (f: 'a -> 'b link) : 'b link = fun (x:e) -> f (u x) x;;
130 let z (f: 'a -> e -> 'b) (u: 'a link) : e -> 'b = fun (x:e) -> f (u x) x;;
133 `Bind` takes an `'a link`, and a function that maps an `'a` to a `'b
134 link`, and returns a `'b link`, i.e., the result is in the link monad.
135 *z*, on the other hand, takes the same two arguments (in reverse
136 order), but returns something that is not in the monad. Rather, it
137 will be a function from individuals to a computation in which the
138 pronoun in question is bound to that individual. We could emphasize
139 the parallel with the reader monad even more by writing a `shift`
140 operator that used `unit` to produce a monadic result, if we wanted to.
142 The monad version of *Everyone_i thinks he_i left*, then (remembering
143 that `he = fun x -> x`, and letting `t a f = f a`) is
146 everyone (z thinks (g left he))
148 ~~> forall w (thinks (left w) w)
150 everyone (z thinks (g (t bill) (g said (g left he))))
152 ~~> forall w (thinks (said (left w) bill) w)
155 So *g* is exactly `lift` (a combination of `bind` and `unit`), and *z*
156 is exactly `bind` with the arguments reversed. It appears that
157 Jacobson's variable-free semantics is essentially a reader monad.
159 One of Jacobson's main points survives: restricting the reader monad
160 to a single-value environment eliminates the need for variable names.
162 It requires some cleverness to use the link monad to bind more than
163 one variable at a time. Whereas in the standard reader monad a single
164 environment can record any number of variable assignments, because
165 Jacobson's monad only tracks a single dependency, binding more than
166 one pronoun requires layering the monad, so that intermediate regions
167 of the computation will be functors inside of a link monad box inside
168 another link monad box, and so on.
170 [Give details of the readings of *Everyone said someone thinks that he
171 likes her*. Jacobson needs to add a variant of g; is it necessary to
172 write a link swap that reverses the nesting of the monad boxes?]