Recursive path orderings can be context-sensitive

Abstract

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.