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