Оглавление
Stergios Chatzikyriakidis. Formal Semantics in Modern Type Theories
Table of Contents
List of Illustrations
List of Tables
Guide
Pages
Formal Semantics in Modern Type Theories
Preface
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.3.1. Simple type theory: a formal description
1.3.2. Montague semantics: examples and intensionality
1.4. MTT-semantics: formal semantics in modern type theories
1.4.1. A glance at MTT-semantics
1.4.2. MTTs as foundational semantic languages: historical notes
1.4.3. Merits of MTT-semantics
2. Modern Type Theories
2.1. Judgments and contextual mechanisms
2.2. Type constructors
2.2.1. Π-Types of dependent functions
2.2.2. Σ-types of dependent pairs
2.2.3. Disjoint union types, unit types and finite types
2.3. Universes
2.3.1.Prop and logical propositions
2.3.2. Universes in linguistic semantics
2.3.3. Tarski-style and Russell-style universes
2.4. Subtyping
2.5. Formal presentation of type theories with signatures
3. Formal Semantics in Modern Type Theories
3.1. Basic linguistic categories
3.2. Several unique features of MTT-semantics
3.2.1. Common nouns as types
3.2.2. Subtyping in MTT-semantics
3.2.3. Judgmental interpretations and their propositional forms
3.3. Adjectival modification: a case study
3.3.1. Intersective adjectives
3.3.2. Subsective adjectives
3.3.3. Privative adjectives
3.3.4. Non-committal adjectives
4. Advanced Modification
4.1. The data
4.2. Gradable adjectives
4.3. Gradable nouns
4.3.1. Gradable nouns asΣ-types
4.4. Multidimensional adjectives
4.4.1. Multidimensional adjectives: going more fine-grained
4.5. Adverbial modification
4.5.1. Veridicality
4.5.2. Event adverbs: manner, agent-oriented and speech-act adverbs
4.5.3. Domain, evaluative adverbs
4.5.4. Intensional adverbs
4.6. Final remarks on modification: vagueness
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
5.3.1. Inheritance of identity criteria: usual cases of individuation
5.3.2. Generic semantics of numerical quantifiers
5.3.3. Copredication with quantification
5.3.4. Verbs plus adjectives: more on copredication with quantification
5.4. Concluding remarks and related work
6. Reasoning and Verifying NL Semantics in Coq
6.1. Proof assistant technology based on MTTs
6.1.1. Mathematical proofs
6.1.2. Software verification
6.2. A linguist friendly introduction to Coq
6.2.1. Basics of Coq: types, sorts, functions
6.2.2. The proof engine of Coq
6.2.3. Useful proof tactics in Coq
6.2.4. Inductive types and record types
6.3. MTT-semantics in Coq
6.3.1. Adjectival and adverbial modification
6.3.2. Copredication and individuation in Coq
6.3.3. Related work
7. Advanced Topics
7.1. Propositional forms of judgmental interpretations: formal treatment
7.2. Dependent event types
7.3. Dependent categorial grammars
Appendix 1. Simple Type Theory C. A1.1. Inference rules ofC
A1.2. Logical operators inC
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
References
Index. A
C
D, E
F, G
H, I
J
L
M
N
O, P
S
T
U, V
WILEY END USER LICENSE AGREEMENT
