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