Context-sensitive rewriting strategies
Context-sensitive rewriting is a simple rewriting restriction which
is formalized by imposing fixed restrictions on replacements. Such a
restriction is given on a purely syntactic basis: it is given
on the arguments of symbols of the signature and
inductively extended to arbitrary positions of terms built from those symbols.
The termination behavior is not only preserved but usually improved
and several methods have been developed to formally prove it.
In this paper, we investigate the definition, properties, and use of
context-sensitive rewriting strategies, i.e., particular, fixed
sequences of context-sensitive rewriting steps. We study how to define
them in order to obtain efficient computations and to
ensure that context-sensitive computations terminate
whenever possible. We give conditions enabling the use of these
strategies for root-normalization, normalization, and infinitary
normalization. We show that this theory is suitable for formalizing the
definition and analysis of real computational strategies which are used in
programming languages such as OBJ or Elan.
infinitary normalization, normalization, replacement restrictions,
root-normalization, sequentiality, strategies, term rewriting.