Formal Semantics in Modern Type Theories

Authors:

Language: English
Cover of the book Formal Semantics in Modern Type Theories

Subject for Formal Semantics in Modern Type Theories

171.59 €

In Print (Delivery period: 14 days).

Add to cartAdd to cart
Publication date:
256 p. · 1x1 cm · Hardback
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

1.1. Historical development of type theories 2

1.2. Foundational semantic languages 4

1.3. Montague’s model-theoretic semantics 6

1.3.1. Simple type theory: a formal description 6

1.3.2. Montague semantics: examples and intensionality 9

1.4. MTT-semantics: formal semantics in modern type theories 10

1.4.1. A glance at MTT-semantics 10

1.4.2. MTTs as foundational semantic languages: historical notes 13

1.4.3. Merits of MTT-semantics 17

Chapter 2. Modern Type Theories 23

2.1. Judgments and contextual mechanisms 24

2.2. Type constructors 28

2.2.1. Π-Types of dependent functions 28

2.2.2. Σ-types of dependent pairs 30

2.2.3. Disjoint union types, unit types and finite types 32

2.3. Universes 33

2.3.1. Prop and logical propositions 33

2.3.2. Universes in linguistic semantics 35

2.3.3. Tarski-style and Russell-style universes 37

2.4. Subtyping 38

2.5. Formal presentation of type theories with signatures 43

Chapter 3. Formal Semantics in Modern Type Theories 47

3.1. Basic linguistic categories 48

3.2. Several unique features of MTT-semantics 51

3.2.1. Common nouns as types 51

3.2.2. Subtyping in MTT-semantics 54

3.2.3. Judgmental interpretations and their propositional forms 60

3.3. Adjectival modification: a case study 65

3.3.1. Intersective adjectives 67

3.3.2. Subsective adjectives 69

3.3.3. Privative adjectives 71

3.3.4. Non-committal adjectives 72

Chapter 4. Advanced Modification 75

4.1. The data 75

4.2. Gradable adjectives 80

4.3. Gradable nouns 84

4.3.1. Gradable nouns as Σ-types 85

4.4. Multidimensional adjectives 86

4.4.1. Multidimensional adjectives: going more fine-grained 87

4.5. Adverbial modification 90

4.5.1. Veridicality 91

4.5.2. Event adverbs: manner, agent-oriented and speech-act adverbs 91

4.5.3. Domain, evaluative adverbs 95

4.5.4. Intensional adverbs 96

4.6. Final remarks on modification: vagueness 98

Chapter 5. Copredication and Individuation 99

5.1. Copredication and individuation: an introduction 100

5.2. Dot-types for copredication: a brief introduction 104

5.3. Identity criteria: individuation and CNs as setoids 108

5.3.1. Inheritance of identity criteria: usual cases of individuation 110

5.3.2. Generic semantics of numerical quantifiers 112

5.3.3. Copredication with quantification 113

5.3.4. Verbs plus adjectives: more on copredication with quantification 117

5.4. Concluding remarks and related work 119

Chapter 6. Reasoning and Verifying NL Semantics in Coq 127

6.1. Proof assistant technology based on MTTs 128

6.1.1. Mathematical proofs 128

6.1.2. Software verification 128

6.2. A linguist friendly introduction to Coq 129

6.2.1. Basics of Coq: types, sorts, functions 130

6.2.2. The proof engine of Coq 132

6.2.3. Useful proof tactics in Coq 135

6.2.4. Inductive types and record types 139

6.3. MTT-semantics in Coq 142

6.3.1. Adjectival and adverbial modification 143

6.3.2. Copredication and individuation in Coq 146

6.3.3. Related work 149

Chapter 7. Advanced Topics 151

7.1. Propositional forms of judgmental interpretations: formal treatment 151

7.2. Dependent event types 157

7.3. Dependent categorial grammars 163

Appendices 173

Appendix 1. Simple Type Theory C 175

Appendix 2. Type Constructors 177

Appendix 3. Prop and Logical Operators in Impredicative MTTs 181

Appendix 4. And for Coordination 183

Appendix 5. Formal System LFΔ 187

Appendix 6. Rules for Dot-Types 191

Appendix 7. Coq Codes 193

References 209

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.