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

TL;DR

This paper investigates various notions of isomorphism between term rewriting systems, analyzing their properties, and establishing the computational complexity of deciding such isomorphisms, including efficient algorithms and complexity classifications.

Contribution

It introduces new notions of isomorphisms, analyzes their semantic preservation, and provides algorithms and complexity results for deciding these isomorphisms.

Findings

Some isomorphism problems are efficiently solvable.

Other isomorphism problems are complete for the graph isomorphism class.

Algorithms for computing templates and maximal normal forms are presented.

Abstract

Motivated 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 function symbols is the same for all term rewriting rules of the system, local ones, where a single renaming for every rule is used, and a combination, where one symbol set is renamed globally while the other set is renamed locally. Preservation of semantic properties like convertibility and termination is analysed for the different isomorphism notions. The notions of templates and maximal normal forms of term rewriting systems are introduced and algorithms to efficiently compute them are presented. Equipped with these techniques, the complexity of the underlying decision problems of the isomorphisms are analysed and either shown to be efficiently solvable or proved to be complete for the graph isomorphism complexity class.