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 variable.  It will turn out that 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* performs binding.  Here is a typical
  20 computation.  This implementation is based closely on email from Simon
  21 Charlow, with beta reduction as performed by the on-line evaluator:
  22
  23 <pre>
  24 ; Analysis of "Everyone_i thinks he_i left"
  25 let g = \f g x. f (g x) in
  26 let z = \f g x. f (g x) x in
  27 let he = \x. x in
  28 let everyone = \P. FORALL x (P x) in
  29
  30 everyone (z thinks (g left he))
  31
  32 ~~>  FORALL x (thinks (left x) x)
  33 </pre>
  34
  35 Several things to notice: First, pronouns denote identity functions.
  36 As Jeremy Kuhn has pointed out, this is related to the fact that in
  37 the mapping from the lambda calculus into combinatory logic that we
  38 discussed earlier in the course, bound variables translated to I, the
  39 identity combinator (see additional comments below).  We'll return to
  40 the idea of pronouns as identity functions in later discussions.
  41
  42 Second, *g* plays the role of transmitting a binding dependency for an
  43 embedded constituent to a containing constituent.
  44
  45 Third, one of the peculiar aspects of Jacobson's system is that
  46 binding is accomplished not by applying *z* to the element that will
  47 (in some pre-theoretic sense) bind the pronoun, here, *everyone*, but
  48 rather by applying *z* instead to the predicate that will take
  49 *everyone* as an argument, here, *thinks*.
  50
  51 The basic recipe in Jacobson's system, then, is that you transmit the
  52 dependence of a pronoun upwards through the tree using *g* until just
  53 before you are about to combine with the binder, when you finish off
  54 with *z*.  (There are examples with longer chains of *g*'s below.)
  55
  56 Last week we saw a reader monad for tracking variable assignments:
  57
  58 <pre>
  59 type env = (char * int) list;;
  60 type 'a reader = env -> 'a;;
  61 let unit x = fun (e : env) -> x;;
  62 let bind (u : 'a reader) (f: 'a -> 'b reader) : 'b reader =
  63     fun (e : env) -> f (u e) e;;
  64 let shift (c : char) (v : int reader) (u : 'a reader) =
  65     fun (e : env) -> u ((c, v e) :: e);;
  66 let lookup (c : char) : int reader = fun (e : env) -> List.assoc c e;;
  67 </pre>
  68
  69 (We've used a simplified term for the bind function here in order to
  70 emphasize its similarities with Jacboson's geach combinator.)
  71
  72 This monad boxes up a value along with an assignment function, where
  73 an assignemnt function was implemented as a list of `char * int`.  The
  74 idea is that a list like `[('a', 2); ('b',5)]` associates the variable
  75 `'a'` with the value 2, and the variable `'b'` with the value 5.
  76
  77 Combining this reader monad with ideas from Jacobson's approach, we
  78 can consider the following monad:
  79
  80 <pre>
  81 type e = int;;
  82 type 'a link = e -> 'a;;
  83 let unit (a:'a): 'a link = fun x -> a;;
  84 let bind (u: 'a link) (f: 'a -> 'b link) : 'b link = fun (x:e) -> f (u x) x;;
  85 let ap (u: ('a -> 'b) link) (v: 'a link) : 'b link = fun (x:e) -> u x (v x);;
  86 let lift (f: 'a -> 'b) (u: 'a link): ('b link) = ap (unit f) u;;
  87 let g = lift;;
  88 let z (f: 'a -> e -> 'b) (u: 'a link) : e -> 'b = fun (x:e) -> f (u x) x;;
  89 </pre>
  90
  91 I've called this the *link* monad, because it links (exactly one)
  92 pronoun with a binder, but it's a kind of reader monad.  (Prove that
  93 `ap`, the combinator for applying a linked functor to a linked object,
  94 can be equivalently defined in terms of `bind` and `unit`.)
  95
  96 In order to keep the types super simple, I've assumed that the only
  97 kind of value that can be linked into a structure is an individual of
  98 type `e`.  It is easy to make the monad polymorphic in the type of the
  99 linked value, which will be necessary to handle, e.g., paycheck pronouns.
 100
 101 In the standard reader monad, the environment is an assignment
 102 function.  Here, instead this monad provides a single value.  The idea
 103 is that this is the value that will be used to replace the pronoun
 104 linked to it by the monad.
 105
 106 Jacobson's *g* combinator is exactly our `lift` operator: it takes a
 107 functor and lifts it into the monad.  Surely this is more than a coincidence.
 108
 109 Furthermore, Jacobson's *z* combinator, which is what she uses to
 110 create binding links, is essentially identical to our reader-monad
 111 `bind`!  Interestingly, the types are different, at least at a
 112 conceptual level.  Here they are side by side:
 113
 114 <pre>
 115 let bind (u: 'a link) (f: 'a -> 'b link) : 'b link = fun (x:e) -> f (u x) x;;
 116 let z (f: 'a -> e -> 'b) (u: 'a link) : e -> 'b = fun (x:e) -> f (u x) x;;
 117 </pre>
 118
 119 `Bind` takes an `'a link`, and a function that maps an `'a` to a `'b
 120 link`, and returns a `'b link`, i.e., the result is in the link monad.
 121 *z*, on the other hand, takes the same two arguments (in reverse
 122 order), but returns something that is not in the monad.  Rather, it
 123 will be a function from individuals to a computation in which the
 124 pronoun in question is bound to that individual.  We could emphasize
 125 the parallel with the reader monad even more by writing a `shift`
 126 operator that used `unit` to produce a monadic result, if we wanted to.
 127
 128 The monad version of *Everyone_i thinks he_i left*, then (remembering
 129 that `he = fun x -> x`, and letting `t a f = f a`) is
 130
 131 <pre>
 132 everyone (z thinks (g left he))
 133
 134 ~~> forall w (thinks (left w) w)
 135
 136 everyone (z thinks (g (t bill) (g said (g left he))))
 137
 138 ~~> forall w (thinks (said (left w) bill) w)
 139 </pre>
 140
 141 So *g* is exactly `lift` (a combination of `bind` and `unit`), and *z*
 142 is exactly `bind` with the arguments reversed.  It appears that
 143 Jacobson's variable-free semantics is essentially a reader monad.
 144
 145 One of Jacobson's main points survives: restricting the reader monad
 146 to a single-value environment eliminates the need for variable names.
 147
 148 Binding more than one variable at a time
 149 ----------------------------------------
 150
 151 It requires some cleverness to use the link monad to bind more than
 152 one variable at a time.  Whereas in the standard reader monad a single
 153 environment can record any number of variable assignments, because
 154 Jacobson's monad only tracks a single dependency, binding more than
 155 one pronoun requires layering the monad.  (Jacobson provides some
 156 special combinators, but we can make do with the ingredients already
 157 defined.)
 158
 159 Let's take the following sentence as our target, with the obvious
 160 binding relationships:
 161
 162 <pre>
 163     John believes Mary said he thinks she's cute.
 164      |             |         |         |
 165      |             |---------|---------|
 166      |                       |
 167      |-----------------------|
 168 </pre>
 169
 170 It will be convenient to
 171 have a counterpart to the lift operation that combines a monadic
 172 functor with a non-monadic argument:
 173
 174 <pre>
 175     let g f v = ap (unit f) v;;
 176     let g2 u a = ap u (unit a);;
 177 </pre>
 178
 179 As a first step, we'll bind "she" by "Mary":
 180
 181 <pre>
 182 believes (z said (g2 (g thinks (g cute she)) she) mary) john
 183
 184 ~~> believes (said (thinks (cute mary) he) mary) john
 185 </pre>
 186
 187 As usual, there is a trail of *g*'s leading from the pronoun up to the
 188 *z*.  Next, we build a trail from the other pronoun ("he") to its
 189 binder ("John").
 190
 191 <pre>
 192 believes
 193   said
 194     thinks (cute she) he
 195     Mary
 196   John
 197
 198 believes
 199   z said
 200     (g2 ((g thinks) (g cute she))) he
 201     Mary
 202   John
 203
 204 z believes
 205   (g2 (g (z said)
 206          (g (g2 ((g thinks) (g cute she)))
 207             he))
 208       Mary)
 209   John
 210 </pre>
 211
 212 In the first interation, we build a chain of *g*'s and *g2*'s from the
 213 pronoun to be bound ("she") out to the level of the first argument of
 214 *said*.
 215
 216 In the second iteration, we treat the entire structure as ordinary
 217 functions and arguments, without "seeing" the monadic region.  Once
 218 again, we build a chain of *g*'s and *g2*'s from the currently
 219 targeted pronoun ("he") out to the level of the first argument of
 220 *believes*.  (The new *g*'s and *g2*'s are the three leftmost).
 221
 222 <pre>
 223 z believes (g2 (g (z said) (g (g2 ((g thinks) (g cute she))) he)) mary) john
 224
 225 ~~> believes (said (thinks (cute mary) john) mary) john
 226 </pre>
 227
 228 Obviously, we can repeat this strategy for any configuration of pronouns
 229 and binders.
 230
 231 This binding strategy is strongly reminiscent of the translation from
 232 the lambda calculus into Combinatory Logic that we studied earlier
 233 (see the lecture notes for week 2).  Recall that bound pronouns ended
 234 up translating to I, the identity combinator, just like Jacobson's
 235 identity functions for pronouns; abstracts (\a.M) whose body M did not
 236 contain any occurrences of the pronoun to be bound translated as KM,
 237 just like our unit, which you will recognize as an instance of K; and
 238 abstracts of the form (\a.MN) translated to S[\aM][\aN], just like our
 239 ap rule.