From b7a09b298589d5965edea1fd051c22fb69b42b62 Mon Sep 17 00:00:00 2001 From: Chris Barker Date: Sun, 7 Nov 2010 21:28:46 -0500 Subject: [PATCH] Jacobson as a monad --- week8.mdwn | 156 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 156 insertions(+) create mode 100644 week8.mdwn diff --git a/week8.mdwn b/week8.mdwn new file mode 100644 index 00000000..1a0b55bb --- /dev/null +++ b/week8.mdwn @@ -0,0 +1,156 @@ +[[!toc]] + +Jacobson's Variable-Free Semantics as a bare-bones Reader Monad +--------------------------------------------------------------- + +Jacobson's Variable-Free Semantics (e.g., Jacobson 1999, [Towards a +Variable-Free +Semantics](http://www.springerlink.com/content/j706674r4w217jj5/)) +uses combinators to impose binding relationships between argument +positions. The system does not make use of assignment functions or +variables. We'll see that from the point of view of our discussion of +monads, Jacobson's system is essentially a reader monad in which the +assignment function threaded through the computation is limited to at +most one assignment. + +Jacobson's system contains two main combinators, *g* and *z*. She +calls *g* the Geach rule, and *z* effects binding. (There is a third +combinator, *l*, which adjusts function/argument order when the +argument precedes its functor, but we'll finesse that here by freely +reordering the English predicates so that functors always precede +their arguments.) Here is a typical computation (based closely on +email from Simon Charlow, with beta reduction as performed by the +on-line evaluator): + +
+; Analysis of "Everyone_i thinks he_i left"
+let g = \f g x. f (g x) in
+let z = \f g x. f (g x) x in
+let everyone = \P. FORALL x (P x) in
+let he = \x. x in
+everyone ((z thinks) (g left he))
+
+~~>  FORALL x (thinks (left x) x)
+
+ +Several things to notice: First, pronouns denote identity functions. +As Jeremy Kuhn has pointed out, this is related to the fact that in +the mapping from the lambda calculus into combinatory logic that we +discussed earlier in the course, bound variables translated to I, the +identity combinator. This is a point we'll return to in later +discussions. + +Second, *g* plays the role of transmitting a binding dependency for an +embedded constituent to a containing constituent. If the sentence had +been *Everyone_i thinks Bill said he_i left*, there would be an +occurrence of *g* in the most deeply embedded clause (*he left*), and +another occurrence of (a variant of) *g* in the next most deeply +embedded clause (*Bill said he left*). + +Third, binding is accomplished by applying *z* not to the element that +will (in some pre-theoretic sense) bind the pronoun, here, *everyone*, +but by applying *z* instead to the predicate that will take *everyone* +as an argument, here, *thinks*. The basic recipe in Jacobson's system +is that you transmit the dependence of a pronoun upwards through the +tree using *g* until just before you are about to combine with the +binder, when you finish off with *z*. + +Last week we saw a reader monad for tracking variable assignments: + +
+type env = (char * int) list;;
+type 'a reader = env -> 'a;;
+let unit x = fun (e : env) -> x;;
+let bind (u : 'a reader) (f: 'a -> 'b reader) : 'b reader =
+    fun (e : env) -> f (u e) e;;
+let shift (c : char) (v : int reader) (u : 'a reader) =
+    fun (e : env) -> u ((c, v e) :: e);;
+let lookup (c : char) : int reader = fun (e : env) -> List.assoc c e;;
+
+ +(We've used a simplified term for the bind function in order to +emphasize its similarities with Jacboson's geach combinator.) + +This monad boxed up a value along with an assignment function, where +an assignemnt function was implemented as a list of `char * int`. The +idea is that a list like `[('a', 2); ('b',5)]` associates the variable +`'a'` with the value 2, and the variable `'b'` with the value 5. + +Combining this reader monad with ideas from Jacobson's approach, we +can consider the following monad: + +
+type e = int;;
+type 'a link = e -> 'a;;
+let unit (a:'a): 'a link = fun x -> a;;
+let bind (u: 'a link) (f: 'a -> 'b link) : 'b link = fun (x:e) -> f (u x) x;;
+let ap (u: ('a -> 'b) link) (v: 'a link) : 'b link = fun (x:e) -> u x (v x);;
+let lift (f: 'a -> 'b) (u: 'a link): ('b link) = ap (unit f) u;;
+let g = lift;;
+let z (f: 'a -> e -> 'b) (u: 'a link) : e -> 'b = fun (x:e) -> f (u x) x;;
+
+ +I've called this the *link* monad, because it links (exactly one) +pronoun with a binder, but it's a kind of reader monad. (Prove that +`ap`, the combinator for applying a linked functor to a linked object, +can be equivalently defined in terms of `bind` and `unit`.) + +In order to keep the types super simple, I've assumed that the only +kind of value that can be linked into a structure is an individual of +type `e`. It is easy to make the monad polymorphic in the type of the +linked value, which will be necessary to handle, e.g., paycheck pronouns. + +Note that in addition to `unit` being Curry's K combinator, this `ap` +is the S combinator. Not coincidentally, recall that the rule for +converting an arbitrary application `M N` into Combinatory Logic is `S +[M] [N]`, where `[M]` is the CL translation of `M` and `[N]` is the CL +translation of `N`. There, as here, the job of `ap` is to take an +argument and make it available for any pronouns (variables) in the two +components of the application. + +In the standard reader monad, the environment is an assignment +function. Here, instead this monad provides a single value. The idea +is that this is the value that will replace the pronouns linked to it +by the monad. + +Jacobson's *g* combinator is exactly our `lift` operator: it takes a +functor and lifts it into the monad. Surely this is more than a coincidence. + +Furthermore, Jacobson's *z* combinator, which is what she uses to +create binding links, is essentially identical to our reader-monad +`bind`! Interestingly, the types are different, at least at a +conceptual level. Here they are side by side: + +
+let bind (u: 'a link) (f: 'a -> 'b link) : 'b link = fun (x:e) -> f (u x) x;;
+let z (f: 'a -> e -> 'b) (u: 'a link) : e -> 'b = fun (x:e) -> f (u x) x;;
+
+ +`Bind` takes an `'a link`, and a function that maps an `'a` to a `'b +link`, and returns a `'b link`, i.e., the result is in the link monad. +*z*, on the other hand, takes the same two arguments (in reverse +order), but returns something that is not in the monad. Rather, it +will be a function from individuals to a computation in which the +pronoun in question is bound to that individual. We could emphasize +the parallel with the reader monad even more by writing a `shift` +operator that used `unit` to produce a monadic result, if we wanted to. + +The monad version of *Everyone_i thinks he_i left*, then (remembering +that `he = fun x -> x`, and that `l a f = f a`) is + +
+everyone (z thinks (g left he))
+
+~~> forall w (thinks (left w) w)
+
+everyone (z thinks (g (l bill) (g said (g left he))))
+
+~~> forall w (thinks (said (left w) bill) w)
+
+ +So *g* is exactly `lift` (a combination of `bind` and `unit`), and *z* +is exactly `bind` with the arguments reversed. It appears that +Jacobson's variable-free semantics is essentially a reader monad. + +One of Jacobson's main points survives: restricting the reader monad +to a single-value environment eliminates the need for variable names. -- 2.11.0