Jacobson as a monad

diff --git a/week8.mdwn b/week8.mdwn
index e99e223..27308c9 100644 (file)
--- a/week8.mdwn
+++ b/week8.mdwn
@@ -15,20 +15,22 @@ 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
 
 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 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):
+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):

 
 <pre>
 ; 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
 
 <pre>
 ; 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
 let he = \x. x in

-everyone ((z thinks) (g left he))
+let everyone = \P. FORALL x (P x) in
+
+everyone (z thinks (g left he))

 
 ~~>  FORALL x (thinks (left x) x)
 </pre>
 
 ~~>  FORALL x (thinks (left x) x)
 </pre>


@@ -136,14 +138,14 @@ 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
 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
+that `he = fun x -> x`, and letting `t a f = f a`) is

 
 <pre>
 everyone (z thinks (g left he))
 
 ~~> forall w (thinks (left w) w)
 
 
 <pre>
 everyone (z thinks (g left he))
 
 ~~> forall w (thinks (left w) w)
 

-everyone (z thinks (g (l bill) (g said (g left he))))
+everyone (z thinks (g (t bill) (g said (g left he))))

 
 ~~> forall w (thinks (said (left w) bill) w)
 </pre>
 
 ~~> forall w (thinks (said (left w) bill) w)
 </pre>