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.
  15
  16 Jacobson's system contains two main combinators, *g* and *z*.  She
  17 calls *g* the Geach rule, and *z* effects binding.  (There is a third
  18 combinator which following Curry and Steedman, I'll call *T*, which
  19 we'll make use of to adjust function/argument order to better match
  20 English word order; N.B., though, that Jacobson's name for this
  21 combinator is "lift", but it is different from the monadic lift
  22 discussed in some detail below.)  Here is a typical computation (based
  23 closely on email from Simon Charlow, with beta reduction as performed
  24 by the on-line evaluator):
  25
  26 <pre>
  27 ; Analysis of "Everyone_i thinks he_i left"
  28 let g = \f g x. f (g x) in
  29 let z = \f g x. f (g x) x in
  30 let he = \x. x in
  31 let everyone = \P. FORALL x (P x) in
  32
  33 everyone (z thinks (g left he))
  34
  35 ~~>  FORALL x (thinks (left x) x)
  36 </pre>
  37
  38 Several things to notice: First, pronouns denote identity functions.
  39 As Jeremy Kuhn has pointed out, this is related to the fact that in
  40 the mapping from the lambda calculus into combinatory logic that we
  41 discussed earlier in the course, bound variables translated to I, the
  42 identity combinator.  This is a point we'll return to in later
  43 discussions.
  44
  45 Second, *g* plays the role of transmitting a binding dependency for an
  46 embedded constituent to a containing constituent.  If the sentence had
  47 been *Everyone_i thinks Bill said he_i left*, there would be an
  48 occurrence of *g* in the most deeply embedded clause (*he left*), and
  49 another occurrence of *g* in the next most deeply
  50 embedded constituent (*said he left*), and so on (see below).
  51
  52 Third, binding is accomplished by applying *z* not to the element that
  53 will (in some pre-theoretic sense) bind the pronoun, here, *everyone*,
  54 but by applying *z* instead to the predicate that will take *everyone*
  55 as an argument, here, *thinks*.  The basic recipe in Jacobson's system
  56 is that you transmit the dependence of a pronoun upwards through the
  57 tree using *g* until just before you are about to combine with the
  58 binder, when you finish off with *z*.
  59
  60 Last week we saw a reader monad for tracking variable assignments:
  61
  62 <pre>
  63 type env = (char * int) list;;
  64 type 'a reader = env -> 'a;;
  65 let unit x = fun (e : env) -> x;;
  66 let bind (u : 'a reader) (f: 'a -> 'b reader) : 'b reader =
  67     fun (e : env) -> f (u e) e;;
  68 let shift (c : char) (v : int reader) (u : 'a reader) =
  69     fun (e : env) -> u ((c, v e) :: e);;
  70 let lookup (c : char) : int reader = fun (e : env) -> List.assoc c e;;
  71 </pre>
  72
  73 (We've used a simplified term for the bind function in order to
  74 emphasize its similarities with Jacboson's geach combinator.)
  75
  76 This monad boxed up a value along with an assignment function, where
  77 an assignemnt function was implemented as a list of `char * int`.  The
  78 idea is that a list like `[('a', 2); ('b',5)]` associates the variable
  79 `'a'` with the value 2, and the variable `'b'` with the value 5.
  80
  81 Combining this reader monad with ideas from Jacobson's approach, we
  82 can consider the following monad:
  83
  84 <pre>
  85 type e = int;;
  86 type 'a link = e -> 'a;;
  87 let unit (a:'a): 'a link = fun x -> a;;
  88 let bind (u: 'a link) (f: 'a -> 'b link) : 'b link = fun (x:e) -> f (u x) x;;
  89 let ap (u: ('a -> 'b) link) (v: 'a link) : 'b link = fun (x:e) -> u x (v x);;
  90 let lift (f: 'a -> 'b) (u: 'a link): ('b link) = ap (unit f) u;;
  91 let g = lift;;
  92 let z (f: 'a -> e -> 'b) (u: 'a link) : e -> 'b = fun (x:e) -> f (u x) x;;
  93 </pre>
  94
  95 I've called this the *link* monad, because it links (exactly one)
  96 pronoun with a binder, but it's a kind of reader monad.  (Prove that
  97 `ap`, the combinator for applying a linked functor to a linked object,
  98 can be equivalently defined in terms of `bind` and `unit`.)
  99
 100 In order to keep the types super simple, I've assumed that the only
 101 kind of value that can be linked into a structure is an individual of
 102 type `e`.  It is easy to make the monad polymorphic in the type of the
 103 linked value, which will be necessary to handle, e.g., paycheck pronouns.
 104
 105 Note that in addition to `unit` being Curry's K combinator, this `ap`
 106 is the S combinator.  Not coincidentally, recall that the rule for
 107 converting an arbitrary application `M N` into Combinatory Logic is `S
 108 [M] [N]`, where `[M]` is the CL translation of `M` and `[N]` is the CL
 109 translation of `N`.  There, as here, the job of `ap` is to take an
 110 argument and make it available for any pronouns (variables) in the two
 111 components of the application.
 112
 113 In the standard reader monad, the environment is an assignment
 114 function.  Here, instead this monad provides a single value.  The idea
 115 is that this is the value that will replace the pronouns linked to it
 116 by the monad.
 117
 118 Jacobson's *g* combinator is exactly our `lift` operator: it takes a
 119 functor and lifts it into the monad.  Surely this is more than a coincidence.
 120
 121 Furthermore, Jacobson's *z* combinator, which is what she uses to
 122 create binding links, is essentially identical to our reader-monad
 123 `bind`!  Interestingly, the types are different, at least at a
 124 conceptual level.  Here they are side by side:
 125
 126 <pre>
 127 let bind (u: 'a link) (f: 'a -> 'b link) : 'b link = fun (x:e) -> f (u x) x;;
 128 let z (f: 'a -> e -> 'b) (u: 'a link) : e -> 'b = fun (x:e) -> f (u x) x;;
 129 </pre>
 130
 131 `Bind` takes an `'a link`, and a function that maps an `'a` to a `'b
 132 link`, and returns a `'b link`, i.e., the result is in the link monad.
 133 *z*, on the other hand, takes the same two arguments (in reverse
 134 order), but returns something that is not in the monad.  Rather, it
 135 will be a function from individuals to a computation in which the
 136 pronoun in question is bound to that individual.  We could emphasize
 137 the parallel with the reader monad even more by writing a `shift`
 138 operator that used `unit` to produce a monadic result, if we wanted to.
 139
 140 The monad version of *Everyone_i thinks he_i left*, then (remembering
 141 that `he = fun x -> x`, and letting `t a f = f a`) is
 142
 143 <pre>
 144 everyone (z thinks (g left he))
 145
 146 ~~> forall w (thinks (left w) w)
 147
 148 everyone (z thinks (g (t bill) (g said (g left he))))
 149
 150 ~~> forall w (thinks (said (left w) bill) w)
 151 </pre>
 152
 153 So *g* is exactly `lift` (a combination of `bind` and `unit`), and *z*
 154 is exactly `bind` with the arguments reversed.  It appears that
 155 Jacobson's variable-free semantics is essentially a reader monad.
 156
 157 One of Jacobson's main points survives: restricting the reader monad
 158 to a single-value environment eliminates the need for variable names.