Context-sensitive rewriting strategies
Author
Salvador Lucas
Abstract
Context-sensitive rewriting is a simple restriction of rewriting which
is formalized by imposing fixed restrictions on replacements. Such a
restriction is given on a purely syntactic basis: it is (explicitly or
automatically) specified on the arguments of symbols of the signature and
inductively extended to arbitrary positions of terms built from those symbols.
Termination 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.
Keywords
infinitary normalization, normalization, replacement restrictions,
root-normalization, strategies, sequentiality, term rewriting.