×

Recursive path orderings can be context-sensitive. (English) Zbl 1072.68537

Voronkov, Andrei (ed.), Automated deduction - CADE-18. 18th international conference, Copenhagen, Denmark, July 27–30, 2002. Proceedings. Berlin: Springer (ISBN 3-540-43931-5). Lect. Notes Comput. Sci. 2392, 314-331 (2002).
Summary: 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}\) into a (standard) rewrite system \({\mathcal R}'\) whose termination implies the termination of the CSR system \({\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.
For the entire collection see [Zbl 0993.00050].

MSC:

68Q42 Grammars and rewriting systems
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite
Full Text: Link