In this article we investigate how a subterm pattern matching algorithm can be exploited to implement efficient term rewriting procedures. From the left-hand sides of the rewrite system we construct a set automaton, which can be used to find all redexes in a term efficiently. We formally describe a procedure that, given a rewrite strategy, interleaves pattern matching steps and rewriting steps and thus smoothly integrates redex discovery and subterm replacement. We then present an efficient implementation that instantiates this procedure with outermost rewriting, and present the results of some experiments. Our implementation shows to be competitive with comparable tools.

翻译：在本文中，我们研究了如何利用子项模式匹配算法来实现高效的术语重写过程。我们从重写系统的左侧构建了一个集自动机，这可以用于高效地找到术语中的所有redex。我们正式描述了一个程序，它给定重写策略，交替进行模式匹配和重写步骤，从而平滑地整合redex发现和子项替换。然后，我们提出了一个实现这个过程的高效方法，并用最外层重写实例化了它，并呈现了一些实验结果。我们的实现表现出与可比工具相当的竞争力。