================================================================================
P9615   S.P. Luttik & P.H. Rodenburg
        "Transformations of reduction systems"


We consider transformations of reduction systems in an abstract setting. We
study some sets of correctness criteria for such transformations, adapt a
notion of simulation proposed by Kamperman and Walters, and show that the
resulting omega-simulation behaves well w.r.t. the criteria. In particular,
we prove that this notion implies preservation of the normal form relation,
confluence and weak termination.

We apply these results in an investigation of a transformation proposed by
Thatte. Rakesh Verma claimed that `weak persistence' was sufficient a
condition on term rewriting systems to obtain that this transformation
preserves confluence. However, we found counterexamples (that we included
in an appendix) that demonstrate that Verma's proof of this claim is
invalid. Upon notification of these errors, Verma found a counterexample to
his claim.

We show that for some important subclasses of the class of term rewriting
systems weak persistence is sufficient to obtain that the transform
omega-simulates the original under Thatte's transformation. This implies
preservation of confluence. Eventually, our investigations lead to a proof
that weak persistence suffices for preservation of semi-completeness.