Читать книгу Formal Semantics in Modern Type Theories - Stergios Chatzikyriakidis - Страница 2
ОглавлениеTable of Contents
1 Cover
4 Preface
5 1 Type Theories and Semantic Studies 1.1. Historical development of type theories 1.2. Foundational semantic languages 1.3. Montague’s model-theoretic semantics 1.4. MTT-semantics: formal semantics in modern type theories
6 2 Modern Type Theories 2.1. Judgments and contextual mechanisms 2.2. Type constructors 2.3. Universes 2.4. Subtyping 2.5. Formal presentation of type theories with signatures
7 3 Formal Semantics in Modern Type Theories 3.1. Basic linguistic categories 3.2. Several unique features of MTT-semantics 3.3. Adjectival modification: a case study
8 4 Advanced Modification 4.1. The data 4.2. Gradable adjectives 4.3. Gradable nouns 4.4. Multidimensional adjectives 4.5. Adverbial modification 4.6. Final remarks on modification: vagueness
9 5 Copredication and Individuation 5.1. Copredication and individuation: an introduction 5.2. Dot-types for copredication: a brief introduction 5.3. Identity criteria: individuation and CNs as setoids
10 6 Reasoning and Verifying NL Semantics in Coq 6.1. Proof assistant technology based on MTTs 6.2. A linguist friendly introduction to Coq 6.3. MTT-semantics in Coq
11 7 Advanced Topics 7.1. Propositional forms of judgmental interpretations: formal treatment 7.2. Dependent event types 7.3. Dependent categorial grammars
12 Appendices Appendix 1: Simple Type Theory C A1.1. Inference rules of C A1.2. Logical operators in C Appendix 2: Type Constructors A2.1. Π-types A2.2. Σ-types A2.3. Disjoint union types A2.4. The unit type and finite types Appendix 3: Prop and Logical Operators in Impredicative MTTs A3.1. Prop A3.2. Logical operators Appendix 4: And for Coordination Appendix 5: Formal System LFΔ A5.1. LFΔ A5.2. Σ-types in LFΔ Appendix 6: Rules for Dot-Types Appendix 7: Coq Codes A7.1. Some basic ontology and subtyping declarations A7.2. Simple homonymy by overloading in coercive subtyping A7.3. Intersective and subsective adjectives A7.4. Privative adjectives A7.5. Multidimensional adjectives A7.6. Gradable adjectives A7.7. Veridical adverbs A7.8. Manner adverbs A7.9. Individuation
13 References
14 Index
List of Illustrations
1 PrefaceFigure P.1. Dependency diagram for reading
2 Chapter 2Figure 2.1. Pictorial illustration of the universe CNFigure 2.2. Pictorial illustration of coercions for A ≤c B
3 Chapter 3Figure 3.1. The semantics of “run” by overloading using coercive subtyping
4 Chapter 7Figure 7.1. Subtyping between DETs parameterized by agents and patientsFigure 7.2. Rules for directed Lambek types B/A.Figure 7.3. Directed Πr-typesFigure 7.4. Rules for Σ∼-types
5 Appendix 4Figure A4.1. Introduction rules for LTYPE
List of Tables
1 Chapter 1Table 1.1. Examples in Montague semanticsTable 1.2. Semantics of “John talks”Table 1.3. Examples in MTT-semantics
2 Chapter 3Table 3.1. Examples in MTT-semanticsTable 3.2. A classification of adjectives
3 Chapter 6Table 6.1. Some important Coq proof tactics according to logical connectives
4 Chapter 7Table 7.1. Directional syntactic typesTable 7.2. Comparison of simple lexical entries in standard versions of categori...Table 7.3. Sample lexicon for a dependent CG in comparison with a standard CG
Pages
1 v
2 iii
3 iv
4 ix
5 x
6 xi
7 xii
8 xiii
9 1
10 2
11 3
12 4
13 5
14 6
15 7
16 8
17 9
18 10
19 11
20 12
21 13
22 14
23 15
24 16
25 17
26 18
27 19
28 20
29 21
30 22
31 23
32 24
33 25
34 26
35 27
36 28
37 29
38 30
39 31
40 32
41 33
42 34
43 35
44 36
45 37
46 38
47 39
48 40
49 41
50 42
51 43
52 44
53 45
54 46
55 47
56 48
57 49
58 50
59 51
60 52
61 53
62 54
63 55
64 56
65 57
66 58
67 59
68 60
69 61
70 62
71 63
72 64
73 65
74 66
75 67
76 68
77 69
78 70
79 71
80 72
81 73
82 74
83 75
84 76
85 77
86 78
87 79
88 80
89 81
90 82
91 83
92 84
93 85
94 86
95 87
96 88
97 89
98 90
99 91
100 92
101 93
102 94
103 95
104 96
105 97
106 98
107 99
108 100
109 101
110 102
111 103
112 104
113 105
114 106
115 107
116 108
117 109
118 110
119 111
120 112
121 113
122 114
123 115
124 116
125 117
126 118
127 119
128 120
129 121
130 122
131 123
132 124
133 125
134 127
135 128
136 129
137 130
138 131
139 132
140 133
141 134
142 135
143 136
144 137
145 138
146 139
147 140
148 141
149 142
150 143
151 144
152 145
153 146
154 147
155 148
156 149
157 150
158 151
159 152
160 153
161 154
162 155
163 156
164 157
165 158
166 159
167 160
168 161
169 162
170 163
171 164
172 165
173 166
174 167
175 168
176 169
177 170
178 171
179 172
180 173
181 175
182 176
183 177
184 178
185 179
186 181
187 182
188 183
189 184
190 185
191 187
192 188
193 189
194 191
195 192
196 193
197 194
198 195
199 196
200 197
201 198
202 199
203 200
204 201
205 202
206 203
207 204
208 205
209 206
210 207
211 209
212 210
213 211
214 212
215 213
216 214
217 215
218 216
219 217
220 218
221 219
222 220
223 221
224 222
225 223
226 225
227 226
228 227
229 228
230 229
231 231
232 232
233 233
234 234
235 235
236 236
