Orderings for Innermost Termination

  • Mirtha-Lina Fernández
  • Guillem Godoy
  • Albert Rubio
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3467)


This paper shows that the suitable orderings for proving innermost termination are characterized by the innermost parallel monotonicity, IP-monotonicity for short. This property may lead to several innermost-specific orderings. Here, an IP-monotonic version of the Recursive Path Ordering is presented. This variant can be used (directly or as ingredient of the Dependency Pairs method) for proving innermost termination of non-terminating term rewrite systems.


Normal Form Binary Relation Reduction Ordering Structural Induction Dependency Pair 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science 236(1-2), 133–178 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)Google Scholar
  3. 3.
    Ben-Cherifa, A., Lescanne, P.: Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computer Programming 9, 137–160 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Borralleras, C.: Ordering-based methods for proving termination automatically. PhD thesis, Dpto. LSI, Universitat Politècnica de Catalunya, España (2003)Google Scholar
  5. 5.
    Borralleras, C., Ferreira, M., Rubio, A.: Complete monotonic semantic path orderings. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, Springer, Heidelberg (2000)CrossRefGoogle Scholar
  6. 6.
    Dershowitz, N.: Orderings for term rewriting systems. Theoretical Computer Science 17(3), 279–301 (1982)zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    Fernández, M.L.: Relaxing monotonicity for innermost termination. Information Processing Letters 93(3), 117–123 (2005)zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    Fissore, O., Gnaedig, I., Kirchner, H.: Induction for innermost and outermost ground termination. Technical Report A01-R-178, LORIA, Nancy, France (2001)Google Scholar
  9. 9.
    Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Improving dependency pairs. In: Y. Vardi, M., Voronkov, A. (eds.) LPAR 2003. LNCS, vol. 2850, pp. 165–179. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  10. 10.
    Gramlich, B.: On proving termination by innermost termination. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol. 1103, pp. 93–107. Springer, Heidelberg (1996)Google Scholar
  11. 11.
    Hirokawa, N., Middeldorp, A.: Polynomial interpretations with negative coefficients. In: Buchberger, B., Campbell, J. (eds.) AISC 2004. LNCS (LNAI), vol. 3249, pp. 185–198. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  12. 12.
    Kamin, S., Levy, J.J.: Two generalizations of the recursive path ordering. Dept. of Computer Science, Univ. of Illinois, Urbana, IL (1980)Google Scholar
  13. 13.
    Kusakari, K., Nakamura, M., Toyama, Y.: Argument filtering transformation. In: Nadathur, G. (ed.) PPDP 1999. LNCS, vol. 1702, pp. 47–61. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  14. 14.
    Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Proc. POPL, pp. 81–92 (2001)Google Scholar
  15. 15.
    Lucas, S.: Polynomials for proving termination of context-sensitive rewriting. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 318–332. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  16. 16.
    Manna, Z., Ness, S.: On the termination of Markov algorithms. In: Proc. Int. Conf. on System Science, pp. 789–792 (1970)Google Scholar
  17. 17.
    O’Donnell, M.J.: Computing in Systems Described by Equations. LNCS, vol. 58. Springer, Heidelberg (1977)zbMATHGoogle Scholar
  18. 18.
    Krishna Rao, M.R.K.: Some characteristic of strong innermost normalization. Theoretical Computer Science (239), 141–164 (2000)Google Scholar
  19. 19.
    Steinbach, J., Xi, H.: Freezing - termination proofs for classical, context-sensitive and innermost rewriting. Technical report, Institut für Informatik, T.U. München, Germany (1998)Google Scholar
  20. 20.
    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)CrossRefGoogle Scholar
  21. 21.
    Toyama, Y.: Counterexamples to termination for the direct sum of term rewriting systems. Information Processing Letters 25, 141–143 (1987)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Mirtha-Lina Fernández
    • 1
  • Guillem Godoy
    • 2
  • Albert Rubio
    • 2
  1. 1.Universidad de OrienteSantiago de CubaCuba
  2. 2.Universitat Politècnica de CatalunyaBarcelonaEspaña

Personalised recommendations