From 3286774dd5086d93efc40df3c846f26b3f5b39ef Mon Sep 17 00:00:00 2001 From: Chris Date: Sun, 1 Mar 2015 18:21:04 -0500 Subject: [PATCH] adjusted talk about *and* --- topics/_week5_system_F.mdwn | 79 ++++++++++++++++++++++----------------------- 1 file changed, 39 insertions(+), 40 deletions(-) diff --git a/topics/_week5_system_F.mdwn b/topics/_week5_system_F.mdwn index 76725d65..242ada43 100644 --- 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.) - 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 @@ -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 -uses. Can we capture this using polymorphic types? +uses. + +Can we capture this using polymorphic types? 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 - 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 -"and [β]" 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 -- 2.11.0