Abstract
BNF (Backus Naur Formalism) grammar is extended by semantic structures. This yields a grammatical formalism that describes semantics uniformly with syntax, semantical BNF. It is formulated in type theoretical grammar, which is a categorial grammar designed for natural languages and formulated in constructive type theory. Semantical BNF applies type theoretical grammar to formal languages, in particular programming languages.
From the point of view of BNF, semantical BNF extends its productions by semantic structures. They allow the grammarian to write rules that generate only semantically as well as syntactically well-formed expressions. This stands in contrast to approaches to grammar in terms of BNF such as attribute grammar. They first generate expressions by BNF productions. Then a separate phase of type checking discards those expressions which are syntactically well-formed but meaningless, i.e. semantically ill-formed. Furthermore, this type checking phase typically does not relate to the syntactic phase of generation in a theoretically rigorous way. Semantical BNF integrates these two phases in terms of a uniform syntactic-semantic grammatical formalism.
From the point of view of constructive type theory, semantical BNF can be seen as its extension with syntactic categories. This allows making syntactic distinctions that are otherwise unavailable in constructive type theory. They are necessary for describing the abstract syntax of a language, and can also be used to vary concrete syntax. A mathematical interpretation function maps the extension back into constructive type theory.
To show how a formal language with variables is described grammatically, Knuth's binary number grammar is interpreted as a semantical BNF grammar, and extended into a small, functional language with typed lambda terms. Semantical BNF is also related to standard contemporary grammars of programming languages that use denotational semantics and to the theory of higher-order abstract syntax.
Preview
Unable to display preview. Download preview PDF.
References
Alfred V. Aho, Ravi Sethi, and Jeffrey D. Ullman. Compilers, Principles, Techniques, and Tools. Addison-Wesley, Reading, Massachusetts, 1986.
N. G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae, 34:381–392, 1972. Reprinted in R. Nederpelt et al., editors, Selected Papers on Automath, pages 865–935. North-Holland, Amsterdam, 1994.
Joëlle Despeyroux, Amy Felty, and André Hirschowitz. Higher-order abstract syntax in Coq. In M. Dezani and G. Plotkin, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, pages 124–138. Lecture Notes in Computer Science 902, Springer-Verlag, Heidelberg, 1995.
Donald E. Knuth. Semantics of context-free languages. Mathematical Systems Theory, 2:127–145, 1968. Errata 5:95–96, 1971.
Donald E. Knuth. Examples of formal semantics. In E. Engeler, editor, Symposium on Semantics of Algorithmic Languages, pages 212–235. Lecture Notes in Mathematics 188, Springer-Verlag, Heidelberg, 1971.
Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, Naples, 1984.
Richard Montague. Formal Philosophy Collected papers edited by Richmond Thomason. Yale University Press, New Haven, 1974.
Aarne Ranta. Type Theoretical Grammar. Oxford University Press, Oxford, 1994.
Aarne Ranta. Type-theoretical interpretation and generalization of phrase structure grammar. Bulletin of the IGPL, 3:319–342, 1995a.
Aarne Ranta. Syntactic categories in the language of mathematics. In P. Dybjer, B. Nordström, and J. Smith, editors, Types for Proofs and Programs, pages 162–182. Lecture Notes in Computer Science 996, Springer-Verlag, Heidelberg, 1995b.
Aarne Ranta. Context-dependent syntactic categories and the formalization of mathematical text. In S. Berardi and M. Coppo, editors, Types for Proofs and Programs, pages 162–182. Lecture Notes in Computer Science 1158, Springer-Verlag, Heidelberg, 1996.
Aarne Ranta. Structures grammaticales dans le français mathématique. To appear in Mathématiques Informatique, Sciences humaines, 1997.
David A. Schmidt. The Structure of Typed Programming Languages. MIT Press, Massachusetts, 1994.
Alvaro Tasistro. Formulation of Martin-Löf's theory of types with explicit substitutions. Licentiate's thesis, Chalmers University of Technology and University of Göteborg, 1993.
R. D. Tennent. Semantics of Programming Languages. Prentice Hall, New York, 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mäenpää, P. (1998). Semantical BNF. In: Giménez, E., Paulin-Mohring, C. (eds) Types for Proofs and Programs. TYPES 1996. Lecture Notes in Computer Science, vol 1512. Springer, Berlin, Heidelberg . https://doi.org/10.1007/BFb0097793
Download citation
DOI: https://doi.org/10.1007/BFb0097793
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65137-6
Online ISBN: 978-3-540-49562-8
eBook Packages: Springer Book Archive