zbMATH — the first resource for mathematics

BNF-style notation as it is actually used. (English) Zbl 1428.68350
Kaliszyk, Cezary (ed.) et al., Intelligent computer mathematics. 12th international conference, CICM 2019, Prague, Czech Republic, July 8–12, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11617, 187-204 (2019).
Summary: The famous BNF grammar notation, as introduced and used in the Algol 60 report, was subsequently followed by numerous notational variants (EBNF, ABNF, RBNF, etc.), and later by a new formal “grammars” metalanguage used for discussing structured objects in Computer Science and Mathematical Logic. We refer to this latter offspring of BNF as MBNF (Math-BNF), and to aspects common to MBNF, BNF, and its notational variants as BNF-style. MBNF is sometimes called “abstract syntax”, but we avoid that name because MBNF is in fact a concrete form and there is a more abstract form. What all BNF-style notations share is the use of production rules like (P) below which state that “every instance of \(\circ_i\) for \(i \in \{1,\dots,n\}\) is also an instance of \(\bullet \)”. \[\bullet ::=\circ_i\mid\dots\mid\circ_n\tag{P}\] However, MBNF is distinct from all variants of BNF in the entities and operations it allows. Instead of strings, MBNF builds arrangements of symbols that we call math-text and allows “syntax” to be built by interleaving MBNF production rules and other mathematical definitions that can contain chunks of math-text. The differences between BNF (or its variant forms) and MBNF have not been clearly presented before. (There is also no clear definition of MBNF anywhere but this is beyond the scope of this paper.)
This paper reviews BNF and some of its variant forms as well as MBNF, highlighting the differences between BNF (including its variant forms) and MBNF. We show via a series of detailed examples that MBNF, while superficially similar to BNF, differs substantially from BNF and its variants in how it is written, the operations it allows, and the sets of entities it defines. We also argue that the entities MBNF handles may extend far outside the scope of rewriting relations on strings and syntax trees derived from such rewriting sequences, which are often used to express the meaning of BNF and its notational variants.
For the entire collection see [Zbl 1428.68028].
68V25 Presentation and content markup for mathematics
68Q42 Grammars and rewriting systems
ALGOL 60; MLsub; Ott; MathML
Full Text: DOI