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)。本文正式描述了一个过程：在给定重写策略的情况下，该过程交错执行模式匹配步骤与重写步骤，从而平滑地集成可归约式发现与子项替换。随后，我们给出了一个高效实现，该实例化该过程为最外层重写，并展示了一些实验的结果。我们的实现在与同类工具的对比中表现出竞争力。