I just came across the following grammar definition:

CommentChar ::

      SourceCharacter but not LineTerminator

But for discussion, I'll present this similar construct:

Digit ::

       '0' | '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9'

Zero ::


NonZeroDigit ::

       Digit but not Zero

Is this "but not" construct common in formal grammar specifications? If there a name for it?

I realize that NonZeroDigit could be defined by "manually" expanding the nonterminals and finding the difference -- here that process is as straightforward as it gets. But for more complicated "but not" constructs, I imagine that would be painful and error-prone.

Or, in grammars that support it, is this just considered just a sequence of (a) a negative lookahead (for Zero) combined with (b) the nonterminal for Digit.

  • 10
    $\begingroup$ You can read "but" as "and" here. Any help? $\endgroup$ Mar 22 '20 at 21:11
  • 2
    $\begingroup$ @RickDecker surprisingly (to me, but probably not you), that helps tremendously. Thank you. $\endgroup$
    – jedwards
    Mar 22 '20 at 22:22
  • $\begingroup$ Presumably, these things are used as shorthands in lexer definitions. As long as regular (or even finite) languages are concerned, it's not an issue REG is closed against complement and difference. $\endgroup$
    – Raphael
    Mar 22 '20 at 22:28
  • 1
    $\begingroup$ @raphael: those examples are lexical rules but the construct is mostly used in the syntactic grammar, to remove certain semireserved words from a lexical category. In that sense, it breaks into the lexical abstraction. For example, there's a rule "FragmentName: Name but not on*". Name is a lexeme here; *on is one of its possible values. The lexer does not identify on, but int a context where *Name might be reduced to FragmentName, one has to look at the precise spelling of the Name to see if the reduction is possible. $\endgroup$
    – rici
    Mar 23 '20 at 0:04
  • 1
    $\begingroup$ @raphael: precisely, but for a different reason. CFG is closed against difference with REG. $\endgroup$
    – rici
    Mar 23 '20 at 0:09

For context-free grammars (I guess your question concerns this type of formal grammars), it would be not only painful, but also impossible in general.

Suppose we have an algorithm that provides such "expansion" and yields a new grammar without $\text{but not }$occurrences. Then we can take two arbitrary context-free languages $L, L'$ with start nonterminals $A, A'$ respectively, write down a rule $B \longrightarrow A \text{ but not } A'$, run the algorithm on it, and get a context-free grammar for $L\backslash L'$. It contradicts a well-known fact that difference of two context-free languages can be not context-free.

  • $\begingroup$ While correct, this may be missing the mark: the application at hand might be restricted to regular languages. $\endgroup$
    – Raphael
    Mar 22 '20 at 22:29
  • $\begingroup$ @raphael: it's not restricted to regular languages (at least in theory) but the exclusions seem to always be a finite set. $\endgroup$
    – rici
    Mar 22 '20 at 23:46
  • $\begingroup$ @rici I would stress that you talking about final set of words, not final set of nonterminals. $\endgroup$
    – Vladislav
    Mar 23 '20 at 6:30
  • $\begingroup$ @vlad: well, both sets are finite :-) but yes, that's what I meant. The question is, was that the intention for the notation, or is it just that this particular grammar didn't happen to use infinite exception sets. $\endgroup$
    – rici
    Mar 23 '20 at 13:57

