Merge branch 'working'
authorJim <jim.pryor@nyu.edu>
Mon, 6 Apr 2015 18:45:34 +0000 (14:45 -0400)
committerJim <jim.pryor@nyu.edu>
Mon, 6 Apr 2015 18:45:34 +0000 (14:45 -0400)
* working:
  remove old binding page

exercises/assignment8-9.mdwn
index.mdwn
topics/week8_reader_monad.mdwn

index c41ee9b..fbdeb85 100644 (file)
@@ -14,20 +14,21 @@ relationships, as in
 
         John_x thinks Mary_y said he_x likes her_y.
 
-    See her 1999 paper for details.
+    See her 1999 paper for details. Essentially, she ends up layering several
+Reader monads over each other.
 
     Here is [[code for the arithmetic tree Chris presented in week 8|code/arith1.ml]]. It computes
-`\x. (+ 1 (* (/ 6 x) 4))`.  Your task is to modify it to compute
-`\x y. (+ 1 (* (/ 6 x) y))`.  You will need to modify five lines.
+`\n. (+ 1 (* (/ 6 n) 4))`.  Your task is to modify it to compute
+`\n m. (+ 1 (* (/ 6 n) m))`.  You will need to modify five lines.
 The first one is the type of a boxed int.  Instead of `type num = int
 -> int`, you'll need
 
         type num = int -> int -> int
 
     The second and third are the definitions of `mid` and `map2`. The fourth
-is the one that encodes the variable `x`, the line that begins `(Leaf
-(Num (fun x -> ...`.  The fifth line you need to modify is the one
-that replaces "4" with "y".  When you have these lines modified,
+is the one that encodes the variable `n`, the line that begins `(Leaf
+(Num (fun n -> ...`.  The fifth line you need to modify is the one
+that replaces "4" with "m".  When you have these lines modified,
 you should be able to execute the following expression:
 
         # match eval t2 with Leaf (Num f) -> f 2 4;;
index 7230010..1b9e672 100644 (file)
@@ -179,6 +179,7 @@ We've posted a [[State Monad Tutorial]].
 
 (**Week 10**) Thursday April 9
 
+> Topics: We will be discussing the reading posted above.
 
 
 
index 492f7a3..93e2086 100644 (file)
@@ -449,7 +449,11 @@ arguments reversed (i.e., `(z k xx) == (xx >>= k)`).
 
 (The `T` combinator in the derivations above is given by `T x <~~> \f. f x`;
 it handles situations in which English word order reverses
-the usual function/argument order.)
+the usual function/argument order. `T` is what Curry and Steedman call this
+combinator. Jacobson calls it "lift", but it shouldn't be confused with the
+`mid` and `map` operations that lift values into the Reader monad we're focusing
+on here. It does lift values into a *different* monad, that we'll consider in
+a few weeks.)
 
 In other words, 
 Jacobson's variable-free semantics is essentially a Reader monad.
@@ -568,7 +572,7 @@ Now we add intensions. Because different people leave in different
 worlds, the meaning of *leave* must depend on the world in which it is
 being evaluated:
 
-    let left (x:e) (w:s) = match (x, w) with ('c', 2) -> false | _ -> true
+    let left (x : e) (w : s) = match (x, w) with ('c', 2) -> false | _ -> true
     left ann 1 (* true: Ann left in world 1 *)
     left cam 2 (* false: Cam didn't leave in world 2 *) 
 
@@ -630,21 +634,23 @@ in action:
     (mid cam >>= left) 2  (* false: Cam didn't leave in world 2 *)
 
 As usual, `>>=` takes a monadic box containing Ann, extracts Ann, and
-feeds her to the extensional *left*. In linguistic terms, we take the
+feeds her to the function *left*. In linguistic terms, we take the
 individual concept `mid ann`, apply it to the world of evaluation in
 order to get hold of an individual (`'a'`), then feed that individual
-to the extensional predicate *left*.
+to the predicate *left*.
 
 We can arrange for a transitive verb that is extensional in both of
 its arguments to take intensional arguments:
 
-    let map2' f xx yy = xx >>= (fun x -> yy >>= (fun y -> f x y))
+<pre>
+let map2' f xx yy = xx >>= (fun x -> yy >>= (fun y -> <span class=ul>f x y</span>))
+</pre>
 
 This is almost the same `map2` predicate we defined in order to allow
-addition in our division monad example. The difference is that this
+addition in our division monad example. The *difference* is that this
 variant operates on verb meanings that take extensional arguments but
 returns an intensional result. Thus the original `map2` predicate
-has `mid (f x y)` where we have just `f x y` here.
+has `mid (f x y)` where we have just <code><span class=ul>f x y</span></code> here.
 
 The use of `>>=` here to combine *left* with an individual concept,
 and the use of `map2'` to combine *see* with two intensional
@@ -660,12 +666,12 @@ map2' saw (mid bill) (mid ann) 2  (* false *)
 Ann did see Bill in world 1, but Ann didn't see Bill in world 2.
 
 Finally, we can define our intensional verb *thinks*. *Think* is
-intensional with respect to its sentential complement, though still extensional
-with respect to its subject. (As Montague noticed, almost all verbs
+intensional with respect to its sentential complement (it takes complements of type `s -> t`), though still extensional
+with respect to its subject (type `e`). (As Montague noticed, almost all verbs
 in English are extensional with respect to their subject; a possible
 exception is *appear*.)
 
-    let thinks (p:s->t) (x:e) (w:s) = 
+    let thinks (p : s->t) (x : e) (w : s) = 
       match (x, p 2) with ('a', false) -> false | _ -> p w
 
 In every world, Ann fails to believe any proposition that is false in world 2.
@@ -691,4 +697,6 @@ he didn't leave in world 2, so Ann doesn't in world 1 believe that Cam left:
  (using `mbind`), and the non-intersective adjectives will take
  intensional arguments.
 
+**Connections with variable binding**: the rigid individual concepts generated by `mid ann` and the like correspond to the numerical constants, that don't interact with the environment in any way, in the variable binding examples we considered earlier on the page. If we had any non-contingent predicates that were wholly insensitive to intensional effects, they would be modeled using `map2` and would correspond to the operations like `map2 (+)` in the earlier examples. As it is, our predicates *lift* and *saw*, though only sensitive to the *extension* of their arguments, nonetheless *are* sensitive to the world of evaluation for their `bool` output. So these are somewhat akin, at the predicate level, to expressions like `var_n`, at the singular term level, in the variable bindings examples. Our predicate *thinks* shows yet a further kind of interaction with the intensional structures we introduced: namely, its output can depend upon evaluating its complement relative to other possible worlds. We didn't discuss analogues of this in the variable binding case, but they exist: namely, they are expressions like `let x = 2 in ...` and `forall x ...`, that have the effect of supplying their arguments with an environment or assignment function that is shifted from the one they are themselves being evaluated with.
+
 notes: cascade, general env