Stergios Chatzikyriakidis - Formal Semantics in Modern Type Theories

1 Cover

2 Title page Logic Linguistics and Computer Science Set coordinated by Christian Retoré Volume 2

3 Copyright 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

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 CA1.1. Inference rules of C A1.2. Logical operators in C Appendix 2: Type ConstructorsA2.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 CodesA7.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

15 End User License Agreement

1 PrefaceFigure P.1. Dependency diagram for reading

2 Chapter 2 Figure 2.1. Pictorial illustration of the universe CNFigure 2.2. Pictorial illustration of coercions for A ≤ cB

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 patients Figure 7.2. Rules for directed Lambek types B/A. Figure 7.3. Directed Πr-types Figure 7.4. Rules for Σ∼-types

5 Appendix 4Figure A4.1. Introduction rules for LTYPE

1 Chapter 1Table 1.1. Examples in Montague semantics Table 1.2. Semantics of “John talks” Table 1.3. Examples in MTT-semantics

2 Chapter 3Table 3.1. Examples in MTT-semantics Table 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 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

1 Cover

2 Table of Contents

3 Title page Logic Linguistics and Computer Science Set coordinated by Christian Retoré Volume 2

4 Copyright 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

5 Preface

6 Begin Reading

7 References

8 Index

9 End User License Agreement

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