2D dependency pairs for proving operational termination of CTRSs

Salvador Lucas, José Meseguer

Research output: Contribution to journalArticle

Abstract

The notion of operational termination captures nonterminating computations due to subsidiary processes that are necessary to issue a single ‘main’ step but which often remain ‘hidden’ when the main computation sequence is observed. This highlights two dimensions of nontermination: one for the infinite sequencing of computation steps, and the other that concerns the proof of some single steps. For conditional term rewriting systems (CTRSs), we introduce a new dependency pair framework which exploits the bidimensional nature of conditional rewriting (rewriting steps + satisfaction of the conditions as reachability problems) to obtain a powerful and more expressive framework for proving operational termination of CTRSs.

    Fingerprint

Keywords

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this