Linearizing Term Rewriting Systems Using Test Sets

Often non left-linear rules in term rewriting systems can be replaced by a finite set of left-linear ones without changing the set of irreducible ground terms. Using appropriate test sets, we can always decide if this is possible and, in case it is, effectively perform such a transformation. We thus can also decide if the set of irreducible ground terms is a regular tree language.