adjusted talk about *and*

diff --git a/topics/_week5_system_F.mdwn b/topics/_week5_system_F.mdwn
index 76725d6..242ada4 100644 (file)
--- a/topics/_week5_system_F.mdwn
+++ b/topics/_week5_system_F.mdwn
@@ -192,10 +192,11 @@ The classic case study motivating polymorphism in natural language
 comes from coordination.  (The locus classicus is Partee and Rooth
 1983.)
 
 comes from coordination.  (The locus classicus is Partee and Rooth
 1983.)
 

-    Ann left and Bill left.
-    Ann left and slept.
-    Ann and Bill left.
-    Ann read and reviewed the book.
+                                      Type of the argument of "and":
+    Ann left and Bill left.           t
+    Ann left and slept.               e->t
+    Ann and Bill left.                (e->t)-t  (i.e, generalize quantifiers)
+    Ann read and reviewed the book.   e->e->t

 
 In English (likewise, many other languages), *and* can coordinate
 clauses, verb phrases, determiner phrases, transitive verbs, and many
 
 In English (likewise, many other languages), *and* can coordinate
 clauses, verb phrases, determiner phrases, transitive verbs, and many


@@ -203,7 +204,9 @@ other phrase types.  In a garden-variety simply-typed grammar, each
 kind of conjunct has a different semantic type, and so we would need
 an independent rule for each one.  Yet there is a strong intuition
 that the contribution of *and* remains constant across all of these
 kind of conjunct has a different semantic type, and so we would need
 an independent rule for each one.  Yet there is a strong intuition
 that the contribution of *and* remains constant across all of these

-uses.  Can we capture this using polymorphic types?
+uses.  
+
+Can we capture this using polymorphic types?

 
     Ann, Bill      e
     left, slept    e -> t    
 
     Ann, Bill      e
     left, slept    e -> t    


@@ -212,45 +215,41 @@ uses.  Can we capture this using polymorphic types?
 With these basic types, we want to say something like this:
 
     and:t->t->t = λl:t. λr:t. l r false
 With these basic types, we want to say something like this:
 
     and:t->t->t = λl:t. λr:t. l r false

-    and = Λα.Λβ.λl:α->β.λr:α->β.λx:α. and [β] (l x) (r x)
+    gen_and = Λα.Λβ.λf:(β->t).λl:α->β.λr:α->β.λx:α. f (l x) (r x)

 
 The idea is that the basic *and* (the one defined in the first line)
 conjoins expressions of type `t`.  But when *and* conjoins functional
 types (the definition in the second line), it builds a function that
 
 The idea is that the basic *and* (the one defined in the first line)
 conjoins expressions of type `t`.  But when *and* conjoins functional
 types (the definition in the second line), it builds a function that

-distributes its argument across the two conjuncts and conjoins the two
-results.  The intention is that `Ann left and slept` will evaluate to
-`(\x.and(left x)(slept x)) ann`.  Following the terminology of Partee
-and Rooth, this strategy of defining the coordination of expressions
-with complex types in terms of the coordination of expressions with
-less complex types is known as Generalized Coordination.
-
-But the definitions just given are not well-formed expressions in
-System F.  There are three problems.  The first is that we have two
-definitions of the same word.  The intention is for one of the
-definitions to be operative when the type of its arguments is type
-`t`, but we have no way of conditioning evaluation on the *type* of an
-argument.  The second is that for the polymorphic definition, the term
-*and* occurs inside of the definition.  We know how to handle some
-cases of using a function name inside of its own definition in the
-untyped lambda calculus, but System F does not have
-recursion.  [Exercise: convince yourself that the fixed-point
-combinator `Y` can't be typed in System F.]
-
-The third problem is more subtle.  The defintion as given takes two
-types as parameters: the type of the first argument expected by each
-conjunct, and the type of the result of applying each conjunct to an
-argument of that type.  We would like to instantiate the recursive use
-of *and* in the definition by using the result type, so that
-"<code>and [&beta;]</code>" evaluates to the kind of *and* that
-coordinates expressions of type &beta;.  But fully instantiating the
-definition as given requires type application to a *pair* of types,
-not to just to a single type.  We want to somehow guarantee that β
-will always itself be a complex type.  This goes beyond the expressive
-power of System F.
-
-So conjunction and disjunction provide a compelling motivation for
-polymorphism in natural language, but we don't yet have the ability to
-build the polymorphism into a formal system.
+distributes its argument across the two conjuncts and then applies the
+appropriate lower-order instance of *and*.
+
+    and (Ann left) (Bill left)
+    gen_and [e] [t] and left slept
+    gen_and [e] [e->t] (gen_and [e] [t] and) read reviewed
+
+Following the terminology of Partee and Rooth, this strategy of
+defining the coordination of expressions with complex types in terms
+of the coordination of expressions with less complex types is known as
+Generalized Coordination, which is why we call the polymorphic part of
+the definition `gen_and`.
+
+In the first line, the basic *and* is ready to conjoin two truth
+values.  In the second line, the polymorphic definition of `gen_and`
+makes explicit exactly how the meaning of *and* when it coordinates
+verb phrases depends on the meaning of the basic truth connective.
+Likewise, when *and* coordinates transitive verbs of type `e->e->t`,
+the generalized *and* depends on the `e->t` version constructed for
+dealing with coordinated verb phrases.
+
+On the one hand, this definition accurately expresses the way in which
+the meaning of the conjunction of more complex types relates to the
+meaning of the conjunction of simpler types.  On the other hand, it's
+awkward to have to explicitly supply an expression each time that
+builds up the meaning of the *and* that coordinates the expressions of
+the simpler types.  We'd like to have that automatically handled by
+the polymorphic definition; but that would require writing code that
+behaved differently depending on the types of its type arguments,
+which goes beyond the expressive power of System F.

 
 And in fact, discussions of generalized coordination in the
 linguistics literature are almost always left as a meta-level
 
 And in fact, discussions of generalized coordination in the
 linguistics literature are almost always left as a meta-level