In a rewriting system, suppose the production rule
<S>:=x<A>y<A>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
<v:A> instead of
<A>: a kind of "typed variable", whose type is a nonterminal symbol and the variable is the same substitution for all its occurrences. Thus,
<v:A> 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?