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 - 2014 |
Keywords
- Conditional term rewriting
- Dependency pairs
- Operational termination
- Program analysis
ASJC Scopus subject areas
- Theoretical Computer Science
- Computer Science(all)