tailieunhanh - Báo cáo khoa học: "Ambiguous propositions typed"

Ambiguous propositions are analyzed in a type system where disambiguation is effected during assembly (. by coercion). Ambiguity is introduced through a layer of types that are underspecified relative to a pre-existing collection of dependent types, construed as unambiguous propositions. A simple system of reasoning directly with such underspecification is described, and shown to be sound and complete for the full range of disambiguations. Beyond erasing types, the system supports constraints on disambiguations, including co-variation. . | Proceedings of EACL 99 Ambiguous propositions typed Tim Fernando Philosophy Department University of Texas Austin TX 78712-1180 USA Abstract Ambiguous propositions are analyzed in a type system where disambiguation is effected during assembly . by coercion . Ambiguity is introduced through a layer of types that are underspecified relative to a pre-existing collection of dependent types construed as unambiguous propositions. A simple system of reasoning directly with such underspecification is described and shown to be sound and complete for the full range of disambiguations. Beyond erasing types the system supports constraints on disambiguations 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 obvious approach is to take the disjunction of all alternatives assuming for the sake of the argument that the disjunction is a formula. Even if it were however various objections have been raised against this proposal . Deemter 1996 . For the purposes of the present paper what is interesting about a word phrase sentence or discourse that is ambiguous in isolation is how it may get disambiguated when combined with other expressions or more generally when placed in a wider context the challenge for any theory of ambiguity is to throw light on that process of disambiguation. From June to mid-August 1999 1 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 connective on propositions A and B such that A B is a proposition ambiguous between A and B. Under the propositions-as-types paradigm . Girard et al. 1989 identifying proofs