This book studies formal semantics in modern type theories (MTTsemantics). Compared with simple type theory, MTTs have much richer type structures and provide powerful means for adequate semantic constructions. This offers a serious alternative to the traditional settheoretical foundation for linguistic semantics and opens up a new avenue for developing formal semantics that is both model-theoretic and proof-theoretic, which was not available before the development of MTTsemantics. This book provides a reader-friendly and precise description of MTTs and offers a comprehensive introduction to…mehr
This book studies formal semantics in modern type theories (MTTsemantics). Compared with simple type theory, MTTs have much richer type structures and provide powerful means for adequate semantic constructions. This offers a serious alternative to the traditional settheoretical foundation for linguistic semantics and opens up a new avenue for developing formal semantics that is both model-theoretic and proof-theoretic, which was not available before the development of MTTsemantics. This book provides a reader-friendly and precise description of MTTs and offers a comprehensive introduction to MTT-semantics. It develops several case studies, such as adjectival modification and copredication, to exemplify the attractiveness of using MTTs for the study of linguistic meaning. It also examines existing proof assistant technology based on MTT-semantics for the verification of semantic constructions and reasoning in natural language. Several advanced topics are also briefly studied, including dependent event types, an application of dependent typing to event semantics.Hinweis: Dieser Artikel kann nur an eine deutsche Lieferadresse ausgeliefert werden.
Stergios Chatzikyriakidis is Associate Professor in Computational Linguistics and Associate Director of the Center for Linguistic Theory and Studies in Probability at the University of Gothenburg, Sweden. He is a computational semanticist with an interest in formal semantics and formal syntax. Zhaohui Luo is Professor of Computer Science at Royal Holloway, University of London, UK. He has published extensively on type theory, including a research monograph published by Oxford University Press. His research has focused on MTT-semantics over the last decade.
Inhaltsangabe
Preface ix Chapter 1. Type Theories and Semantic Studies 1 1.1. Historical development of type theories 2 1.2. Foundational semantic languages 4 1.3. Montague's model-theoretic semantics 6 1.3.1. Simple type theory: a formal description 6 1.3.2. Montague semantics: examples and intensionality 9 1.4. MTT-semantics: formal semantics in modern type theories 10 1.4.1. A glance at MTT-semantics 10 1.4.2. MTTs as foundational semantic languages: historical notes 13 1.4.3. Merits of MTT-semantics 17 Chapter 2. Modern Type Theories 23 2.1. Judgments and contextual mechanisms 24 2.2. Type constructors 28 2.2.1. -Types of dependent functions 28 2.2.2. -types of dependent pairs 30 2.2.3. Disjoint union types, unit types and finite types 32 2.3. Universes 33 2.3.1. Prop and logical propositions 33 2.3.2. Universes in linguistic semantics 35 2.3.3. Tarski-style and Russell-style universes 37 2.4. Subtyping 38 2.5. Formal presentation of type theories with signatures 43 Chapter 3. Formal Semantics in Modern Type Theories 47 3.1. Basic linguistic categories 48 3.2. Several unique features of MTT-semantics 51 3.2.1. Common nouns as types 51 3.2.2. Subtyping in MTT-semantics 54 3.2.3. Judgmental interpretations and their propositional forms 60 3.3. Adjectival modification: a case study 65 3.3.1. Intersective adjectives 67 3.3.2. Subsective adjectives 69 3.3.3. Privative adjectives 71 3.3.4. Non-committal adjectives 72 Chapter 4. Advanced Modification 75 4.1. The data 75 4.2. Gradable adjectives 80 4.3. Gradable nouns 84 4.3.1. Gradable nouns as -types 85 4.4. Multidimensional adjectives 86 4.4.1. Multidimensional adjectives: going more fine-grained 87 4.5. Adverbial modification 90 4.5.1. Veridicality 91 4.5.2. Event adverbs: manner, agent-oriented and speech-act adverbs 91 4.5.3. Domain, evaluative adverbs 95 4.5.4. Intensional adverbs 96 4.6. Final remarks on modification: vagueness 98 Chapter 5. Copredication and Individuation 99 5.1. Copredication and individuation: an introduction 100 5.2. Dot-types for copredication: a brief introduction 104 5.3. Identity criteria: individuation and CNs as setoids 108 5.3.1. Inheritance of identity criteria: usual cases of individuation 110 5.3.2. Generic semantics of numerical quantifiers 112 5.3.3. Copredication with quantification 113 5.3.4. Verbs plus adjectives: more on copredication with quantification 117 5.4. Concluding remarks and related work 119 Chapter 6. Reasoning and Verifying NL Semantics in Coq 127 6.1. Proof assistant technology based on MTTs 128 6.1.1. Mathematical proofs 128 6.1.2. Software verification 128 6.2. A linguist friendly introduction to Coq 129 6.2.1. Basics of Coq: types, sorts, functions 130 6.2.2. The proof engine of Coq 132 6.2.3. Useful proof tactics in Coq 135 6.2.4. Inductive types and record types 139 6.3. MTT-semantics in Coq 142 6.3.1. Adjectival and adverbial modification 143 6.3.2. Copredication and individuation in Coq 146 6.3.3. Related work 149 Chapter 7. Advanced Topics 151 7.1. Propositional forms of judgmental interpretations: formal treatment 151 7.2. Dependent event types 157 7.3. Dependent categorial grammars 163 Appendices 173 Appendix 1. Simple Type Theory C 175 Appendix 2. Type Constructors 177 Appendix 3. Prop and Logical Operators in Impredicative MTTs 181 Appendix 4. And for Coordination 183 Appendix 5. Formal System LF 187 Appendix 6. Rules for Dot-Types 191 Appendix 7. Coq Codes 193 References 209 Index 225
Preface ix Chapter 1. Type Theories and Semantic Studies 1 1.1. Historical development of type theories 2 1.2. Foundational semantic languages 4 1.3. Montague's model-theoretic semantics 6 1.3.1. Simple type theory: a formal description 6 1.3.2. Montague semantics: examples and intensionality 9 1.4. MTT-semantics: formal semantics in modern type theories 10 1.4.1. A glance at MTT-semantics 10 1.4.2. MTTs as foundational semantic languages: historical notes 13 1.4.3. Merits of MTT-semantics 17 Chapter 2. Modern Type Theories 23 2.1. Judgments and contextual mechanisms 24 2.2. Type constructors 28 2.2.1. -Types of dependent functions 28 2.2.2. -types of dependent pairs 30 2.2.3. Disjoint union types, unit types and finite types 32 2.3. Universes 33 2.3.1. Prop and logical propositions 33 2.3.2. Universes in linguistic semantics 35 2.3.3. Tarski-style and Russell-style universes 37 2.4. Subtyping 38 2.5. Formal presentation of type theories with signatures 43 Chapter 3. Formal Semantics in Modern Type Theories 47 3.1. Basic linguistic categories 48 3.2. Several unique features of MTT-semantics 51 3.2.1. Common nouns as types 51 3.2.2. Subtyping in MTT-semantics 54 3.2.3. Judgmental interpretations and their propositional forms 60 3.3. Adjectival modification: a case study 65 3.3.1. Intersective adjectives 67 3.3.2. Subsective adjectives 69 3.3.3. Privative adjectives 71 3.3.4. Non-committal adjectives 72 Chapter 4. Advanced Modification 75 4.1. The data 75 4.2. Gradable adjectives 80 4.3. Gradable nouns 84 4.3.1. Gradable nouns as -types 85 4.4. Multidimensional adjectives 86 4.4.1. Multidimensional adjectives: going more fine-grained 87 4.5. Adverbial modification 90 4.5.1. Veridicality 91 4.5.2. Event adverbs: manner, agent-oriented and speech-act adverbs 91 4.5.3. Domain, evaluative adverbs 95 4.5.4. Intensional adverbs 96 4.6. Final remarks on modification: vagueness 98 Chapter 5. Copredication and Individuation 99 5.1. Copredication and individuation: an introduction 100 5.2. Dot-types for copredication: a brief introduction 104 5.3. Identity criteria: individuation and CNs as setoids 108 5.3.1. Inheritance of identity criteria: usual cases of individuation 110 5.3.2. Generic semantics of numerical quantifiers 112 5.3.3. Copredication with quantification 113 5.3.4. Verbs plus adjectives: more on copredication with quantification 117 5.4. Concluding remarks and related work 119 Chapter 6. Reasoning and Verifying NL Semantics in Coq 127 6.1. Proof assistant technology based on MTTs 128 6.1.1. Mathematical proofs 128 6.1.2. Software verification 128 6.2. A linguist friendly introduction to Coq 129 6.2.1. Basics of Coq: types, sorts, functions 130 6.2.2. The proof engine of Coq 132 6.2.3. Useful proof tactics in Coq 135 6.2.4. Inductive types and record types 139 6.3. MTT-semantics in Coq 142 6.3.1. Adjectival and adverbial modification 143 6.3.2. Copredication and individuation in Coq 146 6.3.3. Related work 149 Chapter 7. Advanced Topics 151 7.1. Propositional forms of judgmental interpretations: formal treatment 151 7.2. Dependent event types 157 7.3. Dependent categorial grammars 163 Appendices 173 Appendix 1. Simple Type Theory C 175 Appendix 2. Type Constructors 177 Appendix 3. Prop and Logical Operators in Impredicative MTTs 181 Appendix 4. And for Coordination 183 Appendix 5. Formal System LF 187 Appendix 6. Rules for Dot-Types 191 Appendix 7. Coq Codes 193 References 209 Index 225
Es gelten unsere Allgemeinen Geschäftsbedingungen: www.buecher.de/agb
Impressum
www.buecher.de ist ein Internetauftritt der buecher.de internetstores GmbH
Geschäftsführung: Monica Sawhney | Roland Kölbl | Günter Hilger
Sitz der Gesellschaft: Batheyer Straße 115 - 117, 58099 Hagen
Postanschrift: Bürgermeister-Wegele-Str. 12, 86167 Augsburg
Amtsgericht Hagen HRB 13257
Steuernummer: 321/5800/1497
