Istituto di Scienza e Tecnologie dell'Informazione     
Inverardi P., Nesi M. Infinite normal forms for non-linear term rewriting systems. In: Mathematical Foundations of Computer Science 1991. 16th International Symposium. (Kazimierz Dolny, Poland, 9 - 13 September 1991). Proceedings, pp. 231 - 239. Andrzej Tarlecki (ed.). Springer-Verlag, 1991.
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.
Subject CCS

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional