Atjaunināt sīkdatņu piekrišanu

E-grāmata: Formal Semantics in Modern Type Theories [Wiley Online]

,
  • Formāts: 256 pages
  • Izdošanas datums: 05-Mar-2021
  • Izdevniecība: ISTE Ltd and John Wiley & Sons Inc
  • ISBN-10: 1119489253
  • ISBN-13: 9781119489252
Citas grāmatas par šo tēmu:
  • Wiley Online
  • Cena: 168,05 €*
  • * this price gives unlimited concurrent access for unlimited time
Formal Semantics in Modern Type TheoriesPalielināt
  • Formāts: 256 pages
  • Izdošanas datums: 05-Mar-2021
  • Izdevniecība: ISTE Ltd and John Wiley & Sons Inc
  • ISBN-10: 1119489253
  • ISBN-13: 9781119489252
Citas grāmatas par šo tēmu:
Wiley Online E-booksMore info about Wiley Online
Rokasgrāmatas mājas lapa: https://onlinelibrary.wiley.com/doi/book/10.1002/9781119489252
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.
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)
2.2 Type constructors
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)
2.3 Universes
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)
2.4 Subtyping
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)
4.1 The data
75(5)
4.2 Gradable adjectives
80(4)
4.3 Gradable nouns
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)
4.5.1 Veridicality
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)
6.3 MTT-semantics in Coq
142(9)
6.3.1 Adjectival and adverbial modification
143(3)
6.3.2 Copredication and individuation in Coq
146(3)
6.3.3 Related work
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)
Appendices
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)
Appendix 7 Coq Codes
193(16)
References 209(16)
Index 225
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.
Permanent link: https://www.kriso.lv/db/9781119489252_pe.html
Keywords: