The set of irreducible ground terms w. r. t. a term rewriting system R can often be characterized by a finite test set. We describe a fast algorithm to compute such a test set for all left-linear and well-behaved non-left-linear term rewriting systems. Our algorithm uses a new data structure called top set tree which is expanded in a dynamic programming like manner. The tree expansion technique we use to generate the test sets elucidate the connection between the test set approaches and grammatical appraoches to ground reducibility. Our method can also be extended to term rewriting systems modulo AC.
原文链接
分享
引用
