Incremental techniques for efficient normalization of nonlinear rewrite systems

In [8] we described a nonlinear pattern-matching algorithm with the best known worst-case and optimal average-case time complexity. In this paper we first report on some experiments conducted on our algorithm. Based on these experiments we believe that our algorithm is useful in speeding up normalization of nonlinear rewrite systems even when it has a small number (≥5) of rewrite rules. In order to find matches quickly our algorithm operates in two phases. In the first phase it scans the subject tree to collect some “information” which is then used to find matches quickly in the second phase. Scanning can become very expensive especially for large subject trees. However the normalization process is “incremental” in nature. After each reduction step the subject tree is altered and this modified tree is usually not completely different from the old tree. Hence it should be possible to avoid scanning and searching the entire tree for new matches. We describe general techniques to exploit the incremental nature of normalization to speed up each reduction step. Specifically, using these techniques we show that the search for new matches in the subject tree following a replacement can be made independent of the size of the subject tree.