week8.mdwn

   1 [[!toc]]
   2
   3 Jacobson's Variable-Free Semantics as a bare-bones Reader Monad
   4 ---------------------------------------------------------------
   5
   6 Jacobson's Variable-Free Semantics (e.g., Jacobson 1999, [Towards a
   7 Variable-Free
   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!
  17
  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):
  27
  28 <pre>
  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
  32 let he = \x. x in
  33 let everyone = \P. FORALL x (P x) in
  34
  35 everyone (z thinks (g left he))
  36
  37 ~~>  FORALL x (thinks (left x) x)
  38 </pre>
  39
  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
  45 discussions.
  46
  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).
  53
  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*.
  61
  62 Last week we saw a reader monad for tracking variable assignments:
  63
  64 <pre>
  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;;
  73 </pre>
  74
  75 (We've used a simplified term for the bind function in order to
  76 emphasize its similarities with Jacboson's geach combinator.)
  77
  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.
  82
  83 Combining this reader monad with ideas from Jacobson's approach, we
  84 can consider the following monad:
  85
  86 <pre>
  87 type e = int;;
  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;;
  93 let g = lift;;
  94 let z (f: 'a -> e -> 'b) (u: 'a link) : e -> 'b = fun (x:e) -> f (u x) x;;
  95 </pre>
  96
  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`.)
 101
 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.
 106
 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.
 114
 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
 118 by the monad.
 119
 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.
 122
 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:
 127
 128 <pre>
 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;;
 131 </pre>
 132
 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.
 141
 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
 144
 145 <pre>
 146 everyone (z thinks (g left he))
 147
 148 ~~> forall w (thinks (left w) w)
 149
 150 everyone (z thinks (g (t bill) (g said (g left he))))
 151
 152 ~~> forall w (thinks (said (left w) bill) w)
 153 </pre>
 154
 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.
 158
 159 One of Jacobson's main points survives: restricting the reader monad
 160 to a single-value environment eliminates the need for variable names.
 161
 162 Binding more than one variable at a time
 163 ----------------------------------------
 164
 165 It requires some cleverness to use the link monad to bind more than
 166 one variable at a time.  Whereas in the standard reader monad a single
 167 environment can record any number of variable assignments, because
 168 Jacobson's monad only tracks a single dependency, binding more than
 169 one pronoun requires layering the monad.  (Jacobson provides some
 170 special combinators, but we can make do with the ingredients already
 171 defined.)
 172
 173 Let's take the following sentence as our target, with the obvious
 174 binding relationships:
 175
 176 <pre>
 177     John believes Mary said he thinks she's cute.
 178      |             |         |         |
 179      |             |---------|---------|
 180      |                       |
 181      |-----------------------|
 182 </pre>
 183
 184 It will be convenient to
 185 have a counterpart to the lift operation that combines a monadic
 186 functor with a non-monadic argument:
 187
 188 <pre>
 189     let g f v = ap (unit f) v;;
 190     let g2 u a = ap u (unit a);;
 191 </pre>
 192
 193 As a first step, we'll bind "she" by "Mary":
 194
 195 <pre>
 196 believes (z said (g2 (g thinks (g cute she)) she) mary) john
 197
 198 ~~> believes (said (thinks (cute mary) he) mary) john
 199 </pre>
 200
 201 As usual, there is a trail of *g*'s leading from the pronoun up to the
 202 *z*.  Next, we build a trail from the other pronoun ("he") to its
 203 binder ("John").
 204
 205 <pre>
 206 believes
 207   said
 208     thinks (cute she) he
 209     Mary
 210   John
 211
 212 believes
 213   z said
 214     (g2 ((g thinks) (g cute she))) he
 215     Mary
 216   John
 217
 218 z believes
 219   (g2 (g (z said)
 220          (g (g2 ((g thinks) (g cute she)))
 221             he))
 222       Mary)
 223   John
 224 </pre>
 225
 226 In the first interation, we build a chain of *g*'s and *g2*'s from the
 227 pronoun to be bound ("she") out to the level of the first argument of
 228 *said*.
 229
 230 In the second iteration, we treat the entire structure as ordinary
 231 functions and arguments, without "seeing" the monadic region.  Once
 232 again, we build a chain of *g*'s and *g2*'s from the currently
 233 targeted pronoun ("he") out to the level of the first argument of
 234 *believes*.  (The new *g*'s and *g2*'s are the three leftmost).
 235
 236 <pre>
 237 z believes (g2 (g (z said) (g (g2 ((g thinks) (g cute she))) he)) mary) john
 238
 239 ~~> believes (said (thinks (cute mary) john) mary) john
 240 </pre>
 241
 242 Obviously, we can repeat this strategy for any configuration of pronouns
 243 and binders.
 244
 245 This binding strategy is strongly reminiscent of the translation from
 246 the lambda calculus into Combinatory Logic that we studied earlier
 247 (see the lecture notes for week 2).  Recall that bound pronouns ended
 248 up translating to I, the identity combinator, just like Jacobson's
 249 identity functions for pronouns; abstracts (\a.M) whose body M did not
 250 contain any occurrences of the pronoun to be bound translated as KM,
 251 just like our unit, K; and abstracts of the form (\a.MN) translated to
 252 S[\aM][\aN], just like our ap rule.
 253