Modular Termination of Context-Sensitive Rewriting
Author
Bernhard Gramlich and Salvador Lucas
Abstract
Context-sensitive rewriting (CSR) has recently emerged as an
interesting and flexible paradigm that provides a bridge
between the abstract world of general rewriting and the
(more) applied setting of declarative specification and
programming languages such as OBJ*, CafeOBJ, ELAN, and
Maude. A natural approach to study properties of programs
written in these languages is to model them as context-sensitive
rewriting systems. Here we are especially
interested in proving termination of such systems, and
thereby providing methods to establish termination of e.g.
OBJ* programs. For proving termination of context-sensitive
rewriting, there exist a few transformation methods, that
reduce the problem to termination of a transformed ordinary
term rewriting system (TRS). These transformations, however,
have some serious drawbacks. In particular, most of them do
not seem to support a modular analysis of the termination
problem. In this paper we will show that a substantial part
of the well-known theory of modular term rewriting can be
extended to CSR, via a thorough analysis of the additional
complications arising from context-sensitivity. More
precisely, we will mainly concentrate on termination
(properties). The obtained modularity results correspond
nicely to the fact that in the above languages the modular
design of programs and specifications is explicitly
promoted, since it can now also be complemented by modular
analysis techniques.
Keywords
Context-sensitive rewriting, modular proofs of termination,
declarative programming, evaluation strategies, modular analysis
and construction of programs, program verification.