Termination of (Canonical) Context-Sensitive Rewriting
Context-sensitive rewriting (CSR) is a restriction of rewriting which
forbids reductions on selected arguments of functions. A replacement
discriminates, for each symbol of the signature, the argument positions
on which replacements are allowed. If the replacement
restrictions are less restrictive than the expressed by the so called
canonical replacement map, then CSR can be used for computing
(infinite) normal forms of terms. Termination of such canonical CSR
is desirable when using CSR for these purposes.
Existing transformations for proving termination of CSR
fulfill a number of new properties when used for
proving termination of canonical CSR.
(infinitary) normalization, term rewriting, termination.