Term Rewriting Based On Set Automaton Matching

TL;DR

This paper introduces a set automaton-based pattern matching algorithm to improve the efficiency of term rewriting, integrating redex discovery and rewriting, with a practical implementation demonstrating competitive performance.

Contribution

It presents a novel set automaton approach for efficient subterm pattern matching in term rewriting systems, including an implementation for outermost rewriting.

Findings

Efficient pattern matching reduces rewriting time.

Implementation is competitive with existing tools.

Experimental results validate the approach's effectiveness.

Abstract

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.