In the case of regular languages (and in your examples, we're just talking about character classes, which are an especially simple form of regular language), they are closed under set difference. Not only that, but unlike (say) Thompson's method, Brzozowski's method for constructing DFAs can be easily extended to handle the set difference operator.

I'm going to use ring notation, because Brzozowski's algorithm looks much neater that way.

  • $0$ is the language with no strings in it (i.e. the empty set), and $1$ is the language containing just the zero-length string.
  • $E_1 + E_2$ is the set union of $E_1$ and $E_2$.
  • $E_1 E_2$ is the language concatenation operator.
  • $E^*$ is the Kleene closure of $E$.
  • $E_1 - E_2$ is the set difference.

Now we introduce some additional notation.

$E(0)$ is $1$ if $1 \in E$, otherwise $0$. You can compute this by replacing all of the terminal symbols in $E$ with $0$ and simplifying; if you think of the terminal symbols as "variables", this is what you get by "evaluating" the expression at $0$.

If it seems unclear as to why you would think of terminal symbols as "variables", then the Brzozowski derivative should make this much more obvious. If $a, b, \ldots$ are terminal symbols, recursively define the Brzozowski derivative as:

$$\begin{align*} \frac{\partial}{\partial a} a & = 1 \\ \frac{\partial}{\partial a} b & = 0 \\ \frac{\partial}{\partial a} \left( E_1 + E_2 \right) & = \frac{\partial}{\partial a} E_1 + \frac{\partial}{\partial a} E_2 \\ \frac{\partial}{\partial a} E^* & = \frac{\partial}{\partial a} E\,E^* \\ \frac{\partial}{\partial a} \left(E_1 E_2 \right) & = \frac{\partial}{\partial a} E_1\, E_2 + E_1(0)\,\frac{\partial}{\partial a} E_2 \\ \frac{\partial}{\partial a} \left( E_1 - E_2 \right) & = \frac{\partial}{\partial a} E_1 - \frac{\partial}{\partial a} E_2 \end{align*}$$

The interesting things to note:

  • Terminal symbols act like variables.
  • Addition and subtraction (i.e. set union and set difference) behave normally.
  • Kleene closure acts like $e^x$ (i.e. $\frac{\partial}{\partial x} e^{E} = \frac{\partial E}{\partial x} e^{E}$).
  • Concatenation acts a bit like a product, but it's asymmetrical.

(Exercise: Suppose there was another product operator which obeyed the symmetric product rule $\frac{\partial}{\partial a} \left(E_1 \times E_2 \right) = \frac{\partial E_1}{\partial a} \times E_2 + E_1 \times \frac{\partial E_2}{\partial a}$. What would that operator mean?)

Then Taylor's theorem for regular languages states:

$$E = E(0) + a \frac{\partial E}{\partial a} + b \frac{\partial E}{\partial b} + \cdots$$

where the sum is taken over all terminal symbols. This gives an expansion for a DFA state. The first term, $E(0)$, tells you whether the expression represents a final state or not, and the other terms give the transitions.

So, for example, if we want to construct the DFA for $q_0 = (a + b)^* - (a + b)^* a a (a + b)^*$, we just do the expansion.

$$\begin{align*} q_0(0) & = (0 + 0)^* - (0 + 0)^* 0 0 (0 + 0)^* = 1 \\ \frac{\partial q_0}{\partial a} & = \frac{\partial}{\partial a}(a + b)^* - \frac{\partial}{\partial a} \left( (a + b)^* a a (a + b)^* \right) \\ & = \frac{\partial}{\partial a}(a + b) \, (a + b)^* - \left( \frac{\partial}{\partial a} (a + b)^* \left( (a + b)^* a a (a + b)^* \right) + \left( (a + b)^* \right)(0) \frac{\partial}{\partial a} \left( a a (a + b)^* \right) \right) \\ & \hbox {(some calculation later)} \\ & = (a + b)^* - \left( (a + b)^* a a (a + b)^* + a (a + b)^* \right) \\ \frac{\partial q_0}{\partial b} & = (a + b)^* - \left( (a + b)^* a a (a + b)^* \right) \end{align*}$$

That is:

$$q_0 = 1 + a\,q_1 + b\,q_0$$


$$q_1 = (a + b)^* - \left( (a + b)^* a a (a + b)^* + a (a + b)^* \right)$$

That is, the start state is a final state, with a $b$ transition back to itself, and an $a$ transition to the next state, which we can then calculate using the same method.

  • $\begingroup$ Does "if $1\in E$" check if $E$ contains the empty word? $\endgroup$
    – chi
    Mar 23 '20 at 8:27
  • $\begingroup$ Yes. Substituting $0$ into $E$ does the same thing as checking that $1 \in E$. $\endgroup$
    – Pseudonym
    Mar 23 '20 at 23:06
  • $\begingroup$ So you use 1 for both the empty word and the language containing the empty word. I see, I was mildly confused at first. $\endgroup$
    – chi
    Mar 23 '20 at 23:34
  • $\begingroup$ Yes, sorry about that. Notation overloading is ubiquitous in formal language theory; it's like how we just say $a$ to refer the terminal symbol, the string of length 1, and the language containing just that string. $\endgroup$
    – Pseudonym
    Mar 24 '20 at 0:31
  • 1
    $\begingroup$ Sure. Somehow I was accustomed to $a$ being used as a one-symbol word and a language, but somehow still kept $\epsilon$ and $\{\epsilon\}$ separate. $\endgroup$
    – chi
    Mar 24 '20 at 8:35

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.

That phrasing is certainly not unique to GraphQL. ECMA-262, which defines the language formerly known as Javascript, contains virtually the same wording in the description of the formalism it uses:

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 : vs. :: 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.

Semantically, 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:

EnumValue :
     Name but not true or false or null

FragmentName :
     Name but not on

Similarly, in ECMA-262 we find

Identifier :
     IdentifierName but not ReservedWord

[Note 2]

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.
          —(§9.8/1, [stmt.ambig])

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.


  1. 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

              —(§5.13.3, [lex.ccon])

  2. 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:

    BlockStringCharacter ::
        SourceCharacter but not """ or \"""

    Here, neither """ nor \""" are in SourceCharacter, so the restriction has no effect. What was intended was something like

    NoTripleQuote ::
        SourceCharacterlist but not SourceCharacterlist,opt """ SourceCharacterlist,opt
    BlockStringCharacterList ::
        BlockStringCharacterListopt \""" NoTripleQuoteopt 
  3. 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.

  • $\begingroup$ Facebook is at least a distant contributor to ECMAScript, even if they're not necessarily sitting on the TC39 committee, so I wouldn't be surprised if there was some cross-pollination in the writing style of the two specs. $\endgroup$ Mar 24 '20 at 7:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.