Abstract
In this paper the Recursive Path Ordering is adapted for proving termination of rewriting incrementally. The new ordering, called Recursive Path Ordering with Modules, has as ingredients not only a precedence but also an underlying ordering \(\sqsupset_{B}\). It can be used for incremental (innermost) termination proofs of hierarchical unions by defining \(\sqsupset_{B}\) as an extension of the termination proof obtained for the base system. Furthermore, there are practical situations in which such proofs can be done modularly.
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
Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science 236(1-2), 133–178 (2000)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Bendix, P.B., Knuth, D.E.: Simple word problems in universal algebras. In: Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press, Oxford (1970)
Borralleras, C.: Ordering-based methods for proving termination automatically. PhD thesis, Dpto. LSI, Universitat Politècnica de Catalunya, España (2003)
Borralleras, C., Ferreira, M., Rubio, A.: Complete monotonic semantic path orderings. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 346–364. Springer, Heidelberg (2000)
Calude, C.: Theories of Computational Complexity. North-Holland, Amsterdam (1988)
Calude, C., Marcus, S., Tevy, I.: The first example of a recursive function which is not primitive recursive. Historia Math. 9, 380–384 (1979)
Dershowitz, N.: Orderings for term rewriting systems. Theoretical Computer Science 17(3), 279–301 (1982)
Fernández, M.L.: Relaxing monotonicity for innermost termination. Information Processing Letters 93(3), 117–123 (2005)
Fernández, M.L.: On proving \(\mathcal{C}\varepsilon\)-termination of rewriting by size-change termination. Information Processing Letters 93(4), 155–162 (2005)
Fernández, M.L., Godoy, G., Rubio, A.: Orderings for innermost termination. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 17–31. Springer, Heidelberg (2005)
Gramlich, B.: On proving termination by innermost termination. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol. 1103, pp. 93–107. Springer, Heidelberg (1996)
Jouannaud, J.P., Rubio, A.: The higher-order recursive path ordering. In: Proc. LICS, pp. 402–411 (1999)
Krishna Rao, M.R.K.: Modular proofs for completeness of hierarchical term rewriting systems. Theoretical Computer Science 151(2), 487–512 (1995)
Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Proc. POPL, pp. 81–92 (2001)
Hirokawa, N., Middeldorp, A.: Dependency Pairs Revisited. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 249–268. Springer, Heidelberg (2004)
Ohlebusch, E.: Hierarchical termination revisited. Information Processing Letters 84(4), 207–214 (2002)
Rubio, A.: Extension Orderings. In: Fülöp, Z., Gecseg, F. (eds.) ICALP 1995. LNCS, vol. 944, pp. 511–522. Springer, Heidelberg (1995)
Thiemann, R., Giesl, J.: Size-change termination for term rewriting. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 264–278. Springer, Heidelberg (2003)
Thiemann, R., Giesl, J., Schneider-Kamp, P.: Improved Modular Termination Proofs Using Dependency Pairs. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 75–90. Springer, Heidelberg (2004)
Toyama, Y.: Counterexamples to termination for the direct sum of term rewriting systems. Information Processing Letters 25, 141–143 (1987)
Urbain, X.: Modular and incremental automated termination proofs. Journal of Automated Reasoning 32, 315–355 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fernández, ML., Godoy, G., Rubio, A. (2005). Recursive Path Orderings Can Also Be Incremental. In: Sutcliffe, G., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2005. Lecture Notes in Computer Science(), vol 3835. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11591191_17
Download citation
DOI: https://doi.org/10.1007/11591191_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-30553-8
Online ISBN: 978-3-540-31650-3
eBook Packages: Computer ScienceComputer Science (R0)