Abstract
A new criterion for termination of rewriting has been described by Arts and Giesl in 1997. We show how this criterion can be generalized to rewriting modulo associativity and commutativity. We also show how one can build weak AC-compatible reduction orderings which may be used in this criterion.
This research was supported in part by the EWG CCL II, the HCM Network CON-SOLE, and the “GDR de programmation du CNRS”.
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
T. Arts. Automatically proving termination and innermost normalisation of term rewriting systems. PhD thesis, Universiteit Utrecht, 1997.
T. Arts and J. Giesl. Automatically proving termination where simplification orderings fail. In M. Bidoit and M. Dauchet, editors, Theory and Practice of Soßware Development, volume 1214 of Lecture Notes in Computer Science, Lille, France, Apr. 1997. Springer-Verlag.
L. Bachmair. Associative-commutative reduction orderings. Info Proc. Letters, 1992.
L. Bachmair and N. Dershowitz. Commutation, transformation, and termination. In J. H. Siekmann, editor, Proc. 8th Int. Conf. on Automated Deduction, Oxford, England, LNCS 230, pages 5–20, July 1986.
L. Bachmair and N. Dershowitz. Critical pair criteria for completion. Journal of Symbolic Computation, 6(1):1–18, 1988.
L. Bachmair, N. Dershowitz, and J. Hsiang. Orderings for equational proofs. In Proc. 1st IEEE Symp. Logic in Computer Science, Cambridge, Mass., pages 346–357, June 1986.
L. Bachmair and D. A. Plaisted. Termination orderings for associativecommutative rewriting systems. Journal of Symbolic Computation, 1(4):329–349, Dec. 1985.
A. Ben Cherifa and P. Lescanne. An actual implementation of a procedure that mechanically proves termination of rewriting systems based on inequalities between polynomial interpretations. In Proc. 8th Int. Conf. on Automated Deduction, Oxford, England, LNCS 230, pages 42–51. Springer-Verlag, July 1986.
H. Comon, editor. 8th International Conference on Rewriting Techniques and Applications, volume 1232 of Lecture Notes in Computer Science, Barcelona, Spain, June 1997. Springer-Verlag.
E. Contejean and C. Marché. CiME: Completion Modulo E. In H. Ganzinger, editor, 7th International Conference on Rewriting Techniques and Applications, volume 1103 of Lecture Notes in Computer Science, pages 416–419, New Brunswick, NJ, USA, July 1996. Springer-Verlag. System Description available at http: //www.lri. fr/~demons/cime. html.
E. Contejean, C. Marché, and L. Rabehasaina. Rewrite systems for natural, integral, and rational arithmetic. In Comon [9].
C. Delor and L. Puel. Extension of the associative path ordering to a chain of associative-commutative symbols. In Proc. 5th Rewriting Techniques and Applications, Montréal, LNCS 690, pages 389–404, 1993.
N. Dershowitz. Orderings for term rewriting systems. Theoretical Computer Science, 17(3):279–301, Mar. 1982.
N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3(1):69–115, Feb. 1987.
J. Giesl. Generating polynomial orderings for termination proofs. In J. Hsiang, editor, 6th International Conference on Rewriting Techniques and Applications, volume 914 of Lecture Notes in Computer Science, Kaiserslautern, Germany, Apr. 1995. Springer-Verlag.
G. Huet. A complete proof of correctness of the Knuth-Bendix completion algorithm. J. Comput. Syst. Sci., 23:11–21, 1981.
J.-P. Jouannaud and H. Kirchner. Completion of a set of rules modulo a set of equations. SIAM Journal on Computing, 15(4):1155–1194, 1986.
D. Kapur and G. Sivakumar. A total, ground path ordering for proving termination of AC-rewrite systems. In Comon [9].
D. E. Knuth. The art of computer programming, volume 2. Addison-Wesley, 2nd edition, 1981.
P. Lescanne. Uniform termination of term rewriting systems with status. In Proc. 9th CAAP, Cambridge, 1984. Cambridge University Press.
C. Marché. Réécriture modulo une théorie présentée par un système convergent et décidabilité des problèmes du mot dans certaines classes de théories équationnelles. Thèse de doctorat, Université Paris-Sud, Orsay, France, Oct. 1993.
C. Marché. Normalized rewriting: an alternative to rewriting modulo a set of equations. Journal of Symbolic Computation, 21(3):253–288, 1996.
R. Nieuwenhuis and A. Rubio. A precedence-based total AC-compatible ordering. In C. Kirchner, editor, Proc. 5th Rewriting Techniques and Applications, Montréal, LNCS 690. Springer-Verlag, June 1993.
G. E. Peterson and M. E. Stickel. Complete sets of reductions for some equational theories. J. ACM, 28(2):233–264, Apr. 1981.
J. Steinbach. Proving polynomials positive. In R. Shyamasundar, editor, Foundations of Software Technology and Theoretical Computer Science, volume 652 of Lecture Notes in Computer Science, pages 191–202, New Delhi, India, Dec. 1992. Springer-Verlag.
X. Urbain. Preuves de terminaison à l'aide de paires de dépendances. Rapport de DEA, Université Paris-Sud, Orsay, France, 1997.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag
About this paper
Cite this paper
Marché, C., Urbain, X. (1998). Termination of associative-commutative rewriting by dependency pairs. In: Nipkow, T. (eds) Rewriting Techniques and Applications. RTA 1998. Lecture Notes in Computer Science, vol 1379. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0052374
Download citation
DOI: https://doi.org/10.1007/BFb0052374
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64301-2
Online ISBN: 978-3-540-69721-3
eBook Packages: Springer Book Archive