Polynomial grammars with substitution

Polynomial grammars are grammars whose nonterminals generate tuples of integers (or elements of some ring in general) and productions use polynomial functions. They proved to be useful for proving decidability of equivalence of MSO transductions over strings and unordered trees and in general can be used for recursively defined functions on trees. In this talk we show two ways of adding substitution to polynomial grammar that preserve decidability of equivalence.