Abstract
We define an ordering called transformation ordering which is useful for proving termination of rewriting systems. A transformation ordering is defined using two relations: a relation which transforms terms and a relation which ensures the well-foundedness of the ordering. A property between these two relations called cooperation is required. Cooperation is similar to confluence and thus may be localized. Therefore, if relations are rewrite relations, it is possible to decide the cooperation by looking at critical pairs. Transformation orderings prove termination of rewriting systems that cannot be proved by the classical methods.
Chapter PDF
Similar content being viewed by others
References
L. Bachmair and N. Dershowitz, "Commutation, Transformation, and Termination," in Proc. 8th Conf. on Automated Deduction, Lecture Notes in Computer Science, vol. 230, Springer Verlag, Oxford (England), 1986.
L. Bachmair and D. Plaisted, "Associative Path Orderings," in tProc. 1st Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 202, pp. 241–254, Springer Verlag, Dijon (France), 1985.
J. Backus, "Can Programming Be Liberated From the Von Neumann Style? A Functional Style And Its Algebra of Programs," Comm. of ACM, vol. 21, no. 8, pp. 613–641, 1978.
F. Bellegarde, "Utilisation des Systèmes de Réécriture d'Expressions Fonctionnelles comme outiles de Transformation de Programmes Itératifs," Thèse de doctorat d'Etat, Université de Nancy I, Dept. Mathématiques Appliquées, 1985.
F. Bellegarde, "Rewriting Systems on FP Expressions to reduce the number of Sequences Yielded." Science of Computer Programming, vol. 6. pp. 11–34, North-Holland, 1986.
F. Bellegarde and P. Lescanne, "Termination Proofs Based On Transformation Techniques," Submitted To Information and Control, 1986.
N. Dershowitz, "Termination," in Proc. 1rst Conf. Rewriting Techniques and Applications, Lecture Notes in Computer Science, Vol. 202, pp. 180–224, Springer Verlag, Dijon (France), May 1985.
I. Gnaedig and P. Lescanne, "Proving Termination of Associative Commutative Rewriting Systems by Rewriting," Proceedings 8th International Conference on Automated Deduction, Oxford (England), 27–31 July 1986.
G. Huet and D. Oppen, "Equations and Rewrite Rules: A Survey," in Formal Languages: Perspectives And Open Problems, ed. Book R., Academic Press, 1980.
S. Kamin and J.J. Levy, "Attempts for Generalizing the Recursive Path Ordering," Inria, Rocquencourt, 1982, University of Illinois Report.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1987 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bellegarde, F., Lescanne, P. (1987). Transformation ordering. In: Ehrig, H., Kowalski, R., Levi, G., Montanari, U. (eds) TAPSOFT '87. CAAP 1987. Lecture Notes in Computer Science, vol 249. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-17660-8_48
Download citation
DOI: https://doi.org/10.1007/3-540-17660-8_48
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-17660-2
Online ISBN: 978-3-540-47746-4
eBook Packages: Springer Book Archive