Abstract
A method based on polynomial interpretations is currently implemented in REVE. Though this termination check procedure is absolutely necessary in order to run some of the examples we know, like Associativity+Endomorphism, we do not think it will replace the current methods based on recursive path ordering [Dersh82] or recursive decomposition ordering [Jouan.etal.82], since they have shown to have a large scope and to be really easy to use in many practical cases [Forg&Det185], and Dershowitz has exhibited examples where polynomial interpretation fail [Dersh83]. So, we think we will keep both methods in REVE and let the user choose the method he or she wants to use. However in the case of associative-commutative operators, the methods based on extensions of the recursive path ordering either fail or are not ready for being incorporated in a rewrite rule laboratory like REVE. So, it is the only method currently available and we are incorporating it into REVE-3 (the general equational rewriting laboratory) as the mechanism for proving termination in the associative-commutative case.
In conclusion, we would like to mention a limit of our criterion. It cannot prove the positiveness of the polynomial x 21 +x 22 −2x1x2+1=(x1−x2)2+1. Since we never encountered such a polynomial in termination proofs we feel that would not be an obstacle for using it.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
L. Bachmair and D. Plaisted, ”Associative Path Orderings,” in Proc. 1st Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 202, pp. 241–254, Springer Verlag, Dijon (France), 1985.
L. Bachmair and D.A. Plaisted, ”Termination Orderings For Associative-Commutative Rewriting Systems,” Journal of Symbolic Computation, 1985.
F. Bellegarde, ”Rewriting Systems on FP Expressions that Reduce the Number of Sequences they yield,” in Symposium on LISP and Functional Programming, ACM, Austin, USA, 1984.
Nachum Dershowitz, ”Orderings for Term-Rewriting Systems,” Theoretical Computer Science, vol. 17, pp. 279–301, 1982.
N. Dershowitz, ”Well-Founded Orderings,” ATR-83(8478)-3, Information Science Research Office, The Aerospace Corporation, El Segundo, California (USA), May 1983.
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.
R. Forgaard and D. Detlefs, ”An incremental algorithm for proving termination of term rewriting systems,” in Proc. 1rst International Conference on Rewriting Techniques and Applications., Lecture Notes in Computer Science, vol. 202, Springer Verlag, Dijon (France), 1985.
G. Huet, ”Confluent reductions: abstract properties and applications to term rewriting systems,” J. of ACM, vol. 27, no. 4, pp. 797–821, Oct. 1980.
G. Huet and D. Oppen, ”Equations and Rewrite Rules: A Survey,” in Formal Languages: Perspectives And Open Problems, ed. Book R., Academic Press, 1980.
[Jouan.etal.82]. J.P. Jouannaud, P. Lescanne, and F. Reinig, ”Recursive Decomposition Ordering,” in Formal Description of Programming Concepts 2, ed. Bjorner D., pp. 331–346, North Holland, Garmish Partenkirschen, RFA, 1982.
D.S. Lankford, ”On Proving Term Rewriting Systems Are Noetherian,” Report Mtp-3, Math. Dept., Louisiana Tech University, May 1979.
P. Lescanne, ”Computer Experiments with the REVE Term Rewriting System Generator,” in 10th ACM Conf. on Principles of Programming Languages, pp. 99–108, Austin Texas, January 1983.
Z. Manna and S. Ness, ”On the Termination of Markov Algorithms,” Third Hawaii International Conference on System Sciences, pp. 789–792, 1970.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1986 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cherifa, A.B., Lescanne, P. (1986). An actual implementation of a procedure that mechanically proves termination of rewriting systems based on inequalities between polynomial interpretations. In: Siekmann, J.H. (eds) 8th International Conference on Automated Deduction. CADE 1986. Lecture Notes in Computer Science, vol 230. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16780-3_78
Download citation
DOI: https://doi.org/10.1007/3-540-16780-3_78
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-16780-8
Online ISBN: 978-3-540-39861-5
eBook Packages: Springer Book Archive