Infinite normal forms for non-linear term rewriting systems

Recently, a great amount of work has been dedicated to the study of non-terminating rewriting relations. These attempts have the merit of sheding light on the nature of non-terminating relations thus permitting to extend the rewriting setting to a number of interesting equational theories. In this paper we discuss the applicability of the framework defined in [DK89, DKP89, DKP91] about the existence of infinite normal forms on a particular class of non-left-linear term rewriting systems. The approaeh has been used in [IN90b] to prove the existence of infinite normal forms for recursive (finite state) CCS expressions [MiI80] with respect to a correct and complete axiomatization of the observational congruence given by Milner [Mil89]. In fact, our interest in non-terminating non-linear rewriting systems comes from the experience we have made by developing verification techniques for the CCS language based on term rewriting [DIN90, IN90a]. In that framework it results that all the axiomatic characterizations of the various behavioural equivalences contain non-left-linear rules. On the other hand, non-termination arises as soon as one wants to consider recursive processes.