Ambiguous propositions typed

Proceedings of EACL '99 Ambiguous propositions typed Tim Fernando Philosophy Department University of Texas Austin, TX 78712-1180, USA f ernando~ims, uni-stuttgart, de* Abstract Ambiguous propositions are analyzed in a type system where disambiguation is effected during assembly (i.e. by coer- cion). Ambiguity is introduced through a layer of types that are underspecified relative to a pre-existing collection of de- pendent types, construed as unambigu- ous propositions. A simple system of reasoning directly with such underspec- ification is described, and shown to be sound and complete for the full range of disambiguations. Beyond erasing types, the system supports constraints on dis- ambiguations, including co-variation. 1 Introduction A widely held view expressed in (Carbonell and Hayes, 1987) is that "if there were one word to describe why natural language processing is hard, it is ambiguity." For any given natural language utterance, a formal language such as predicate logic typically offers several non-equivalent (well- formed) formulas as possible translations. An ob- vious approach is to take the disjunction of all alternatives, assuming (for the sake of the argu- ment) that the disjunction is a formula. Even if it were, however, various objections have been raised against this proposal (e.g. (Deemter, 1996)). For the purposes of the present paper, what is inter- esting about a word, phrase, sentence or discourse that is ambiguous in isolation is how it may get disambiguated when combined with other expres- sions (or, more generally, when placed in a wider context); the challenge for any theory of ambigu- ity is to throw light on that process of disambigua- tion. *From June to mid-August 1999, I will be visiting IMS, Uni Stuttgart, Azenbergstr 12, 70174 Stuttgart, Germany. Where I might be after that is unclear. More concretely, suppose • were a binary con- nective on propositions A and B such that A • B is a proposition ambiguous between A and B. Under the "propositions-as-types" paradigm (e.g. (Gi- rard et al., 1989)) identifying proofs of a proposi- tion with programs of the corresponding type (so that "t: A" can be read as t is a proof of proposi- tion A, or equivalently, t is a program of type A), disambiguation may take the form of type coer- cion. An instructive example with F as the con- text is x:(A-+ B) oC, y:DoA r ~- ap(p.(x),q.(y)):B (1) where ap is function application (corresponding to modus ponens), while p. and qo are the first and second o-projections, so that and x:(A ~ B)•C ~ p,(x):A ~ B y:D.A ~- qo(y):A. Evidently, there is something conjunctive (never mind disjunctive) about o; but beyond the ques- tion as to whether the unambiguous propositions constituting the possible readings of an ambigu- ous proposition form a conjunctive or disjunctive set (whatever that may precisely mean), there is also the matter of the interconnected choices from such sets, mediated by terms such as p°(x) and q°(Y). To ground these abstract considerations in nat- ural language processing, a few words about how to think of the terms t …

Content truncated to 500 words