From: Chris Date: Wed, 25 Feb 2015 18:40:10 +0000 (-0500) Subject: edits X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=69cefc9d2ec23b63ee6ae14d6b0c2b0ddabfd68e edits --- diff --git a/topics/_week5_system_F.mdwn b/topics/_week5_system_F.mdwn index ff0b341b..1e3edbcb 100644 --- a/topics/_week5_system_F.mdwn +++ b/topics/_week5_system_F.mdwn @@ -203,7 +203,7 @@ Turing complete. ## Polymorphism in natural language Is the simply-typed lambda calclus enough for analyzing natural -language, or do we need polymorphic types (or something even more expressive)? +language, or do we need polymorphic types? Or something even more expressive? The classic case study motivating polymorphism in natural language comes from coordination. (The locus classicus is Partee and Rooth @@ -218,9 +218,9 @@ In English (likewise, many other languages), *and* can coordinate clauses, verb phrases, determiner phrases, transitive verbs, and many 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 treatment of *and* 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? +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? Ann, Bill e left, slept e -> t @@ -234,45 +234,49 @@ With these basic types, we want to say something like this: lambda x:'a . and:'b (l x) (r x) The idea is that the basic *and* conjoins expressions of type `t`, and -when *and* conjoins functional types, the result is a function that -distributes its argument across the two conjuncts and conjoins the -result. So `Ann left and slept` will evaluate to `(\x.and(left -x)(slept x)) ann`. Following Partee and Rooth, the 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. +when *and* conjoins functional types, it builds a function that +distributes its argument across the two conjuncts and conjoins the two +results. So `Ann left and slept` will evaluate to `(\x.and(left +x)(slept x)) ann`. Following the terminology of Partee and Rooth, the +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 several problems. The first is that we have two +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 +`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. System F does not have -recursion. 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. -But fully instantiating the definition as given requires type -application to a pair of types, not just one type. +recursion. + +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. But fully +instantiating the definition as given requires type application to a +pair of types, not to just a single type. We want to somehow +guarantee that 'b will always itself be a complex type. 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. And in fact, discussions of generalized coordination in the -linguistics literature are almost always left as a metageneralization -over a basic simply-typed grammar. For instance, in Hendriks' 1992:74 -dissertation, generalized coordination is implemented as a method for -generating a suitable set of translation rules, which are in turn -expressed in a simply-typed grammar. +linguistics literature are almost always left as a meta-level +generalizations over a basic simply-typed grammar. For instance, in +Hendriks' 1992:74 dissertation, generalized coordination is +implemented as a method for generating a suitable set of translation +rules, which are in turn expressed in a simply-typed grammar. -Not incidentally, we're not aware of any programming language that +Not incidentally, we're not aware of any programming language that makes generalized coordination available, despite is naturalness and ubiquity in natural language. That is, coordination in programming -languages is always at the sentential level. You might be able to evaluate -`delete file1 and delete file2` but never `delete file1 and file2`. +languages is always at the sentential level. You might be able to +evaluate `(delete file1) and (delete file2)`, but never `delete (file1 +and file2)`. We'll return to thinking about generalized coordination as we get deeper into types. There will be an analysis in term of continuations