Church-Rosser Properties of Weakly Terminating Term Rewriting Systems

Abstract

The well known Knuth and Bendix completion procedure computes a convergent term rewriting system from a given set of equational axioms. This procedure was extended to handle mixed sets of rules and equations in order to deal with axioms that cannot be used as rules without loosing the required termination property. The developed technique requires the termination property of the rules model of computation, assuming the termination property of the set of rules only. We show that two abstract properties, "uniform confluence modulo " and "uniform coherence modulo " are both necessary and sufficient ones to compute with these models. We then give sufficient properties that can be checked on "parallel critical pairs", assuming the rules are left linear. These results allow to deal with sets of axioms including coramutativity, associativity and idempotency.