1 [[!toc]]
4 ---------------------------------------------------------------
6 Jacobson's Variable-Free Semantics (e.g., Jacobson 1999, [Towards a
7 Variable-Free
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
13 assignment function threaded through the computation is limited to at
14 most one assignment.
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):
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))
33 ~~>  FORALL x (thinks (left x) x)
34 </pre>
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.
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*).
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*.
58 Last week we saw a reader monad for tracking variable assignments:
60 <pre>
61 type env = (char * int) list;;
62 type 'a reader = env -> 'a;;
63 let unit x = fun (e : env) -> x;;
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>
71 (We've used a simplified term for the bind function in order to
72 emphasize its similarities with Jacboson's geach combinator.)
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.
80 can consider the following monad:
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>
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`.)
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.
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.
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
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.
119 Furthermore, Jacobson's *z* combinator, which is what she uses to
121 `bind`!  Interestingly, the types are different, at least at a
122 conceptual level.  Here they are side by side:
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>
129 `Bind` takes an `'a link`, and a function that maps an `'a` to a `'b
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.
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
141 <pre>
142 everyone (z thinks (g left he))
144 ~~> forall w (thinks (left w) w)
146 everyone (z thinks (g (l bill) (g said (g left he))))
148 ~~> forall w (thinks (said (left w) bill) w)
149 </pre>
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