# Term Rewriting Based On Set Automaton Matching

arXiv: https://arxiv.org/abs/2202.08687 · HTML: https://mlsanity.com/paper/2202.08687/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 2 of its 34 references that are in the map.
- First posted on arXiv 17 Feb 2022.

## Builds on (most cited first, 2 of 2)

- [The New Rewriting Engine of Dedukti](https://mlsanity.com/paper/2010.16115/) (2020)
- [Adaptive Non-linear Pattern Matching Automata](https://mlsanity.com/paper/2011.13752/) (2020)

## Abstract (arXiv)

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.