https://hal.inria.fr/hal-01812800Feller, DavidDavidFellerULTRA (Useful Logics, Types, Rewriting and their Automation) group - HWU - Heriot-Watt University [Edinburgh]Wells, Joe B.Joe B.WellsKamareddine, FairouzFairouzKamareddineULTRA - Useful Logics, Types, Rewriting and their Automation - HWU - Heriot-Watt University [Edinburgh]Carlier, SebastienSebastienCarlierFrance-IOI - France-IOIWhat Does This Notation Mean Anyway?What Does This Notation Mean Anyway?HAL CCSD2018Set theoryFormal definitionNotationAbstract syntax[INFO.INFO-FL] Computer Science [cs]/Formal Languages and Automata Theory [cs.FL]Feller, David2018-06-11 19:00:282019-02-14 01:13:192018-06-12 15:07:44enConference papershttps://hal.inria.fr/hal-01812800/documentapplication/pdf1Following the introduction of BNF notation by Backus for the Algol 60 report and subsequent notational variants, a metalanguage involving formal“grammars” has developed for discussing structured objects in Computer Science and MathematicalLogic.We refer to this offspring of BNF as Math-BNF or MBNF,to the original BNF and its notational variants just as BNF,and to aspects common to both as BNF-style.MBNF is sometimes called abstract syntax, but we avoid that name because MBNF is in fact a concrete form and has a more abstract form.What all BNF-style notations share is the use of production rules roughly of this form:◯ ⩴ □₁ | ⋯ | □ₙNormally, such a rule says “every instance of □ᵢ for i ∈ {1, ..., n} is also an instance of ◯”.MBNF is distinct from BNF in the entities and operations it allows.Instead of strings, MBNF builds arrangements of symbols that we callmath-text.Sometimes “syntax” is defined by interleaving MBNF production rulesand other mathematical definitions that can contain chunks ofmath-text.There is no clear definition of MBNF.Readers do not have a document which tells them how MBNF is to be readand must learn MBNF through a process of cultural initiation.To the extent that MBNF is defined, it is largely through examplesscattered throughout the literature.This paper gives MBNF examples illustrating some of the differencesbetween MBNF and BNF.We propose a definition of syntactic math text (SMT) whichhandles many (but far from all) uses of math-text and MBNF in thewild.We aim to balance the goal of being accessible and not requiring toomuch prerequisite knowledge with the conflicting goal of providing arich mathematical structure that already supports many uses and haspossibilities to be extended to support more challenging cases.