Derivational Complexity and Context-Sensitive Rewriting

Context-sensitive rewriting is a restriction of rewriting where reduction steps are allowed on specific arguments $$\mu (f)\subseteq \{1,\ldots ,k\}$$ μ ( f ) ⊆ { 1 , … , k } of k-ary function symbols f only. Terms which cannot be further rewritten in this way are called $$\mu $$ μ -normal forms. For left-linear term rewriting systems (TRSs), the so-called normalization via$$\mu $$ μ -normalization procedure provides a systematic way to obtain normal forms by the stepwise computation and combination of intermediate $$\mu $$ μ -normal forms. In this paper, we show how to obtain bounds on the derivational complexity of computations using this procedure by using bounds on the derivational complexity of context-sensitive rewriting. Two main applications are envisaged: Normalization via $$\mu $$ μ -normalization can be used with non-terminating TRSs where the procedure still terminates; on the other hand, it can be used to improve on bounds of derivational complexity of terminating TRSs as it discards many rewritings.