author Chris Barker Sat, 27 Nov 2010 04:42:40 +0000 (23:42 -0500) committer Chris Barker Sat, 27 Nov 2010 04:42:40 +0000 (23:42 -0500)

index d13dc35..8c052f0 100644 (file)
@@ -248,3 +248,59 @@ To bad this digression, though it ties together various
elements of the course, has *no relevance whatsoever* to the topic of
continuations.

+Montague's PTQ treatment of DPs as generalized quantifiers
+----------------------------------------------------------
+
+We've hinted that Montague's treatment of DPs as generalized
+quantifiers embodies the spirit of continuations (see de Groote 2001,
+Barker 2002 for lengthy discussion).  Let's see why.
+
+First, we'll need a type constructor.  As you probably know,
+Montague replaced individual-denoting determiner phrases (with type `e`)
+with generalized quantifiers (with [extensional] type `(e -> t) -> t`.
+In particular, the denotation of a proper name like *John*, which
+might originally denote a object `j` of type `e`, came to denote a
+generalized quantifier `fun pred -> pred j` of type `(e -> t) -> t`.
+Let's write a general function that will map individuals into their
+corresponding generalized quantifier:
+
+   gqize (x:e) = fun (p:e->t) -> p x
+
+This function wraps up an individual in a fancy box.  That is to say,
+we are in the presence of a monad.  The type constructor, the unit and
+the bind follow naturally.  We've done this enough times that I won't
+belabor the construction of the bind function, the derivation is
+similar to the List monad just given:
+
+   type 'a continuation = ('a -> 'b) -> 'b
+   c_unit (x:'a) = fun (p:'a -> 'b) -> p x
+   c_bind (u:('a -> 'b) -> 'b) (f: 'a -> ('c -> 'd) -> 'd): ('c -> 'd) -> 'd =
+     fun (k:'a -> 'b) -> u (fun (x:'a) -> f x k)
+
+How similar is it to the List monad?  Let's examine the type
+constructor and the terms from the list monad derived above:
+
+    type ('a, 'b) list' = ('a -> 'b -> 'b) -> 'b -> 'b
+    l'_unit x = fun f -> f x
+    l'_bind u f = fun k -> u (fun x -> f x k)
+
+(I performed a sneaky but valid eta reduction in the unit term.)
+
+The unit and the bind for the Montague continuation monad and the
+homemade List monad are the same terms!  In other words, the behavior
+of the List monad and the behavior of the continuations monad are
+parallel in a deep sense.  To emphasize the parallel, we can
+instantiate the type of the list' monad using the Ocaml list type:
+
+    type 'a c_list = ('a -> 'a list) -> 'a list
+    let c_list_unit x = fun f -> f x;;
+    let c_list_bind u f = fun k -> u (fun x -> f x k);;
+
+Have we really discovered that lists are secretly continuations?
+Or have we merely found a way of simulating lists using list
+continuations?  Both perspectives are valid, and we can use our