Abstract
We have been studying the structure of simple mathematical statements in English. It has turned out that both phrase structure grammar and type theory are needed. Then we have given an interpretation and generalization of phrase structure grammar in type theory—in other words, an extension of type theory with a system of categories of phrase structure grammar. We have ended up with a formalism that comprises both informal English (that is, strings of words), a system of syntactic categories and syntax trees, and a formal mathematical language. We have shown how syntax trees are sugared into English and interpreted in the mathematical formalism.
We have not shown how to define the inverses of sugaring and interpretation, which are by no means trivial. The inverse of sugaring, that is, parsing, was briefly discussed at the end of Section 6. The inverse of interpretation would be a function that takes type-theoretical formulae into syntax trees. It could be combined with the sugaring operation that we already have, to obtain a sugaring method for the mathematical formalism. We have previously tried to define sugaring directly for the mathematical formalism (see Ranta 1994a, chapter 9, and 1994b), but then we did not have access to other categorial structure than the structure of type theory.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Yehoshua Bar-Hillel. On categorial and phrase structure grammars. The Bulletin of the Research Council of Israel 9F, pages 1–16, 1960. Reprinted in Y. Bar-Hillel, Language and Information, pages 99–115. Addison-Wesley Publishing Company and the Jerusalem Academic Press, Jerusalem, 1964.
Noam Chomsky. Syntactic Structures. Mouton, The Hague, 1957.
Noam Chomsky. Aspects of the Theory of Syntax. The M.I.T. Press, Cambridge (Ma.), 1965.
Thierry Coquand. Pattern matching with dependent types. Informal proceedings of the Logical Frameworks Workshop held at Båstad in 1992.
Gottlob Frege. Begriffsschrift. Louis Nebert, Halle A/S, 1879.
Petri Mäenpää. Semantical BNF. Manuscript, University of Helsinki, 1994. To appear.
Lena Magnusson and Bengt Nordström. The ALF Proof Editor and Its Proof Engine. In H. Barendregt and T. Nipkow, editors, Types for Proofs and Programs, pages 213–237. Lecture Notes in Computer Science 806, Springer-Verlag, Heidelberg, 1994.
Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, Naples, 1984.
Richard Montague. Formal Philosophy. Yale University Press, New Haven, 1974. Collected papers edited by Richmond Thomason.
Jan von Plato. The axioms of constructive geometry. To appear in the Annals of Pure and Applied Logic.
Aarne Ranta. Type Theoretical Grammar. Oxford University Press, Oxford, 1994a.
Aarne Ranta. Type theory and the informal language of mathematics. In H. Barendregt and T., Nipkow, editors, Types for Proofs and Programs, pages 352–365. Lecture Notes in Computer Science 806, Springer-Verlag, Heidelberg, 1994b.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ranta, A. (1995). Syntactic categories in the language of mathematics. In: Dybjer, P., Nordström, B., Smith, J. (eds) Types for Proofs and Programs. TYPES 1994. Lecture Notes in Computer Science, vol 996. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60579-7_9
Download citation
DOI: https://doi.org/10.1007/3-540-60579-7_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60579-9
Online ISBN: 978-3-540-47770-9
eBook Packages: Springer Book Archive