139,99 €
Mehr erfahren.
- Herausgeber: John Wiley & Sons
- Kategorie: Geisteswissenschaft
- Sprache: Englisch
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.
Sie lesen das E-Book in den Legimi-Apps auf:
Seitenzahl: 432
Veröffentlichungsjahr: 2020
Ähnliche
Table of Contents
Cover
Title page
Copyright
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.4. MTT-semantics: formal semantics in modern type theories
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
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
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
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
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
7 Advanced Topics
7.1. Propositional forms of judgmental interpretations: formal treatment
7.2. Dependent event types
7.3. Dependent categorial grammars
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
References
Index
End User License Agreement
List of Illustrations
Preface
Figure P.1. Dependency diagram for reading
Chapter 2
Figure 2.1. Pictorial illustration of the universe CN
Figure 2.2. Pictorial illustration of coercions for
A
≤
c
B
Chapter 3
Figure 3.1.
The semantics of “run” by overloading using coercive subtyping
Chapter 7
Figure 7.1.
Subtyping between DETs parameterized by agents and patients
Figure 7.2.
Rules for directed Lambek types B/A.
Figure 7.3.
Directed Π
r
-types
Figure 7.4.
Rules for Σ
∼
-types
Appendix 4
Figure A4.1.
Introduction rules for LTYPE
List of Tables
Chapter 1
Table 1.1.
Examples in Montague semantics
Table 1.2.
Semantics of “John talks”
Table 1.3.
Examples in MTT-semantics
Chapter 3
Table 3.1.
Examples in MTT-semantics
Table 3.2.
A classification of adjectives
Chapter 6
Table 6.1.
Some important Coq proof tactics according to logical connectives
Chapter 7
Table 7.1.
Directional syntactic types
Table 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
Guide
Cover
Table of Contents
Title page
Copyright
Preface
Begin Reading
References
Index
End User License Agreement
Pages
v
iii
iv
ix
x
xi
xii
xiii
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
175
176
177
178
179
181
182
183
184
185
187
188
189
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
225
226
227
228
229
231
232
233
234
235
236
Logic Linguistics and Computer Science Set
coordinated by
Christian Retoré
Volume 2
Formal Semantics in Modern Type Theories
Stergios Chatzikyriakidis
Zhaohui Luo
First published 2020 in Great Britain and the United States by ISTE Ltd and John Wiley & Sons, Inc.
Apart from any fair dealing for the purposes of research or private study, or criticism or review, as permitted under the Copyright, Designs and Patents Act 1988, this publication may only be reproduced, stored or transmitted, in any form or by any means, with the prior permission in writing of the publishers, or in the case of reprographic reproduction in accordance with the terms and licenses issued by the CLA. Enquiries concerning reproduction outside these terms should be sent to the publishers at the undermentioned address:
ISTE Ltd
27-37 St George’s Road
London SW19 4EU
UK
www.iste.co.uk
John Wiley & Sons, Inc.
111 River Street
Hoboken, NJ 07030
USA
www.wiley.com
© ISTE Ltd 2020
The rights of Stergios Chatzikyriakidis and Zhaohui Luo to be identified as the authors of this work have been asserted by them in accordance with the Copyright, Designs and Patents Act 1988.
Library of Congress Control Number: 2020943853
British Library Cataloguing-in-Publication Data
A CIP record for this book is available from the British Library
ISBN 978-1-78630-128-4
Preface
To communicate linguistically is to convey meaning. Semantics is the academic discipline that analyzes meaning. In this book, we study natural language semantics formally in the framework of modern type theories (MTTs). Examples of MTTs include Martin-Löf’s predicative type theory (Martin-Löf 1984; Nordström et al. 1990) and the impredicative type theories – unifying theory of dependent types UTT (Luo 1994) and pCIC (Coq 2010). MTTs offer a foundational framework that was not available in the study of formal semantics until Ranta’s work in the early 1990s when he applied Martin-Löf’s type theory to formal semantics (Ranta 1994). In the past decade, the development of formal semantics in MTTs (MTT-semantics for short) has shown that MTTs are powerful alternatives to, and arguably more advantageous than, Church’s simple type theory (Church 1940) as employed in Montague semantics (Montague 1974).
MTTs have rich type structures and, at the same time, are specified by means of proof-theoretic natural deduction rules. Therefore, they provide powerful tools in formal semantics, on the one hand, and have the appeal of being supported by a proof-theoretic theory of meaning, on the other hand. The former allows one to study a wide range of linguistic features, some of which have proved difficult to describe adequately in the Montagovian setting. The latter not only provides a solid proof-theoretic foundation for MTT-semantics but also leads to practical computer-assisted reasoning tools supported by the existing proof technology. These two aspects can be summarized by saying that MTT-semantics is both model-theoretic and proof-theoretic, a thesis that was put forward by the second author in Luo (2014) and further elaborated in Luo (2019a). This makes MTTs a promising and attractive semantic framework that is unique: such a framework was not available in traditional logical settings and the MTT-framework offers new perspectives on natural language semantics.
Learning MTTs can be laborious. This is partly because MTTs incorporate several new concepts that even traditional logicians may find difficult to comprehend at the beginning, let alone the linguists who apply logics to formal semantics. Therefore, in this book, besides studying MTT-semantics, we shall try our best to introduce the basics of MTTs informally: the explanations will be rigorous with examples from linguistic semantics. It is our hope that this will make it easier to understand and study MTT-semantics.
This book consists of the following seven chapters, where Chapters 1, 2, 3, sections 7.1 and 7.2 are mainly written by Luo, and Chapters 4, 5, 6 and section 7.3 are mainly written by Chatzikyriakidis.
–
Chapter 1
,
Type Theories and Semantic Studies
, starts with an overview of the historical development of type theories and a discussion on how to use a type theory as a foundational language for formal semantics. We then briefly describe Montague semantics, which is based on simple type theory,
1
and MTT-semantics, and compare them by means of some simple examples. This serves to introduce the basics of MTT-semantics in a very sketchy manner, together with some summary notes on its historical development, and allows us to outline several important merits of employing MTTs as a foundational semantic framework.
–
Chapter 2
,
Modern Type Theories
, consists of an informal but rigorous and precise introduction to MTTs, mainly for linguistic semanticists. In order to introduce the basic concepts in MTTs, we use explanatory examples to show how these may be employed in semantic constructions and, in most cases, we present their formal rules in appendices (mainly for completeness). Special attention is paid to several mechanisms that are particularly important for MTT-semantics, including coercive subtyping (Luo 1997), signatures (Luo 2014) and linguistic universes (Luo 2011b; Chatzikyriakidis and Luo 2012). We shall also give a complete formal presentation of the type theories used in this book, which is based on various studies (Luo 2014, 2019a), both for completeness and for reference in future work.
–
Chapter 3
,
Formal Semantics in Modern Type Theories
, is a central chapter that explicates several important features of MTT-semantics and shows that the MTT-semantic approach is viable and coherent, on the one hand, and provides flexible and powerful mechanisms for adequate semantic interpretations, on the other hand. Some features are discussed in depth: the CNs-as-types paradigm (Ranta 1994; Luo 2012a), subtyping in MTT-semantics (Luo 2009c, 2012b) and propositional forms of judgmental interpretations (Xue
et al
. 2018). As a case study for MTT-semantics, we study semantics of adjectival modification according to a traditional classification of adjectives into intersective, subsective, privative and non-committal adjectives, and investigate how such different adjectival modifications can be modeled adequately in the CNs-as-types paradigm.
2
This case study, together with the next two chapters, illustrates how the rich type structure in MTTs provide fruitful tools for modeling various linguistic features.
–
Chapter 4
,
Advanced Modification
, studies more advanced issues in adjectival and adverbial modification based on various studies (Chatzikyriakidis 2014; Chatzikyriakidis and Luo 2017a, 2020). After studying adjectival modification in
section 3.3
, we delve deeper into further issues concerning the semantics of modification, traditionally regarded as more advanced. In particular, we shall look at both adjectival and adverbial modification and argue that the rich typing mechanisms in MTTs are fit to deal with a number of issues on modification: gradability; gradable nouns; and veridical, event and intensional adverbs.
–
Chapter 5
,
Copredication and Individuation
, studies how the issue of copredication can be dealt with in MTT-semantics. First, the notion of dot-types proposed in the MTT-semantic setting (Luo 2009c, 2012b) is reviewed and shown to offer satisfactory semantic solutions to copredication. Then, we consider a number of challenging examples where both copredication and quantification are involved and show that, as proposed and studied in (Luo 2012a; Chatzikyriakidis and Luo 2018), CNs are better be interpreted as types associated with their own identity criteria (i.e. setoids) and copredication in such sophisticated situations requires a form of double distinctness of individuation: we provide an account based on the view of CNs-as-setoids and show that this gives us the correct semantics with intended results.
–
Chapter 6
,
Reasoning and Verifying NL Semantics in Coq
, shows how existing proof assistants such as Coq can be used in natural language reasoning based on MTT-semantics (Luo 2011b; Chatzikyriakidis and Luo 2014, 2016) – a promising technology that becomes available because MTTs are proof-theoretic and hence can be directly implemented. In this chapter, we introduce one of the leading proof assistants, Coq, and provide implementations for most of the semantic phenomena covered in the previous chapters. We further check the correctness of the implementations by providing proofs of a number of inferences that should go through, verifying that correct semantic accounts are given for the phenomena in question.
–
Chapter 7
,
Advanced Topics
, reports on several more advanced or on-going research developments on MTT-semantics. It consists of the following three sections:
1) in
section 7.1
, we conduct a formal study of propositional forms as informally introduced in
section 3.2.3
. It is shown that the relevant propositional forms can be introduced axiomatically by means of a negation operator and this extension can be justified (Xue
et al
. 2018) and, furthermore, semantic overgeneration by such propositional forms can be avoided (Luo and Xue 2020; Xue
et al
. 2020);
2) in
section 7.2
, we study dependent event types (DETs) proposed by Luo and Soloviev (2017) in the Montagovian setting,
3
showing that dependent types may play a useful role in refining types of events in event semantics and that the extension with DETs is conservative and hence preserves the nice properties of the original theory (Luo and Soloviev 2020);
3) in
section 7.3
, we study how to extend traditional categorial grammars with dependent types, starting to study dependent categorial grammars (DCGs). The theoretical basis for DCGs was developed and studied by the second author in Luo (2015, 2018c), where it is shown how to consider dependent Lambek types as syntactic categories corresponding to MTT-semantic types. In this book, we investigate DCGs in several aspects as related to CNs-as-types and more refined syntactic categories, and consider future promising research directions.
The diagram in Figure P.1 indicates how each chapter depends on the preceding chapters, although we have two points to make clear: (1) For Chapter 2, you can first read it through in less detail and then come back to revisit it later when needed. (2) Chapter 6 depends on earlier chapters only partly – you may read and understand most of the chapter without studying Chapter 4 or 5 in detail.
The intended audience of the present book includes researchers in formal semantics, computational semanticists, logicians or theoretical computer scientists interested in linguistic semantics and postgraduate students in linguistics with a background in formal semantics. A preliminary background in logic and some basic knowledge about Montague Grammar may be useful.
Figure P.1. Dependency diagram for reading
Throughout our work on MTT-semantics, we have benefited from discussions and communications with many researchers to whom we are extremely grateful. Here is an incomplete list: Robin Adams, Nicholas Asher, Daisuke Bekki, Jean-Philippe Bernardy, Rasmus Blanck, Robin Cooper, David Corfield, Nissim Francez, Matthew Gotham, Justyna Grudziñska, Ruth Kempson, Shalom Lappin, Huimin Lin, Georgiana Lungu, Harry Maclean, Aleksandre Maskharashvili, Louise McNally, Koji Mineshima, Richard Moot, Glyn Morrill, Larry Moss, Bengt Nordström, Gabriele Paveri-Fontana, Aarne Ranta, Christian Retoré, Sergei Soloviev, Göran Sundholm, Ribeka Tanaka, Tao Xue, Yu Zhang and Colin Zwanziger.
SC and ZL September 2020
1
The simple type theory employed in Montague semantics is presented in
section 1.3.1
as a natural deduction system, which will be further extended in
section 7.2
where we study dependent event types (Luo and Soloviev 2017) – an application of dependent types to event semantics.
2
The studies of interpreting various adjectival modifications can be found in the authors’ previous writings (Luo 2011a; Chatzikyriakidis and Luo 2013, 2017a), but in this book, we shall develop this further, especially concerning privative and non-committal adjectives – see
section 3.3
.
3
As shown in Luo and Soloviev (2017), dependent event types can be similarly considered for MTT-semantics. However, we choose to consider DETs only in the Montagovian setting in this book.
