Recursive Path Orderings can be Context-Sensitive
Cristina Borralleras, Salvador Lucas, and Albert Rubio
Context-sensitive rewriting (CSR) is a simple restriction of rewriting
which can be used e.g. for modelling non-eager evaluation in programming
languages. Many times termination is a crucial property for
program verification. Hence, developing tools for automatically proving
termination of CSR is necessary.
All known methods for proving termination of (CSR) systems are
based on transforming the CSR system R into a (standard) rewrite
system R' whose termination implies the termination of the
CSR system R.
In this paper first several negative results on the applicability of
existing transformation methods are provided. Second, as a
general-purpose way to overcome these problems, we
develop the first (up to our knowledge) method for proving directly
termination of context-sensitive rewrite systems: the context
sensitive recursive path ordering (CSRPO).
Many interesting (realistic) examples that cannot be proved or are
hard to prove with the known transformation methods are easily handled
using CSRPO. Moreover, CSRPO is very suitable for automation.