-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 [β]</code>" evaluates to the kind of *and* that
-coordinates expressions of type β. 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.