Nonoblivious normalization algorithms for nonlinear rewrite systems

Term rewriting systems provide a very important computational paradigm with widespread applications. The fundamental problem in computing with term rewriting systems is normalization. Consequently, efficient algorithms for finding normal forms of given terms have been the subject of considerable research. However most known normalization algorithms are oblivious, i.e., they do not remember earlier computations and so they are likely to repeat them. In this paper, we present new nonoblivious normalization algorithms for several important classes of confluent rewrite systems. These are the first such algorithms which do not require left-linearity from the rewrite system. We devise and prove certain strong structural properties of reductions in nonlinear systems for justifying the steps in our algorithms. Two interesting consequences of our work are as follows. First, in the absence of overlaps left-linearity can be exchanged with termination for nonoblivious normalization. In analogy, note that for confluence also the same exchange holds in the absence of overlaps. Second, we have devised a new technique for proving certain strong properties of reductions in rewrite systems. This technique appears to be useful for proving other properties also.