Termination of Rewriting With Strategy Annotations

Author

Salvador Lucas

Abstract

We investigate termination of rewriting computations guided by strategy annotations. We show that proofs of termination can be obtained by proving (innermost) termination of context-sensitive rewriting (CSR). Hence, we investigate how to prove innermost termination of CSR using existing methods for proving termination of CSR.

Keywords

Rewriting strategies, termination.