Abstract
The problem of termination of a set R of rules modulo a set E of equations, called E-termination problem, arises when trying to complete the set of rules in order to get a Church-Rosser property for the rules modulo the equations. We first show here that termination of the rewriting relation and E-termination are the same whenever the used rewriting relation is E-commuting, a property inspired from Peterson and Stickel’s E-compatibility property. More precisely, their results can be obtained by requiring termination of the rewriting relation instead of E-termination if E-commutation is used instead of E-compatibility. When the rewriting relation is not E-commuting, we show how to reduce E-termination for the starting set of rules to classical termination of the rewriting relation of an extended set of rules that has the E-commutation property. This set can be classicaly constructed by computing critical pairs or extended pairs between rules and equations, according to the used rewriting relation. In addition we show that different orderings can be used for the starting set of rules and the added critical or extended pairs. Interesting issues for further research are also discussed.
Research supported in part by Agenee pour le Developpement de l’Informatique under contract 82/767 and for another part by Office of Naval Research under contract N00014-82-0333.
Part of this work was done while the second author was visiting the Centre de Recherche en Informatique de Nancy and another part while the first author was visiting the Stanford Research Institute, Computer Science Laboratory, 333 Ravenswood Avenue, Menlo Park, CA 94025, USA.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Choque, G. Calcul d’un ensemble complet d’incrementations minimales pour l’ordre recursif de decomposition. Technical Report, CRIN, Nancy, France, 1983.
Dershowitz, N. Ordering for Term-rewriting Systems. Journal of Theoretical Computer Science 17(3):279–301, 1982. Preliminary version in 20th FOCS, 1979.
Dershowitz, N., Hsiang, J., Josephson, N. and Plaisted, D. Associate-Commutative Rewriting. Proceedings 10th IJCAI, 1983.
Huet, G. Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems. Journal of the Association for Computing Machinery 27:797–821, 1980. Preliminary version in 18th FOCS, IEEE, 1977.
Huet, G. and Oppen, D. Equations and Rewrite Rules: A Survey. In Book, R. (editor), Formal Language Theory: Perspectives and Open Problems,. Academic Press, 1980.
Jouannaud, J.P. Church-Rosser Computations with Equational Term Rewriting Systems. Technical Report, CRIN, Nancy, France, January, 1983. Preliminary version in Proc. 5th CAAP, 1983, to appear in Springer Lecture Notes in Computer Science.
Jouannaud, J.P. and Kirchner, H. Completion of a set of rules modulo a set of Equations. Technical Report, SRI-International, 1984. Preliminary version in Proceedings 11th ACM POPL Conference, Salt Lake City, 1984, submitted to the SIAM Journal of Computing.
Jouannaud, J.P., Lescanne, P. On Multiset Ordering. Information Processing letters 15(2), 1982.
Jouannaud, J.P., Kirchner, C. and Kirchner, H. Algebraic manipulations as a unification and matching strategy for equations in signed binary trees. Proceedings 7th International Joint Conference on Artificial Intelligence, Vancouver, 1981.
Jouannaud, J.-P., Lescanne, P., Reinig, F. Recursive Decomposition Ordering. In IFIP Working Conference on Formal Description of Programming Concepts II,. North-Holland, 1983, edited by D. Bjorner., 1983.
Kamin, S. and Levy, J.J. Attempts for generalizing the recursive path ordering. 1980. Unpublished draft.
Kirchner, C. and Kirchner, H. Resolution d’ equations dans les Algebres libres et les varietes equationelles d’Algebres. PhD thesis, Universite Nancy I, 1982.
Knuth, D. and Bendix, P. Simple Word Problems in Universal Algebra. In J. Leech (editor), Computational Problems in Abstract Algebra,. Pergamon Press, 1970.
Lankford, D. and Ballantyne, A. Decision Procedures for Simple Equational Theories with Commutative Axioms: Complete Sets of Commutative Reductions. Technical Report, Univ. of Texas at Austin, Dept. of Mathematics and Computer Science, 1977.
Lankford, D. and Ballantyne, A. Decision Procedures for Simple Equational Theories with Permutative Axioms: Complete Sets of Permutative Reductions. Technical Report, Univ. of Texas at Austin, Dept. of Mathematics and Computer Science, 1977.
Lankford, D. and Ballantyne, A. Decision Procedures for Simple Equational Theories with Associative Commutative Axioms: Complete Sets of Associative Commutative Reductions. Technical Report, Univ. of Texas at Austin, Dept. of Mathematics and Computer Science, 1977.
Lescanne P. Computer Experiments with the REVE Term Rewriting Systems Generator. In Proceedings, 10th POPL,. ACM, 1983.
Lescanne, P. How to prove termination? An approach to the implementation of a new Recursive Decomposition Ordering. Proceedings 6th CAAP, Bordeaux, 1984.
Manna, Z. and Ness, N. On the Termination of Markov Algorithms. Proceedings of the third Hawaii Conference on System Sciences, 1970.
Munoz, M. Probleme de terminaison finie des systemes de reecriture equationnels. PhD thesis, Universite Nancy 1, 1983.
Peterson, G. and Stickel, M. Complete Sets of Reductions for Some Equational Theories. JACM 28:233–264, 1981.
Plaisted, D. A Recursively Defined Ordering for Proving Termination of Term Rewriting Systems. Technical Report R-78-943, University of Illinois, Computer Science Department, 1978.
Plaisted, D. An associative path ordering. Technical Report, University of Illinois, Computer Science Department, 1983.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1984 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jouannaud, JP., Munoz, M. (1984). Termination of a Set of Rules Modulo a Set of Equations. In: Shostak, R.E. (eds) 7th International Conference on Automated Deduction. CADE 1984. Lecture Notes in Computer Science, vol 170. Springer, New York, NY. https://doi.org/10.1007/978-0-387-34768-4_11
Download citation
DOI: https://doi.org/10.1007/978-0-387-34768-4_11
Publisher Name: Springer, New York, NY
Print ISBN: 978-0-387-96022-7
Online ISBN: 978-0-387-34768-4
eBook Packages: Springer Book Archive