×

Termination orderings for associative-commutative rewriting systems. (English) Zbl 0587.68041

In this paper we describe a new class of orderings - associative path orderings - for proving termination of associative-commutative term rewriting systems. These orderings are based on the concept of simplification orderings and extend the well-known recursive path orderings to E-congruence classes, where E is an equational theory consisting of associativity and commutativity axioms. Associative path orderings are applicable to term rewriting systems for which a precedence ordering on the set of operator symbols can be defined that satisfies a certain condition, the associative path condition. These precedence ordering can often be derived from the structure of the reduction rules. We include termination proofs for various term rewriting systems (for rings, Boolean algebra, etc.) and, in addition, point out ways to handle situations where the associative path condition is too restrictive.

MSC:

68W30 Symbolic computation and algebraic computation

Software:

REVE; RRL
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Bachmair, L.; Dershowitz, N., Commutation, transformation, and termination (1985), (Submitted) · Zbl 0642.68036
[2] Dershowitz, N., A note on simplification orderings, Inf. Proc. Lett., 9, 212-215 (1979) · Zbl 0433.68044
[3] Dershowitz, N., Orderings for term-rewriting systems, Theor. Comp. Sci., 17, 279-301 (1982) · Zbl 0525.68054
[4] N., Dershowitz, Termination, Proc. First Int. Conf. on Rewriting Techniques and Applications (1985), Dijon, France, Lect. Notes in Comp. Scie., Springer · Zbl 0581.68031
[5] Dershowitz, N., Computing with rewrite systems, Inf. Control (1985), to appear · Zbl 0584.68020
[6] Dershowitz, N.; Manna, Z., Proving termination with multiset orderings, Commun ACM, 22, 465-476 (1979) · Zbl 0431.68016
[7] Dershowitz, N.; Hsiang, J.; Josephson, N. A.; Plaisted, D. A., Associative-commutative rewriting, Proc. 8th IJCAI, 940-944 (1983), Karlsruhe
[8] Guttag, J. V.; Kapur, D.; Musser, D. R., Abstract data types and software validation, Commun. ACM, 21, 1048-1064 (1978) · Zbl 0387.68012
[9] Hsiang, J., Refutational theorem proving using term-rewriting systems, Artif. Intell., 25, 255-300 (1985) · Zbl 0558.68072
[10] Huet, G., Confluent reductions: abstract properties and applications to term rewriting systems, J. Assoc. Comp. Mach., 27, 797-821 (1980) · Zbl 0458.68007
[11] Huet, G.; Lankford, D. S., On the uniform halting problem for term rewriting systems, Rapport Laboria, 283 (1978), IRIA
[12] Huet, G.; Oppen, D. C., Equations and rewrite rules: a survey, (Book, R., Formal Languages: Perspectives and Open Problems (1980), Academic Press: Academic Press New York), 349-405
[13] Hullot, J.-M., A catalogue of canonical term rewriting systems, Technical Report CSL-113 (1980), SRI International, Menlo Park, Calif
[14] Jouannaud, J.-P.; Kirchner, H., Completion of a set of rules modulo a set of equations, 11th ACM Symp. on Principles of Programming Languages, 83-92 (1984), Salt Lake City, Utah, January 15-16
[15] Jouannaud, J.-P.; Lescanne, P.; Reinig, F., Recursive decomposition ordering, (Bjorner, D., IFIP Working Conf: on Formal Description of Programming Concepts II (1983), North-Holland: North-Holland Amsterdam) · Zbl 0513.68026
[16] Jouannaud, J.-P.; Munoz, M., Termination of a set of rules modulo a set of equations, (Shostak, R., Proc. 7th Int. Conf. on Automated Deduction (1984)), 175-193, Springer Lec. Notes Comp.Sci.
[17] Kamin, S.; Levy, J. J., Two Generalizations of the Recursive Path Ordering, Unpublished memo (1980), Univ. of Illinois at Urbana-Champaign
[18] Kapur, D.; Narendran, P.; Sivakumar, G., A path ordering for proving termination of term rewriting systems, Proc. 10th Colloquium on Trees in Algebra and Programming (1985) · Zbl 0567.68026
[19] Kapur, D.; Sivakumar, G., Architecture of and experiments with RRL, a rewrite rule laboratory, (Proc. NSF, Workshop on the Rewrite Rule Laboratory (1983), Rensellaerville: Rensellaerville New York), 33-56
[20] Knuth, D.; Bendix, P., Simple word problems in universal algebras, (Leech, J., Computational Problems in Abstract Algebra (1970), Pergamon Press: Pergamon Press Oxford), 263-297 · Zbl 0188.04902
[21] Kruskal, J. B., Well-quasi-ordering,the tree theorem and Vazsonyi’s conjecture, Trans. Amer.Math .Soc., 95, 210-225 (1960) · Zbl 0158.27002
[22] Lankford, D., On Proving Term Rewriting Systems are Noetherian, Memo MTP-3 (1979), Mathematics Department, Lousiana Technical University: Mathematics Department, Lousiana Technical University Ruston, LA.
[23] Lankford, D.; Ballantyne, A., Decision Procedures for Simple Equational Theories with Associative Commutative Axioms: Complete Sets of Associative Commutative Reductions (1977), Univ. of Texas at Austin, Dept. of Math. and Comp. Scie, Technical Report
[24] Lescanne, P., Decomposition ordering as a tool to prove the termination of rewriting systems, Proc.7th IJCAI, 548-550 (1981), Vancouver, Canada
[25] Lescanne, P., Some properties of decomposition ordering,a simplification ordering to prove termination of rewriting systems, R.A.I.R.O. Informatique Theoretique/Theoretical Informatics, 16, 331-347 (1982) · Zbl 0518.68025
[26] Lescanne, P., Computer experiments with the REVE term rewriting system, Proc. 10th ACM Symp. on Principles of Programming Languages (1983)
[27] Manna, Z.; Ness, S., On the termination of Markov algorithms, Proc. 3rd Hawaii Int. Conf. on System Science, 789-792 (1970), Honolulu, Hawaii
[28] Munoz, M., Probleme de Terminaison Finie des Systemes de Reécriture Equationnels, Thesis, Université Nancy 1 (1983)
[29] Peterson, G. E.; Stickel, M. E., Complete sets of reductions for some equational theories, J. Assoc. Comp. Mach., 28, 233-264 (1981) · Zbl 0479.68092
[30] Plaisted, D. A., Well founded Orderings for Proving Termination of Systems of Rewrite Rules, (Dept. of Computer Science Report (1978), Univ. of Illinois at Urbana-Champaign), 78-932
[31] Plaisted, D. A., A Recursively Defined Ordering for Proving Termination for Term Rewriting Systems, (Dept. of Computer Science Report (1978), Univ. of Illinois at Urbana-Champaign), 78-943
[32] Plaisted, D. A., An associative path ordering, (Proc. NSF Workshop on the Rewrite Rule Laboratory (1983), Rensellaerville: Rensellaerville New York), 123-126
[33] Rusinowitch, M., Plaisted ordering and recursive decomposition ordering revisited, Proc. First Int.Conf. on Rewriting Techniques and Applications (1985), Springer Lec. Notes Comp.Sci. Dijon, France, in press · Zbl 0576.68016
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.