Extending the 2D Dependency Pair Framework for Conditional Term Rewriting Systems

  • Salvador LucasEmail author
  • José Meseguer
  • Raúl Gutiérrez
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8981)


Recently, a new dependency pair framework for proving operational termination of Conditional Term Rewriting Systems (CTRSs) has been introduced. We call it 2D Dependency Pair (DP) Framework for CTRSs because it makes explicit and exploits the bidimensional nature of the termination behavior of conditional rewriting, where rewriting steps \(s\rightarrow t\) and rewritings \(s\rightarrow ^*t\) (in zero or more steps) are defined for specific terms \(s\) and \(t\) by using an inference system where appropriate proof trees should be exhibited for such particular goals. In this setting, the horizontal component of the termination behavior concerns the existence of infinite sequences of rewriting steps, and the vertical component captures infinitely many climbs during the development of a proof tree for a single rewriting step. In this paper we extend the 2D DP Framework for CTRSs with several powerful processors for proving and disproving operational termination that specifically exploit the structure of conditional rules. We provide the first implementation of the 2D DP Framework as part of the termination tool mu-term. Our benchmarks suggest that, with our new processors, the 2D DP Framework is currently the most powerful technique for proving operational termination of CTRSs.


Conditional rewriting Dependency pairs Operational termination Program analysis 



We thank the referees for their comments and suggestions.


  1. 1.
    Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236(1–2), 133–178 (2000)CrossRefzbMATHMathSciNetGoogle Scholar
  2. 2.
    Alarcón, B., Gutiérrez, R., Lucas, S., Navarro-Marset, R.: Proving termination properties with mu-term. In: Johnson, M., Pavlovic, D. (eds.) AMAST 2010. LNCS, vol. 6486, pp. 201–208. Springer, Heidelberg (2011) CrossRefGoogle Scholar
  3. 3.
    Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. J. Autom. Reasoning 37(3), 155–203 (2006)CrossRefzbMATHMathSciNetGoogle Scholar
  4. 4.
    Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving termination of higher-order functions. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol. 3717, pp. 216–231. Springer, Heidelberg (2005) CrossRefGoogle Scholar
  5. 5.
    Giesl, J., Schneider-Kamp, P., Thiemann, R.: \({\sf {AProVE}}\) 1.2: automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 281–286. Springer, Heidelberg (2006) CrossRefGoogle Scholar
  6. 6.
    Hirokawa, N., Middeldorp, A.: Dependency pairs revisited. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 249–268. Springer, Heidelberg (2004) CrossRefGoogle Scholar
  7. 7.
    Lucas, S., Meseguer, J.: 2D Dependency pairs for proving operational termination of CTRSs. In: Escobar, S. (ed.) WRLA 2014. LNCS, vol. 8663, pp. 195–212. Springer, Heidelberg (2014) CrossRefGoogle Scholar
  8. 8.
    Lucas, S., Marché, C., Meseguer, J.: Operational termination of conditional term rewriting systems. Inf. Process. Lett. 95, 446–453 (2005)CrossRefzbMATHGoogle Scholar
  9. 9.
    Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, Heidelberg (2002) CrossRefzbMATHGoogle Scholar
  10. 10.
    Schernhammer, F., Gramlich, B.: Characterizing and proving operational termination of deterministic conditional term rewriting systems. J. Logic Algebraic Program. 79, 659–688 (2010)CrossRefzbMATHMathSciNetGoogle Scholar
  11. 11.
    Schernhammer, F., Gramlich, B.: VMTL–a modular termination laboratory. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 285–294. Springer, Heidelberg (2009) CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  • Salvador Lucas
    • 1
    • 2
    Email author
  • José Meseguer
    • 1
  • Raúl Gutiérrez
    • 2
  1. 1.CS DepartmentUniversity of Illinois at Urbana-ChampaignChampaignUSA
  2. 2.DSICUniversitat Politècnica de ValènciaValenciaSpain

Personalised recommendations