Dependency pairs for proving termination properties of conditional term rewriting systems

Salvador Lucas, José Meseguer

Research output: Contribution to journalArticle

Abstract

The notion of operational termination provides a logic-based definition of termination of computational systems as the absence of infinite inferences in the computational logic describing the operational semantics of the system. For Conditional Term Rewriting Systems we show that operational termination is characterized as the conjunction of two termination properties. One of them is traditionally called termination and corresponds to the absence of infinite sequences of rewriting steps (a horizontal dimension). The other property, that we call V-termination, concerns the absence of infinitely many attempts to launch the subsidiary processes that are required to perform a single rewriting step (a vertical dimension). We introduce appropriate notions of dependency pairs to characterize termination, V-termination, and operational termination of Conditional Term Rewriting Systems. This can be used to obtain a powerful and more expressive framework for proving termination properties of Conditional Term Rewriting Systems.

Original languageEnglish (US)
Pages (from-to)236-268
Number of pages33
JournalJournal of Logical and Algebraic Methods in Programming
Volume86
Issue number1
DOIs
StatePublished - Jan 1 2017

    Fingerprint

Keywords

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Software
  • Logic
  • Computational Theory and Mathematics

Cite this