Formal grammar with variables for consistent substitutions In a rewriting system, suppose the production rule S→xAyAz (or &lt;S&gt;:=x&lt;A&gt;y&lt;A&gt;z, in BNF), where S and A are nonterminal symbols and x, y, z are any string.

This rule produces the string xa1ya2z, where a1 and a2 are strings substituted by the nonterminal symbol A. The substitutions a1 and a2 may be equal or different strings.

But what if I want to a1 and a2 to be the same string; that is, if the nonterminal A be substituted by the same instance in both its occurrences in that production rule?

I used a kind of BNF I created informally for such purpose, with &lt;v:A&gt; instead of &lt;A&gt;: a kind of "typed variable", whose type is a nonterminal symbol and the variable is the same substitution for all its occurrences. Thus, &lt;S&gt;:=x&lt;v:A&gt;y&lt;v:A&gt;z, and &lt;v:A&gt; is substituted for the same string in its both occurrences.

What is the name of such a grammar that uses variables for consistent substitution of a nonterminal? And there is a grammar formalism for it?
You've created an affix grammar, so named because they were created to deal with affixes (prefixes and suffixes) in natural languages.

Specifically, this is a type of affix grammar where the "affixes" (what you call typed variables) are defined by the same type of grammar rather than coming from a simpler (finite) grammar. This creates a two-level grammar, specifically a type known as a Van Wijngaarden grammar after its creator.

It turns out that this type of grammar is in fact Turing-complete, so non-trivial semantic properties of such grammars are undecidable by Rice's theorem. On the one hand this makes them extremely powerful; on the other hand, it makes them not as useful in practice, since you could use some other Turing-complete system instead.