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
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
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
-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.
And in fact, discussions of generalized coordination in the
linguistics literature are almost always left as a meta-level
implemented as a method for generating a suitable set of translation
rules, which are in turn expressed in a simply-typed grammar.
-There is some work using System F to express generalization about
+There is some work using System F to express generalizations about
natural language: Ponvert, Elias. 2005. Polymorphism in English Logical
Grammar. In *Lambda Calculus Type Theory and Natural Language*: 47--60.