X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week8.mdwn;fp=week8.mdwn;h=0000000000000000000000000000000000000000;hp=e285451add14ef6b1fb8d0d9900e93a2a9ed1d28;hb=fd698b815e417dec463cb0f0e9ed056ab83daed6;hpb=573a8b36ce653c84c2aecb2b81ef99128cb41d13
diff --git a/week8.mdwn b/week8.mdwn
deleted file mode 100644
index e285451a..00000000
--- a/week8.mdwn
+++ /dev/null
@@ -1,239 +0,0 @@
-[[!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 variable. It will turn out that Jacobson's geach combinator
-*g* is exactly our `lift` operator, and her binding combinator *z* is
-exactly our `bind` with the arguments reversed!
-
-Jacobson's system contains two main combinators, *g* and *z*. She
-calls *g* the Geach rule, and *z* performs binding. Here is a typical
-computation. This implementation is 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 he = \x. x in
-let everyone = \P. FORALL x (P 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 (see additional comments below). We'll return to
-the idea of pronouns as identity functions in later discussions.
-
-Second, *g* plays the role of transmitting a binding dependency for an
-embedded constituent to a containing constituent.
-
-Third, one of the peculiar aspects of Jacobson's system is that
-binding is accomplished not by applying *z* to the element that will
-(in some pre-theoretic sense) bind the pronoun, here, *everyone*, but
-rather by applying *z* instead to the predicate that will take
-*everyone* as an argument, here, *thinks*.
-
-The basic recipe in Jacobson's system, then, 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*. (There are examples with longer chains of *g*'s below.)
-
-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 here in order to
-emphasize its similarities with Jacboson's geach combinator.)
-
-This monad boxes 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.
-
-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 be used to replace the pronoun
-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 letting `t a f = f a`) is
-
-
-everyone (z thinks (g left he))
-
-~~> forall w (thinks (left w) w)
-
-everyone (z thinks (g (t 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.
-
-Binding more than one variable at a time
-----------------------------------------
-
-It requires some cleverness to use the link monad to bind more than
-one variable at a time. Whereas in the standard Reader monad a single
-environment can record any number of variable assignments, because
-Jacobson's monad only tracks a single dependency, binding more than
-one pronoun requires layering the monad. (Jacobson provides some
-special combinators, but we can make do with the ingredients already
-defined.)
-
-Let's take the following sentence as our target, with the obvious
-binding relationships:
-
-
- John believes Mary said he thinks she's cute.
- | | | |
- | |---------|---------|
- | |
- |-----------------------|
-
-
-It will be convenient to
-have a counterpart to the lift operation that combines a monadic
-functor with a non-monadic argument:
-
-
- let g f v = ap (unit f) v;;
- let g2 u a = ap u (unit a);;
-
-
-As a first step, we'll bind "she" by "Mary":
-
-
-believes (z said (g2 (g thinks (g cute she)) she) mary) john
-
-~~> believes (said (thinks (cute mary) he) mary) john
-
-
-As usual, there is a trail of *g*'s leading from the pronoun up to the
-*z*. Next, we build a trail from the other pronoun ("he") to its
-binder ("John").
-
-
-believes
- said
- thinks (cute she) he
- Mary
- John
-
-believes
- z said
- (g2 ((g thinks) (g cute she))) he
- Mary
- John
-
-z believes
- (g2 (g (z said)
- (g (g2 ((g thinks) (g cute she)))
- he))
- Mary)
- John
-
-
-In the first interation, we build a chain of *g*'s and *g2*'s from the
-pronoun to be bound ("she") out to the level of the first argument of
-*said*.
-
-In the second iteration, we treat the entire structure as ordinary
-functions and arguments, without "seeing" the monadic region. Once
-again, we build a chain of *g*'s and *g2*'s from the currently
-targeted pronoun ("he") out to the level of the first argument of
-*believes*. (The new *g*'s and *g2*'s are the three leftmost).
-
-
-z believes (g2 (g (z said) (g (g2 ((g thinks) (g cute she))) he)) mary) john
-
-~~> believes (said (thinks (cute mary) john) mary) john
-
-
-Obviously, we can repeat this strategy for any configuration of pronouns
-and binders.
-
-This binding strategy is strongly reminiscent of the translation from
-the lambda calculus into Combinatory Logic that we studied earlier
-(see the lecture notes for week 2). Recall that bound pronouns ended
-up translating to I, the identity combinator, just like Jacobson's
-identity functions for pronouns; abstracts (\a.M) whose body M did not
-contain any occurrences of the pronoun to be bound translated as KM,
-just like our unit, which you will recognize as an instance of K; and
-abstracts of the form (\a.MN) translated to S[\aM][\aN], just like our
-ap rule.