The particular grammar formalism used in the grammar you cite is defined in Appendix A of that document, which includes in section A.3, a precise definition:
A grammar production may specify that certain expansions are not permitted by using the phrase “but not” and then indicating the expansions to be excluded.
The right-hand side of a production may specify that certain expansions are not permitted by using the phrase “but not” and then indicating the expansions to be excluded.
Although the grammar formalisms are not identical, I think the authors of the GraphQL document were influenced, at least, by the ECMAScript formalism, since there is quite a lot of overlap (and the typography is also very similar). They also share the use of
:: to distinguish between syntactic and lexical rules, the use of negative lookahead rules of the form
[ lookahead ∉ Set ], parameterised non-terminal symbols using bracketed subscripts, and the use of the subscript
opt to indicate optional elements in right-hand side. GraphQL adds the use of the subscript
list for repeated elements. The
opt subscript convention is fairly widespread -- it's also used in the C and C++ formal specifications, for example. The other ones are less common.
(GraphQL also uses the phrase
one of in the same way that it is used in ECMA-262 and the C and C++ standards. However, the usage is not formally noted in the notation summary as far as I can see.)
Given the similarity, I'm assuming that the
but not from GraphQL and the one from ECMA-262 are the same operator, which only serves to increase the number of examples of use that I have available.
but not is not a lookahead assertion. Rather, it's the set difference operator. (As noted above, the grammar formalism has a negative lookahead assertion, but set difference does not have anything to do with lookahead.) The left-hand argument of
but not is the right-hand side of a production. In all the examples of use we have, it's a single a non-terminal but in theory it could be any sequence of non-terminals. (And that detail doesn't matter since it would always be possible to create a new non-terminal to avoid that restriction.) So the left-hand side refers to a possibly infinite context-free "language" (in the formal sense of the word: a set of sentences).
The right-hand side is less clear, since the documents only say "the expansions to be excluded". In both GraphQL and ECMA-262, there is a mechanism to create a union of exclusions. GraphQL is explicit: "A grammar may also list a number of restrictions after “but not” separated by
or". ECMA-262 uses the essentially the same form (except that the restriction list is then introduced with the words
one of), without bothering to provide a formal definition.
In practice, the exclusion set is always a finite set. In most cases, it is used to create what would be described as a character class in most regular expression libraries, as in the example of NonZeroDigit which you cite. This usage is widespread in both documents; it applies to a lexical rule (introduced with
::), and both the left- and right-hand sides of
but not are subsets of SourceCharacter. [Note 1]
But it is also used for a more interesting case: the distinction between Identifier and the various keyword tokens. In GraphQL, for example, we have:
Name but not true or false or null
Name but not on
Similarly, in ECMA-262 we find
IdentifierName but not ReservedWord
These are all syntactic rules, as indicated by the single
:, although both the left- and the right-hand sides use lexical symbols. Crucially, in all cases of this usage, the right-hand sides represent finite sets.
The question that then confronts us is whether the fact that the right-hand side of
but not is always finite is an unmentioned restriction on the formalism, or whether it simply reflects the fact that more complex uses were not necessary in these particular grammars.
Without the restriction, this formalism could be used to advantage in C++, for example. Consider the well-known parsing ambiguity which gives rise to the so-called "Most Vexing Parse", whose resolution is written in English in the C++ standard, rather than using any grammar formalism:
There is an ambiguity in the grammar involving expression-statements and declarations: An expression-statement with a function-style explicit type conversion as its leftmost subexpression can be indistinguishable from a declaration where the first declarator starts with a (. In those cases the statement is a declaration.
Using an unrestricted
but for operator, this could be written:
expression-statement : candidate-expression-statement but not declaration
where candidate-expression-statement is the previous definition of expression-statement. It is not immediately obvious whether the result is context-free or not, but the parsing strategy to handle it would reflect current practice: do both possible parses, perhaps in parallel, and if they both work then forget about the
expression-statement parse. (In the context of C++, it doesn't really matter whether or not this is context-free. C++ parsers already need to deal with many non-contet-free aspects.)
If this kind of ambiguity existed within GraphQL (or ECMA-262), then the failure to use
but not to express the resolution could be considered de facto evidence that the intention of the
but for formalism was that the right-hand side not be a general syntax object. While I haven't yet found an example of that, the fix to the error described in [Note 2] would involve a use of the
but for formalism in which the right-hand side was not finite. [Also see Note 3]
For what it's worth, I believe that the intention of the formalism was that the right-hand side be finite, but I obviously have no way to prove it. If so, then the
but not formalism does not add any expressive power to BNF, since the difference between a context-free language and a finite set (or, indeed, any regular language) is still context-free.
If, on the other hand, the intention was that
but not could remove an arbitrary subset of derivations described by a sequence of grammar symbols, then it would permit the definition of non-context-free grammars.
In C and C++, this sort of restriction is expressed as narrative. For example, a character literal is defined in BNF as a sequence of c-char enclosed between ' characters, with the following definition of c-char:
any member of the source character set except
the single-quote ', backslash \, or new-line character
The GraphQL document is marked as a draft, so it would be churlish to criticise it on the basis of small errors. However, I couldn't help noting that it includes an obvious misuse of the
but not operator:
SourceCharacter but not """ or \"""
Here, neither """ nor \""" are in SourceCharacter, so the restriction has no effect. What was intended was something like
SourceCharacterlist but not SourceCharacterlist,opt """ SourceCharacterlist,opt
BlockStringCharacterListopt \""" NoTripleQuoteopt
It would be possible to loosen the restriction to also allow infinite sets described by regular grammars, and the fix in [Note 2] is a regular grammar (although that might not be immediately obvious). However, describing that loosened description in the context of the documents in question would be require hauling in quite a lot of formal language theory which is otherwise unnecessary.