Enhancing Utility of Modular Properties of Term Rewriting Systems

摘要

A property P of term rewriting systems, like for instance confluence or strongnormalization, is called modular if the fact that two term rewriting systems have that property is equivalent with the disjoint union of these two rewrite systems having that property. In the paper it will be shown that the requirement of disjunctness of function symbols of the two constituting term rewriting systems can be relaxed. This relaxation goes further than earlier attempts to weaken the disjunctness precondition. A condition will be presented under which two term rewriting systems with non-disjunct sets of function symbols can be transformed into disjoint systems while preserving the meaning of the union. The relaxation of the disjointness precondition is based on a partition of terms that may be useful for other purposes than modular composition of term rewriting systems.