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.
| Original language | English (US) |
|---|---|
| Pages (from-to) | 195-212 |
| Number of pages | 18 |
| Journal | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
| Volume | 8663 |
| DOIs | |
| State | Published - Jan 1 2014 |
Fingerprint
Keywords
- Conditional term rewriting
- Dependency pairs
- Operational termination
- Program analysis
ASJC Scopus subject areas
- Theoretical Computer Science
- Computer Science(all)
Cite this
2D dependency pairs for proving operational termination of CTRSs. / Lucas, Salvador; Meseguer, José.
In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 8663, 01.01.2014, p. 195-212.Research output: Contribution to journal › Article
}
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 -