Complexity of Deciding Syntactic Equivalence up to Renaming for Term Rewriting Systems (Extended Version)

Inspired by questions from program transformations, eight notions of isomorphisms between term rewriting systems are defined, analysed and classified. The notions include global isomorphisms where the renaming of variables and / or function symbols is the same for all term rewriting rules of the system, and local ones where a single renaming for every rule is used. The complexity of the underlying decision problems are analysed and either shown to be efficiently solvable or proved to be complete for the graph isomorphism complexity class.