Termination of Context-Sensitive Rewriting.pdf

Termination ofcontext-sensitive rewritingH. ZantemaUtrecht University, Department of Computer Science,P.O. box 80.089, 3508 TB Utrecht, The Netherlandse-mail: hansz@cs.ruu.nlAbstractContext-sensitive term rewriting is a kind of term rewriting in whichreduction is not allowed inside some xed arguments of some functionsymbols. We introduce two new techniques for proving termination ofcontext-sensitive rewriting. The rst one is a modication of the tech-nique of interpretation in a well-founded order, the second one is impliedby a transformation in which context-sensitive termination of the origi-nal system can be concluded from termination of the transformed one. Incombination with purely automatic techniques for proving ordinary termi-nation, the latter technique is purely automatic too.1 IntroductionThe function computing the factorial is usually dened as follows:fact(x) = if(x = 0; 1; x  fact(x 1));together with some standard rules like if(true; x; y) = x and if(false; x; y) = y.Considered as a term rewriting system however, the rulefact(x)! if(x = 0; 1; x  fact(x 1))is not terminating. Apparently here general term rewriting does not re ect whatis intended by the denition. In the denition the purpose is that rst the rstargument of if will be reduced to false or true, then the rules if(true; x; y) = xand if(false; x; y) = y will be used to eliminate the if-symbol. In describing thiscomputation process in terms of rewriting, we see that in the intended computa-tion never a redex is reduced inside the second or third argument of an if-symbol.At this point it turns out to be natural to dene a kind of restricted rewritingcorresponding to usual rewriting with the extra restriction that reduction insidethe second or third argument of an if-symbol is not allowed. More general, for1 every symbol we can dene inside which of its arguments reduction is allowed ornot. This kind of rewriting is called context-sensitive rewriting. It is introducedand discussed by Sal