Intuitionistic categorial grammar. (English) Zbl 0727.03019
Classical categorial grammar is based on simple type theory, whose hierarchy of types consists of the ground types of individuals and of truth values, and of types of functions from any given type to any other one. The intuitionistic type theory of Martin-Löf has a richer type structure, based on the type of sets, which also functions as the type of propositions. Function types (\(\alpha\),\(\beta\)) are generalized to product types (x:\(\alpha\))\(\beta\), where \(\beta\) may depend on x. The extra power is used for handling with anaphoric reference within a Montague-style grammar. References inside and between sentences cause no problem as soon as connectives and quantifiers are explained in the intuitionistic way. The paper is intended to be self-contained, so that it provides an outline of Martin-Löf’s type theory only presupposing familiarity with logic.
Reviewer: A.Ranta
Keywords:
intuitionistic categorial grammar; intuitionistic type theory of Martin- Löf; anaphoric reference; Montague-style grammarSoftware:
AutomathReferences:
| [1] | Ahn, R. and H.-P. Kolb: 1989, ?Discourse Representation Meets Constructive Mathematics?, to appear inThe Proceedings of the Second Symposium on Logic and Language, held at Hajdúszoboszló in September 1989. |
| [2] | Benthem, J. van: 1988, ?The Semantics of Variety in Categorial Grammar?, in W. Buszkowski, W. Marciszewski, and J. van Benthem (eds.),Categorial Grammar, John Benjamins Publishing Co., Amsterdam and Philadelphia. · Zbl 0695.03015 |
| [3] | Bruijn, N. G. de: 1970, ?The Mathematical Language AUTOMATH, its Usage and Some of its Extensions?, inLecture Notes in Mathematics 125, 29?61. · Zbl 0208.20101 · doi:10.1007/BFb0060623 |
| [4] | Coquand, Th. and G. Huet: 1988, ?The Calculus of Constructions?, inInformation and Computation 76, 95?120. · Zbl 0654.03045 · doi:10.1016/0890-5401(88)90005-3 |
| [5] | Curry, H. B. and R. Feys: 1958,Combinatory Logic, Vol. 1, North-Holland, Amsterdam, 1958. · Zbl 0081.24104 |
| [6] | Frege, G.: 1879,Begriffsschrift, Verlag von Louis Nebert, Halle. |
| [7] | Geach, G.: 1962,Reference and Generality, Cornell University Press, Ithaca, New York. |
| [8] | Geach, G.: 1972, ?A Program for Syntax?, in D. Davidson and G. Harman (eds.),Semantics of Natural Language, D. Reidel, Dordrecht, pp. 483?497. |
| [9] | Groenendijk, J. and M. Stokhof: ?Dynamic Predicate Calculus?, ITLI Prepublication series LP-89-02, to appear inLinguistics and Philosophy. · Zbl 0726.03024 |
| [10] | Groenendijk, J. and M. Stokhof: ?Dynamic Montague Grammar?, ITLI Prepublication Series LP-90-02. |
| [11] | Harper, R., F. Honsell, and G. Plotkin: 1987, ?A Framework for Defining Logics?,Proceedings of the Symposium on Loic in Computer Science, Ithaca, New York, pp. 194?204. |
| [12] | Heyting, A.: 1956,Intuitionism, North-Holland, Amsterdam. |
| [13] | Hintikka J. and L. Carlson: 1979, ?Conditionals, Generic Quantifiers, and other Applications of Subgames?, E. Saarinen (ed.),Game-Theoretical Semanics, D. Reidel, Dordrecht, pp. 179?214. |
| [14] | Hintikka, J. and J. Kulas: 1985,Anaphora and Definite Descriptions, D. Reidel, Dordrecht. |
| [15] | Howard, W.: 1980, ?The Formulae-as-Types Notion of Construction?, J. P. Seldin and J. R. Hindley (eds.),To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, London, pp. 479?490. |
| [16] | Kamp, H.: 1981, ?A Theory of Truth and Semantic Representation?, in J. A. G. Groenendijk, T. M. V. Janssen, and M. B. J. Stokhof (eds.),Formal Methods in the Study of Language, Part 1, Mathematical Centre Tracts 135, Mathematisch Centrum, Amsterdam, pp. 277?322. |
| [17] | Lambek, J.: 1958, ?The Mathematics of Sentence Structure?, inAmerican Mathematical Monthly 65, 154?170. · Zbl 0080.00702 · doi:10.2307/2310058 |
| [18] | Martin-Löf, P.: 1975, ?An Intuitionistic Theory of Types: Predicative Part?, H. E. Rose and J. C. Shepherdson (eds.), inLogic Colloquium ’73, North-Holland, Amsterdam, pp. 73?118. · Zbl 0334.02016 |
| [19] | Martin-Löf, P.: 1982, ?Constructive Mathematics and Computer Programming?, in L. J. Cohen, J. Los, H. Pfeiffer, and K.-P. Podewski (eds.),Logic, Methodology, and Philosophy of Science VI, North-Holland, Amsterdam, pp. 153?175. |
| [20] | Martin-Löf, P.: 1984,Intuitionistic Type Theory, Bibliopolis, Napoli. |
| [21] | Montague, R.: 1974,Formal Philosophy, Collected papers edited by R. Thomason, Yale University Press, New Haven. |
| [22] | Mäenpää, P. and A. Ranta: 1989, ?An Implementation of Intuitionistic Categorial Grammar?, to appear inThe Proceedings of the Second Symposium on Logic and Language held at Hajdúszoboszló in September 1989. |
| [23] | Nordström, B., K. Petersson, and J. Smith: 1990,Programminq in Martin-Löf’s Type Theory. An Introduction, Oxford University Press, Oxford. · Zbl 0744.03029 |
| [24] | Ranta, A.: 1988, ?Propositions as Games as Types?, Synthese76, 377?395. · doi:10.1007/BF00869607 |
| [25] | Ranta, A.: 1990, ?Anaphora in Game-Theoretical Semantics and in Intuitionistic Type Theory?, to appear in L. Haaparanta, M. Kusch, and I. Niiniluoto (eds.),Language, Knowledge, and Intentionality ? Perspectives in the Philosophy of Jaakko Himikka, Acta Philosophica Fennica, Societas Philosophica Fennica, Helsinki. |
| [26] | Ranta, A.: ?Meaning in Text?, mimeographed, University of Stockholm; forthcoming. |
| [27] | Sundholm, G.: 1986, ?Proof Theory and Meaning?, in D. Gabbay and F. Guenthner (eds.),Handbook of Philosophical Logic, Vol. 3, D. Reidel, Dordrecht, pp. 471?516. · Zbl 0875.03027 |
| [28] | Sundholm, G.: 1989, ?Constructive Generalized Quantifiers?,Synthese 79, 1?12. · doi:10.1007/BF00873254 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
