Extending the 2D dependency pair framework for conditional term rewriting systems

Salvador Lucas, Jose Meseguer, Raúl Gutiérrez

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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 → t and rewritings s →∗ 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.

Original languageEnglish (US)
Title of host publicationLogic-Based Program Synthesis and Transformation - 24th International Symposium, LOPSTR 2014, Revised Selected Papers
EditorsMaurizio Proietti, Hirohisa Seki
PublisherSpringer-Verlag
Pages113-130
Number of pages18
ISBN (Print)9783319178219
DOIs
StatePublished - Jan 1 2015
Event24th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2014 - Canterbury, United Kingdom
Duration: Sep 9 2014Sep 11 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8981
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other24th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2014
CountryUnited Kingdom
CityCanterbury
Period9/9/149/11/14

Keywords

  • Conditional rewriting
  • Dependency pairs
  • Operational termination
  • Program analysis

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Extending the 2D dependency pair framework for conditional term rewriting systems'. Together they form a unique fingerprint.

  • Cite this

    Lucas, S., Meseguer, J., & Gutiérrez, R. (2015). Extending the 2D dependency pair framework for conditional term rewriting systems. In M. Proietti, & H. Seki (Eds.), Logic-Based Program Synthesis and Transformation - 24th International Symposium, LOPSTR 2014, Revised Selected Papers (pp. 113-130). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8981). Springer-Verlag. https://doi.org/10.1007/978-3-319-17822-6_7