X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week8.mdwn;h=e285451add14ef6b1fb8d0d9900e93a2a9ed1d28;hp=4388e4407626df6f2452663fae7f82d4aeefe003;hb=HEAD;hpb=2f32f675472a4cef4f4d6bf47c8531946a717760
diff --git a/week8.mdwn b/week8.mdwn
deleted file mode 100644
index 4388e440..00000000
--- a/week8.mdwn
+++ /dev/null
@@ -1,158 +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 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 which following Curry and Steedman, I'll call *T*, which
-we'll make use of to adjust function/argument order to better match
-English word order; N.B., though, that Jacobson's name for this
-combinator is "lift", but it is different from the monadic lift
-discussed in some detail below.) 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 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. 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 *g* in the next most deeply
-embedded constituent (*said he left*), and so on (see below).
-
-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 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.