Term Rewriting Based On Set Automaton Matching
This work addresses performance improvements in term rewriting systems, which is incremental for the automated reasoning and programming languages communities.
The paper tackled the problem of efficient term rewriting by using a set automaton for subterm pattern matching, resulting in a competitive implementation for outermost rewriting.
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.