Simple Termination of Context-Sensitive Rewriting
Author
Bernhard Gramlich and Salvador Lucas
Abstract
Simple termination is the (often indirect) basis of most existing automatic
techniques for proving termination of rule-based programs (e.g., Knuth-Bendix,
polynomial, or recursive path orderings, but also DP-simple termination, etc.).
An interesting framework for such programs is context-sensitive rewriting (CSR)
that provides a bridge between the abstract world of general rewriting and the
(more) applied setting of declarative specification and programming languages
(e.g., OBJ*, CafeOBJ, ELAN, and Maude). In these languages, certain replacement
restrictions can be specified in programs by the so-called strategy
annotations. They may significantly improve the computational properties
of programs, especially regarding their termination behaviour.
Context-sensitive rewriting techniques (in particular, the methods for
proving termination of CSR) have been proved useful for analyzing
the properties of these programs. This entails the need to provide implementable
methods for proving termination of CSR.
Simplification orderings (corresponding to the notion of simple
termination) which are well-known in term rewriting (and have nice
properties) are, then, natural candidates for such an attempt.
In this paper we introduce and investigate a corresponding notion of
simple termination of CSR. We prove that our notion actually provides a
unifying framework for proving termination of CSR by using standard
simplification orderings via the existing (transformational) methods, and
also covers CSRPO, a very recent proposal that extends the recursive path
ordering (RPO) (a well-known simplification ordering) to context-sensitive terms.
We also introduce polynomial orderings for dealing with (simple) termination of
CSR. Finally, we also give criteria for the modularity of simple
termination, for the case of disjoint unions as well as for
constructor-sharing rewrite systems.
Keywords
Context-sensitive rewriting, declarative programming,
evaluation strategies, automatic proofs of termination; modular
program analysis and verification.