Abstract
Restrictions of rewriting may turn normal forms of some terms unreachable,
leading to incomplete computations. Context-sensitive rewriting (csr) is the
restriction of rewriting that only permits reductions on arguments selected by
a replacement map μ, which associates a subset μ(f) of argument indices to
each function symbol f. Hendrix and Meseguer defined an algebraic semantics
for Term Rewriting Systems (TRSs) executing csr that can be used to reason
about programs written in programming languages like CafeOBJ and Maude,
where such replacement restrictions can be specified in programs. Semantic
completeness of csr was also defined. In this paper we show that canonical
replacement maps, which play a prominent role in simulating rewriting computations
with csr, are necessary for completeness in important classes of TRSs.
