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
$
\mathcal{R}
$
\mathcal{R}
into a (standard) rewrite system
$
\mathcal{R}'
$
\mathcal{R}'
whose termination implies the termination of the CSR system
$
\mathcal{R}
$
\mathcal{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.
C. Borralleras and A. Rubio are supported by the CICYT TIC2001-2476-C03-01, A. Rubio also by the DURSI group 2001SGR 00254
and S. Lucas by CICYT TIC2001-2705-C03-01, Acciones Integradas HI 2000-0161, HA 2001-0059, HU 2001-0019, and Generalitat ValencianaGV01-424.