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

Term Rewriting Systems
Termination
Rewriting
Reachability
Sequencing
Two Dimensions
Necessary
Framework

Keywords

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

@article{dde2f380dc0f49b0ba684ef06a3fe68e,
title = "2D dependency pairs for proving operational termination of CTRSs",
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.",
keywords = "Conditional term rewriting, Dependency pairs, Operational termination, Program analysis",
author = "Salvador Lucas and Jos{\'e} Meseguer",
year = "2014",
month = "1",
day = "1",
doi = "10.1007/978-3-319-12904-4_11",
language = "English (US)",
volume = "8663",
pages = "195--212",
journal = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
issn = "0302-9743",
publisher = "Springer Verlag",

}

TY - JOUR

T1 - 2D dependency pairs for proving operational termination of CTRSs

AU - Lucas, Salvador

AU - Meseguer, José

PY - 2014/1/1

Y1 - 2014/1/1

N2 - 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.

AB - 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.

KW - Conditional term rewriting

KW - Dependency pairs

KW - Operational termination

KW - Program analysis

UR - http://www.scopus.com/inward/record.url?scp=84911972406&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84911972406&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-12904-4_11

DO - 10.1007/978-3-319-12904-4_11

M3 - Article

AN - SCOPUS:84911972406

VL - 8663

SP - 195

EP - 212

JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SN - 0302-9743

ER -