Algorithms and reductions for rewriting problems. II. (Q1853144)

In this paper we give polynomial-time reductions between a version of joinability for rewrite systems and the word problem for rewrite systems. We prove log-space hardness or completeness for \(P\) for several problems of ground rewrite systems. We show that matching (and unification) modulo ground equations is NP-hard even when variables are restricted to at most two occurrences in the pattern and the subject is just a constant. Finally, we give the first polynomial-time algorithms for matching modulo ground equations with linear pattern and for joinability problem with ground rewrite systems. The joinability result leads to polynomial time algorithms for: local confluence of ground rewrite systems, confluence of terminating ground rewrite systems, and completeness of ground rewrite systems. The results for matching modulo ground equations are optimal with respect to occurrences of variables.