The computational model of rewriting-based systems consists in reducing
expressions to a canonical form (a head-normal form, (infinite)
normal form or (infinite) value). In order to avoid useless or
dangerous rewrite sequences it is necesary to restrict the
reduction space associated to a given expression. We define a
rewriting restriction, the context-sensitive rewriting (csr), which is
obtained by imposing a particular syntactical replacement
restriction. The replacement restriction is first associated to argument
positions of symbols and then raised to arbitrary occurrences of terms.
The thesis provides a complete analysis of such a simple syntactic replacement
restriction. Our approach differs from the well-known
strictness-based syntactic annotations which need some
underlying reduction strategy which is eventually modified by
taking the annotations into consideration. Instead, csr can be
thought of as a mechanization of syntactic annotations themselves.
We provide methods for proving the termination and the confluence
of csr, we show how to define good context-sensitive rewriting
strategies, and we give methods to automatically define the replacement restrictions
which allow us to compute several classes of
canonical forms. In this way, we believe that our work demonstrates the viability
of csr as an alternative computational mechanism
for rewriting-based systems which usually provides better results.