Recursive Path Orderings Can Be Context-Sensitive

  • Cristina Borralleras
  • Salvador Lucas
  • Albert Rubio
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2392)


Context-sensitive rewriting (CSR) is a simple restriction of rewriting which can be used e.g. for modelling non-eager evaluation in programming languages. Many times termination is a crucial property for program verification. Hence, developing tools for automatically proving termination of CSR is necessary.

All known methods for proving termination of (CSR) systems are based on transforming the CSR system \( \mathcal{R} \) into a (standard) rewrite system \( \mathcal{R}' \) whose termination implies the termination of the CSR system \( \mathcal{R} \).

In this paper first several negative results on the applicability of existing transformation methods are provided. Second, as a general-purpose way to overcome these problems, we develop the first (up to our knowledge) method for proving directly termination of context-sensitive rewrite systems: the context sensitive recursive path ordering (CSRPO).

Many interesting (realistic) examples that cannot be proved or are hard to prove with the known transformation methods are easily handled using CSRPO. Moreover, CSRPO is very suitable for automation.


Logic Program Transformation Method Function Symbol Termination Proof Label Variable 
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. [AG00]
    T. Arts and J. Giesl. Termination of term rewriting using dependency pairs. Theoretical Computer Science, 236:133–178, 2000.zbMATHCrossRefMathSciNetGoogle Scholar
  2. [AZ96]
    Thomas Arts and Hans Zantema. Termination of logic programs using semantic unification. Fifth International Workshop on Logic Program Synthesis and Transformation, LNCS 1048:219–233. Springer, 1996.Google Scholar
  3. [BN98]
    F. Baader and T. Nipkow. Term Rewriting and all that. Cambridge University Press, 1998.Google Scholar
  4. [BLR02]
    C. Borralleras, S. Lucas and A. Rubio. Recursive Path Orderings can be Context-Sensitive. Available at, 2002. Long version.
  5. [Dau92]
    Max Dauchet. Simulation of turing machines by a regular rewrite rule. Theoretical Computer Science, 103(2):409–420, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  6. [Der82]
    Nachum Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17(3):279–301, 1982.zbMATHCrossRefMathSciNetGoogle Scholar
  7. [FR99]
    M.C.F. Ferreira and A.L. Ribeiro. Context-Sensitive AC-Rewriting. Proc. of 10th International Conference on Rewriting Techniques and Applications, LNCS 1631:286–300, Springer, 1999.Google Scholar
  8. [GM99]
    J. Giesl and A. Middeldorp. Transforming Context-Sensitive Rewrite Systems. Proc. of 10th International Conference on Rewriting Techniques and Applications, LNCS 1631:271–285, Springer, 1999.Google Scholar
  9. [GM01]
    J. Giesl and A. Middeldorp. Transforming Context-Sensitive Rewrite Systems. Proc. of 1th International Workshop on Rewriting Proof and Computation, RPC’01, pages 14–33, RIEC, Tohoku University, 2001.Google Scholar
  10. [Gou01]
    Jean Goubault-Larrecq. Well-Founded Recursive Relations. Proc. 15th Int. Workshop Computer Science Logic, LNCS 2142:484–497, Springer, 2001.CrossRefGoogle Scholar
  11. [GW93]
    Harald Ganzinger and Uwe Waldmann. Termination proofs of well-moded logic programs via conditional rewrite systems. Proc. of 3rd International Workshop on Conditional Term Rewriting Systems, LNCS 656:113–127, Springer, 1993.Google Scholar
  12. [KB70]
    D.E. Knuth and P.B. Bendix. Simple word problems in universal algebras. In Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, 1970.Google Scholar
  13. [KdV02]
    J. Kennaway and F.J. de Vries. Infinitary rewriting. In Term Rewriting Systems. Cambridge University Press, 2002. To appear.Google Scholar
  14. [Luc96]
    S. Lucas. Termination of context-sensitive rewriting by rewriting. Proc. of 23rd. International Colloquium on Automata, Languages and Programming, ICALP’96, LNCS 1099:122–133, Springer, 1996.Google Scholar
  15. [Luc98]
    S. Lucas. Context-sensitive computations in functional and functional logic programs. Journal of Functional and Logic Programming, 1998(1): 1–61, 1998.Google Scholar
  16. [Luc01]
    S. Lucas. Termination of Rewriting With Strategy Annotations. Proc. of 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LNAI 2250:669–684, Springer, 2001.Google Scholar
  17. [NW63]
    C. St. J. A. Nash-Williams. On well-quasi-ordering finite trees. Proceedings of the Cambridge Philosophical Society, 59(4):833–835, 1963.zbMATHCrossRefGoogle Scholar
  18. [SX98]
    J. Steinbach and H. Xi. Freezing — Termination Proofs for Classical, Context-Sensitive and Innermost Rewriting. Institut für Informatik, T.U. München, 1998.Google Scholar
  19. [Zan97]
    H. Zantema. Termination of Context-Sensitive Rewriting. Proc. of 8th International Conference on Rewriting Techniques and Applications, RTA’97, LNCS 1232:172–186, Springer, 1997.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Cristina Borralleras
    • 1
  • Salvador Lucas
    • 2
  • Albert Rubio
    • 3
  1. 1.Dept. Informàtica i MatemàticaE.P.S. Universitat de VicSpain
  2. 2.D.S.I.C.Universidad Politécnica de ValenciaValenciaSpain
  3. 3.Dept. L.S.I.Universitat Politècnica de CatalunyaBarcelonaSpain

Personalised recommendations