Categorial Investigations: Logical and Linguistic Aspects of the Lambek Calculus [PhD Thesis]

Cover ......Page 1
Contents ......Page 6
Preface ......Page 9
Samenvatting ......Page 12
1.0 Introduction ......Page 15
1.1.1 Category structure ......Page 17
1.1.2 Reduction laws ......Page 24
1.2.1 The Lambek-Gentzen calculus ......Page 41
1.2.2 Cuts and decidability ......Page 45
1.2.3 Lambda semantics for Gentzen proofs ......Page 51
1.3.1 Options for categorial calculi ......Page 54
1.3.2 Polymorphism and unification ......Page 63
PART ONE: LINGUISTIC ASPECTS OF THE LAMBEK CALCULUS ......Page 69
2.0 Introduction ......Page 71
2.1 Structural completeness ......Page 72
2.2 Gentzen proofs: prosodic interpretation ......Page 74
2.3 Intonational versus morphosyntactic phrasing ......Page 79
2.4 Morphological bracketing paradoxes ......Page 84
2.5 Cliticization: English auxiliary and genitive \'s ......Page 88
3.0 Strategies for extending L ......Page 95
3.1 LP additions to the L axiom base ......Page 97
3.1.1 Permutation duals: Lifting, Composition, Substitution ......Page 99
3.1.2 Collapse into LP ......Page 104
3.2 Discontinuity at the lexical level ......Page 108
3.2.1 Complement inheritance ......Page 109
3.2.2 Verb-raising, Dutch versus German ......Page 115
3.2.3 Division versus Composition ......Page 118
3.3.1 Extraction/Infixation ......Page 122
3.3.2 Extraction Introduction ......Page 125
Illustration: unbounded dependencies ......Page 127
3.3.3 Infixation Elimination ......Page 128
Illustration: verb-projection raising ......Page 129
3.3.4 Extraction, Infixation: partial logic ......Page 135
PART TWO: CATEGORIAL PARSING AS GENTZEN DEDUCTION ......Page 139
4.1 The Lambek-Gentzen sequent calculus as Horn clause logic ......Page 145
Resolution ......Page 148
Illustration ......Page 150
4.2 An interpreter for the Lambek-Gentzen system ......Page 152
Gentzen proof trees ......Page 153
Full interpreter for the sequent calculus ......Page 158
Resolution, unifying substitutions: examples ......Page 161
Semantic interpretation for Gentzen proofs ......Page 162
4.3 Reducing search complexity ......Page 164
Deduction trees versus proof trees ......Page 165
Pruning the search space: count-invariance ......Page 168
Premise selection: degree ......Page 174
Conclusion ......Page 177
5.0 Introduction ......Page 179
5.1 Complete and incomplete search strategies ......Page 180
Logical infinity of L ......Page 184
5.2 Bottom-up proofs in L + {Cut} ......Page 188
Extending L with Cut ......Page 191
Partial execution of the Elimination rules ......Page 194
5.3 The Lemma Database: System M ......Page 196
Monotonicity ......Page 198
Recursive axiomatization: system M ......Page 200
M semantics: partial execution ......Page 203
Associativity: atomic boundary cases ......Page 206
Conclusion ......Page 213
5.4 Examples ......Page 215
Incremental left-associative processing ......Page 216
Non-determinism and structural ambiguity ......Page 225
Non-constituent coordination ......Page 229
Conclusion ......Page 234
5.5 Flexible semantics for L proofs ......Page 235
Argument lifting: L versus LP ......Page 237
The quantification calculus H ......Page 239
Semantics for Gentzen proofs: L + H ......Page 240
Examples: Type-shifting, scope ambiguity, non-constituent conjunction ......Page 243
Conclusions ......Page 257
Appendix ......Page 261
References ......Page 279