Loops under Strategies

Most techniques to automatically disprove termination of term rewrite systems search for a loop. Whereas a loop implies nontermination for full rewriting, this is not necessarily the case if one considers rewriting under strategies. Therefore, in this paper we first generalize the notion of a loop to a loop under a given strategy. In a second step we present two novel decision procedures to check whether a given loop is a context-sensitive or an outermost loop. We implemented and successfully evaluated our method in the termination prover TTT2.

• Type: Conference
• Year: 2009
• Where: RTA
• Authors: René Thiemann, Christian Sternagel
• Keywords: Loop, Loop Implies Nontermination, RTA 2009, Term Rewrite Systems, Theoretical Computer Science