Details

<p>Preface ix</p> <p><b>Chapter 1. Type Theories and Semantic Studies </b><b>1</b></p> <p>1.1. Historical development of type theories 2</p> <p>1.2. Foundational semantic languages 4</p> <p>1.3. Montague’s model-theoretic semantics 6</p> <p>1.3.1. Simple type theory: a formal description 6</p> <p>1.3.2. Montague semantics: examples and intensionality 9</p> <p>1.4. MTT-semantics: formal semantics in modern type theories 10</p> <p>1.4.1. A glance at MTT-semantics 10</p> <p>1.4.2. MTTs as foundational semantic languages: historical notes 13</p> <p>1.4.3. Merits of MTT-semantics 17</p> <p><b>Chapter 2. Modern Type Theories </b><b>23</b></p> <p>2.1. Judgments and contextual mechanisms 24</p> <p>2.2. Type constructors 28</p> <p>2.2.1. Π-Types of dependent functions 28</p> <p>2.2.2. Σ-types of dependent pairs 30</p> <p>2.2.3. Disjoint union types, unit types and finite types 32</p> <p>2.3. Universes 33</p> <p>2.3.1. <i>Prop</i> and logical propositions 33</p> <p>2.3.2. Universes in linguistic semantics 35</p> <p>2.3.3. Tarski-style and Russell-style universes 37</p> <p>2.4. Subtyping 38</p> <p>2.5. Formal presentation of type theories with signatures 43</p> <p><b>Chapter 3. Formal Semantics in Modern Type Theories </b><b>47</b></p> <p>3.1. Basic linguistic categories 48</p> <p>3.2. Several unique features of MTT-semantics 51</p> <p>3.2.1. Common nouns as types 51</p> <p>3.2.2. Subtyping in MTT-semantics 54</p> <p>3.2.3. Judgmental interpretations and their propositional forms 60</p> <p>3.3. Adjectival modification: a case study 65</p> <p>3.3.1. Intersective adjectives 67</p> <p>3.3.2. Subsective adjectives 69</p> <p>3.3.3. Privative adjectives 71</p> <p>3.3.4. Non-committal adjectives 72</p> <p><b>Chapter 4. Advanced Modification </b><b>75</b></p> <p>4.1. The data 75</p> <p>4.2. Gradable adjectives 80</p> <p>4.3. Gradable nouns 84</p> <p>4.3.1. Gradable nouns as Σ-types 85</p> <p>4.4. Multidimensional adjectives 86</p> <p>4.4.1. Multidimensional adjectives: going more fine-grained 87</p> <p>4.5. Adverbial modification 90</p> <p>4.5.1. Veridicality 91</p> <p>4.5.2. Event adverbs: manner, agent-oriented and speech-act adverbs 91</p> <p>4.5.3. Domain, evaluative adverbs 95</p> <p>4.5.4. Intensional adverbs 96</p> <p>4.6. Final remarks on modification: vagueness 98</p> <p><b>Chapter 5. Copredication and Individuation </b><b>99</b></p> <p>5.1. Copredication and individuation: an introduction 100</p> <p>5.2. Dot-types for copredication: a brief introduction 104</p> <p>5.3. Identity criteria: individuation and CNs as setoids 108</p> <p>5.3.1. Inheritance of identity criteria: usual cases of individuation 110</p> <p>5.3.2. Generic semantics of numerical quantifiers 112</p> <p>5.3.3. Copredication with quantification 113</p> <p>5.3.4. Verbs plus adjectives: more on copredication with quantification 117</p> <p>5.4. Concluding remarks and related work 119</p> <p><b>Chapter 6. Reasoning and Verifying NL Semantics in Coq </b><b>127</b></p> <p>6.1. Proof assistant technology based on MTTs 128</p> <p>6.1.1. Mathematical proofs 128</p> <p>6.1.2. Software verification 128</p> <p>6.2. A linguist friendly introduction to Coq 129</p> <p>6.2.1. Basics of Coq: types, sorts, functions 130</p> <p>6.2.2. The proof engine of Coq 132</p> <p>6.2.3. Useful proof tactics in Coq 135</p> <p>6.2.4. Inductive types and record types 139</p> <p>6.3. MTT-semantics in Coq 142</p> <p>6.3.1. Adjectival and adverbial modification 143</p> <p>6.3.2. Copredication and individuation in Coq 146</p> <p>6.3.3. Related work 149</p> <p><b>Chapter 7. Advanced Topics </b><b>151</b></p> <p>7.1. Propositional forms of judgmental interpretations: formal treatment 151</p> <p>7.2. Dependent event types 157</p> <p>7.3. Dependent categorial grammars 163</p> <p><b>Appendices </b><b>173</b></p> <p>Appendix 1. Simple Type Theory <i>C</i> 175</p> <p>Appendix 2. Type Constructors 177</p> <p>Appendix 3. Prop and Logical Operators in Impredicative MTTs 181</p> <p>Appendix 4. And for Coordination 183</p> <p>Appendix 5. Formal System LF_Δ 187</p> <p>Appendix 6. Rules for Dot-Types 191</p> <p>Appendix 7. Coq Codes 193</p> <p>References 209</p> <p>Index 225</p>

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.

US