11institutetext: Eindhoven University of Technology
The Netherlands
11email: {m.s.bouwman<EMAIL_ADDRESS>
# Term Rewriting Based on Set Automaton Matching

Mark Bouwman  Rick Erkens

###### 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.

###### Keywords:

Term rewriting Term pattern matching Rewrite engine.

##  1 Introduction

The motivation for this research is to develop a new rewriter for fast state
space generation and model checking in mCRL2 [6]. In this formalism, every
state is associated with a vector of normalized data expressions. Over the
years more complex term rewrite systems have been generated from industrial
domain-specific languages. Typically these contain many complex rules, which
makes an optimized rewrite engine desirable. In our setting, rules may have
arbitrary overlap between left-hand sides, as opposed to functional programs
and orthogonal rewrite systems. Moreover the left-hand sides can be non-linear
(i.e. variables can occur multiple times), and the rewrite strategy is not
fixed.

To allow one to deal with large rewrite systems, implementations of term
rewriting use efficient pattern matching algorithms to find redexes. They
exploit the overlap between the left-hand sides of the rules, and mostly use
efficient _root pattern matching algorithms_ , i.e. techniques that preprocess
the left-hand sides into a data structure that can be used to quickly look for
matches at a specific position in the term. Root pattern matching can be
applied to every position in a term to yield every redex, but this solution is
not efficient in general. Function symbols that are inspected in one call to
the matching algorithm, will be inspected again when the same matching
algorithm is called at a later point from a different root. This means that
symbols will be visited many times, resulting in duplicate work. A
theoretically better solution is to use an algorithm that scans a term for
every pattern at every position simultaneously. Such _subterm pattern matching
algorithms_ exist, but they are generally not used in practical
implementations of term rewriting.

We set out to investigate whether an efficient rewrite engine can be made by
using a subterm pattern matching algorithm. We are not aware of any tools or
methods that explicitly and formally intertwine these two, even though the
idea of using subterm pattern matching for rewriting dates back to the 1980s
[15, 16]. The contribution of this paper is a formal description of a rewrite
procedure that explicitly interleaves rewrite steps with subterm pattern
matching steps, based on the set automaton pattern matching technique
described in [11]. We prove that our procedure correctly implements term
rewriting. Lastly we describe a prototype implementation, and compare its
performance to other rewrite engines by using the benchmark set created by
Garavel et al. in the context of the recurring Rewrite Engine Competition
[14]. Even though it is a prototype, its performance is competitive with the
fastest algebraic rewriters.

The set automaton matching algorithm generalizes the Aho-Corasick string
matching algorithm [1] to sets of term patterns. The main advantage of set
automata is that they inspect every symbol of a term only once by traversing
the term from top to bottom. Even though our rewrite procedure is based on
this algorithm, it does not call the pattern matching function as a complex
subroutine. It rather interleaves automaton-guided pattern matching steps
(single function symbol observations) and rewrite steps, and saves the
matching information in a data structure called a _configuration tree_. Based
on the available matching information, a strategy decides to continue
searching for redexes (and where) or to rewrite using a previously found redex
(and which one). This method allows us to preserve a part of the matching work
when we apply a rewrite step.

###  1.1 Related work

The idea to use subterm matching for term rewriting and equational reasoning
dates back to Hoffmann and O’Donnell [15, 16]. In [28] some algorithms are
described based on their ideas. Huet and Lévy use matching dags for orthogonal
rewrite systems in [18]. Fokkink et al. transform left-linear rewrite systems
into so-called minimal rewrite systems with only shallow patterns and right-
hand sides [13]. The transformation on the right-hand sides of the rules is
based on one of Hoffmann and O’Donnell’s algorithms [16].

Current state-of-the-art rewrite engines use efficient root pattern matching
techniques. Maude, the fastest rewrite engine among the algebraic tools of the
latest edition of the Rewrite Engine Competition [14], deploys automaton-based
solutions to several kinds of pattern matching problems [8]. In particular it
uses discrimination nets [7] for matching linear patterns. Dedukti uses
decision trees [17] to deal with non-linearity and higher-order pattern
matching. The compiling rewriter of mCRL2 uses match trees [27] that compute
subtitutions on the fly as well. An overview of root pattern matching
techniques is given in [23].

In functional languages like Haskell [19] and Clean [4] algebraic data types
are specified with constructor function symbols that cannot be the head symbol
of any rewrite rules. In combination with other language choices, such as
priorities between patterns, this ensures that pattern matching is easier than
in general term rewriting. Since our target language is algebraic, we make no
distinction between constructors and function-defining symbols, and impose no
restrictions like orthogonality.

For term rewriting, a deterministic top-down solution to subterm matching is
desirable, so we opted to use set automata for our procedures. The other
deterministic top-down algorithms in [9, 16] are reductions to string
matching: they collect stringpath matches during the matching operation which
must be merged while rewriting. Set automata do not suffer this administrative
overhead and output the term matches themselves while matching. The drawback
of set automata however, is that they require a look-ahead of at most the
largest depth of any left-hand side. This look-ahead is necessary since top-
down deterministic tree automata are not powerful enough to perform any
pattern matching [10]. In some cases this look-ahead can be mitigated, but a
general solution to use set automata for linear time matching is an open
problem.

###  1.2 Structure of the paper

In Section 2 we present some preliminary definitions. In Section 3 we recall
the set automaton matching technique from [11]. A set automaton can be
executed to find all redexes in a term, by storing intermediate configurations
in a _set_. For the rewriting procedures that we introduce, it is important to
save the matching information in a more structured way than a set. To this
end, we introduce _configuration trees_ , where the configurations that would
previously be stored in a set, appear at the leaves of the tree.

To further aid the reader in understanding set automata, we recall in detail
how a set automaton is constructed from a set of patterns in Section 4. This
section is largely copied from [11].

In Section 5 we formally describe a rewrite procedure that takes an arbitrary
strategy, and searches for redexes while maintaining a configuration tree.
When a rewrite step is performed, a part of the information in the
configuration tree is saved. We show that the rewrite procedure correctly
implements term rewriting, regardless of the strategy.

Since set automata can only deal with linear patterns, we define a rewrite
procedure that supports non-linear rewrite systems in Section 6. A slight
adaptation to the set automaton construction that requires non-linear patterns
to be yielded in a separate set, suffices to support these rewrite systems,
albeit in a (arguably necessarily) non-optimal way.

To bridge the gap between formal presentation and practice we discuss an
efficient implementation of our rewrite procedure in Section 7. Specifically
it uses an outmost rewrite strategy and uses a stack to store the
configuration tree. We also present some benchmarks and extensively compare
the results to those of some other rewrite engines.

Lastly in Section 8 we present some concluding remarks and some ideas for
further improvements of the technique that we intend to explore in the future.

##  2 Preliminaries

We recall some preliminaries, found in e.g. [2]. A _ranked alphabet_ is a
finite set of function symbols $\mathbb{F}$ paired with an arity mapping
$\\#:\mathbb{F}\to\mathbb{N}$. The set of _terms over $\mathbb{F}$ with
variables in $\mathbb{V}$_ is denoted by $\mathbb{T}(\mathbb{F},\mathbb{V})$.
The set of variables of $t$ is given by $\mathsf{vars}(t)$. A ground term is a
term without variables.

A _position_ is a list of positive integers. We use $\mathbb{P}$ to denote the
set of all positions and we use $\epsilon$ to denote the empty list, also
referred to as the _root position_. The concatenation of two positions $p$ and
$q$ is denoted by $p.q$. The root position acts as a unit element with respect
to concatenation. Given a set $X$ we often denote a pair $(x,p)$ in
$X\times\mathbb{P}$ by $x@p$. The _term domain function_
$\mathcal{D}:\mathbb{T}(\mathbb{F},\mathbb{V})\to\mathcal{P}(\mathbb{P})$ maps
a term to the set of positions on which it has function symbols or variables,
for example $\mathcal{D}(f(g(a),b))=\\{\epsilon,1,1.1,2\\}$. Similarly the
_edge function_
$\mathcal{E}:\mathbb{T}(\mathbb{F},\mathbb{V})\to\mathcal{P}(\mathbb{P})$ maps
a term $t$ to the subset of $\mathcal{D}(t)$ where $t$ has variables. Define
$\mathcal{D}_{\setminus\mathcal{E}}(t)=\mathcal{D}(t)\setminus\mathcal{E}(t)$.
Given a term $t$ and a position $p\in\mathcal{D}(t)$, the subterm of $t$ at
position $p$ is denoted by $t|_{p}$. Replacing the subterm of $t$ at position
$p$ by $u$ is denoted by $t[u]_{p}$. A _pattern_ is a term, but not a
variable. Said pattern is _linear_ if no variable occurs more than once in
$\ell$. Denote the _head symbol_ of a pattern $\ell$ by $\mathsf{hd}(\ell)$.

A _substitution_ is a mapping
$\sigma:\mathbb{V}\to\mathbb{T}(\mathbb{F},\mathbb{V})$; the term obtained by
replacing all variables $x\in\mathsf{vars}(t)$ by $\sigma(x)$ is denoted by
$t^{\sigma}$. Term $t$ _matches_ pattern $\ell$ iff $t=\ell^{\sigma}$ for some
$\sigma$. A _rewrite rule_ is a pattern $\ell$ paired with a term $r$, denoted
$\ell\to r$, such that all variables of $r$ occur in $\ell$ as well. A _term
rewrite system (TRS)_ is a finite, non-empty set of rewrite rules. A _redex of
$t$_ is a rule $\ell\to r$ and a position $p$ such that $t|_{p}$ matches
$\ell$. Such a redex is often denoted by $(\ell\to r)@p$.

Let $t$ be a term with redex $(\ell\to r)@p$. Then $t$ rewrites to
$t^{\prime}$, denoted by $t\xrightarrow{(\ell\to r)@p}t^{\prime}$, iff there
is a term $u$ with $p\in\mathcal{D}(u)$ such that $t=u[\ell^{\sigma}]_{p}$ and
$t^{\prime}=u[r^{\sigma}]_{p}$. We write $t\xrightarrow{}t^{\prime}$ if $t$
rewrites to $t^{\prime}$ by some rule on some position. The transitive
reflexive closure of $\xrightarrow{}$ is denoted by $\xrightarrow{}^{*}$. A
term $t$ is in _normal form_ iff $t$ has no redexes. Given a rule $\ell\to r$
and a term $t$ such that $\ell$ matches $t$ at position $p$, we denote by
$t[(\ell\to r)@p]$ the unique term $t^{\prime}$ such that
$t\xrightarrow{(\ell\to r)@p}t^{\prime}$.

##  3 Set automata

Since set automata form the foundation for the rewrite procedures, we recall
them in detail from [11]. First we recall their formal definition. Then we
give two methods to execute them on terms. In the next section we recall the
set automaton construction algorithm.

Set automata generalize Aho and Corasick’s string matching automata [1] to
terms. They prescribe how to search for patterns in a term in a top-down
fashion and allow us to match all patterns in every subterm simultaneously. To
find all matches, we have to inspect every symbol of a term only once, modulo
some look-ahead.

Let $\mathcal{R}$ be a TRS with $\mathcal{L}=\\{\ell\mid\ell\to
r\in\mathcal{R}\\}$ being its set of left-hand sides. A set automaton for
$\mathcal{L}$ over the alphabet $\mathbb{F}$ is a tuple
$(S,s_{0},L,\delta,\eta)$ where

  * •

$S$ is a finite set of _states_ ;

  * •

$s_{0}\in S$ is the _initial state_ ;

  * •

$L:S\to\mathbb{P}$ is a _state labelling function_ ;

  * •

$\delta:S\times\mathbb{F}\to\mathcal{P}(S\times\mathbb{P})$ is a _transition
function_ ;

  * •

$\eta:S\times\mathbb{F}\to\mathcal{P}(\mathcal{L}\times\mathbb{P})$ is an
_output function_.

Figure 1: A set automaton for $\ell=+(+(x,s(y)),s(z))$.

Consider the pattern $\ell=+(+(x,s(y)),s(z))$. In Fig. 1 the set automaton for
the singleton pattern set $\\{\ell\\}$ is graphically displayed. The lines of
the form $x\hookrightarrow y$ in the boxes are important in the next section
where we discuss the construction, but for now they can be ignored. The states
are named $s_{0},\dots,s_{3}$, displayed on the top right corner. The state
labels are given on the top left corner; they provide information on what
position to inspect next. The drawn hypertransitions are a combination of the
transition function and the output function, e.g. the $s$-labelled transition
from state $s_{3}$ is captured by
$\delta(s_{3},s)=\\{(s_{0},1.2.1),(s_{2},1)\\}$ and
$\eta(s_{3},s)=(\ell,\epsilon)$.

Note that the transition and output functions are total: for every state and
symbol combination there is a transition. Though for some transitions there
may not be target states: e.g. $\delta(s_{0},0)=\emptyset$. Intuitively,
matching goes as follows. We start in the initial state and with the root
position: the _configuration_ $(s_{0},\epsilon)$. The state label instructs us
what position to inspect relative to the position in the configuration. With
the inspected symbol we select the corresponding transition. If the transition
has an output then we found a match. We follow the transition function,
yielding new states to visit (possibly multiple, possibly none). If the
transition specifies a non-root position then the position in the
configuration is deepened. For example, suppose we want to match on the term
$s(0)$. Then we start with the initial configuration $(s_{0},\epsilon)$. We
inspect $\mathsf{hd}(s(0)|_{\epsilon.\epsilon})=s$ and take the selfloop
transition, yielding the configuration $(s_{0},1)$. We now inspect
$\mathsf{hd}(s(0)|_{1.\epsilon})=0$, and take the corresponding transition.
This does not lead to new configurations, hence matching is finished.

Let us formalize this matching procedure. To find redexes in a ground term
$t$, we traverse it by using the set automaton. To this end, a set of
configurations111Hence the name _set_ automaton \- pairs $(s,p)$ consisting of
a state $s$ in the set automaton and a position $p$ in the term - needs to be
maintained. From a configuration $(s,p)$ we observe the function symbol of
term $t$ on position $p.L(s)$: $\mathsf{hd}(t|_{p.L(s)})$. Then we compute the
successor configurations and the output as follows.

  * •

For all successors $(s^{\prime},q)\in\delta(s,f)$ obtained from configuration
$(s,p)$ we add a new configuration $(s^{\prime},p.q)$ to the configuration
set.

  * •

When $(\ell,q)\in\eta(s,f)$ is given as output from configuration $(s,p)$ then
there is a match for $\ell$ at position $p.q$. In all of our examples the
position $q$ is just $\epsilon$, but when a pattern is a proper subpattern of
another, then $q$ may be deeper.

The set of all redexes of a ground term $t$ is retrieved by
$\mathsf{eval}(s_{0},\epsilon,t)$ where

$\mathsf{eval}(s,p,t)=\\{(\ell,p.q)\mid(\ell,q)\in\eta(s,f)\\}\cup\bigcup_{(s^{\prime},p^{\prime})\in\delta(s,f)}\mathsf{eval}(s^{\prime},p.p^{\prime},t|_{p^{\prime}})$

where $f=\mathsf{hd}(t|_{L(s)})$.

###### Example 1

For a more elaborate example let us consider the ground term
$t=+(+(+(0,s(0)),s(0)),s(0))$. The table below shows how the set automaton is
used to find all matches in $t$ (whilst inspecting every symbol once).

Configuration set | Configuration |  Observed
position |  Observed
symbol | Output
---|---|---|---|---
$(s_{0},\epsilon)$ | $(s_{0},\epsilon)$ |  $\epsilon$ |  $+$ |
$(s_{1},\epsilon)$ | $(s_{1},\epsilon)$ |  $2$ |  $s$ |
$(s_{2},\epsilon)$, $(s_{0},2.1)$ | $(s_{2},\epsilon)$ |  $1$ |  $+$ |
$(s_{0},2.1)$, $(s_{3},\epsilon)$ | $(s_{0},2.1)$ |  $2.1$ |  $0$ |
$(s_{3},\epsilon)$ | $(s_{3},\epsilon)$ |  $1.2$ |  $s$ | $\ell@\epsilon$
$(s_{0},1.2.1)$, $(s_{2},1)$ | $(s_{0},1.2.1)$ |  $1.2.1$ |  $0$ |
$(s_{2},1)$ | $(s_{2},1)$ |  $1.1$ |  $+$ |
$(s_{3},1)$ | $(s_{3},1)$ |  $1.1.2$ |  $s$ | $\ell@1$
$(s_{0},1.1.2.1)$, $(s_{2},1.1)$ | $(s_{0},1.1.2.1)$ |  $1.1.2.1$ |  $0$ |
$(s_{2},1.1)$ | $(s_{2},1.1)$ |  $1.1.1$ |  $0$ |

###  3.1 Configuration trees

Instead of storing configurations in a set we can also represent the
discovered configurations in a tree structure with $(s_{0},\epsilon)$ as root.
Originally this structure was used in the correctness proof of set automata,
but it has appeared to be very useful for rewriting, as we can now also reason
about partially completed configuration trees. An unexplored configuration
appears as a $\mathsf{B}$-labelled pair $\mathsf{B}(s,p)$, a childless vertex
in the tree which we refer to as a _bud_. Upon observing a function symbol in
the subject term, this bud is ‘grown’ into an $\mathsf{N}$-labelled triple
$\mathsf{N}(s,p,cts)$ called a _node_. The component $cts$ of a node is a
possibly empty set of successor trees; when the node is created by growing a
bud, it consists of buds, one for every successor state given by
$\delta(s,f)$. If there are no successor states given by $\delta(s,f)$ then
$cts$ is empty. Hence the trees $\mathsf{B}(s,p)$ and
$\mathsf{N}(s,p,\emptyset)$ differ in the sense that the bud indicates an
unexplored configuration and the node indicates an explored configuration with
no successors. Formally the set of _configuration trees_
$\mathcal{C}\mathcal{T}$ is formed by the grammar
$\mathcal{C}\mathcal{T}::=\mathsf{B}(s,p)\mid\mathsf{N}(s,p,cts)$ where $cts$
is a finite, possibly empty set of configuration trees. Define the set of
$\mathsf{B}$/$\mathsf{N}$-labelled configurations of $ct$ by
$\mathsf{buds}(ct)$ and $\mathsf{nodes}(ct)$ respectively. The set of all
configurations is given by $\mathsf{confs}(ct)$. The _completed configuration
tree_ for term $t$ is defined by $\mathsf{completed}(s_{0},\epsilon,t)$ where

$\mathsf{completed}(s,p,t)=\mathsf{N}(s,p,\\{\mathsf{completed}(s^{\prime},p.p^{\prime},t)\mid(s^{\prime},p^{\prime})\in\delta(s,\mathsf{hd}(t|_{p.L(s)}))\\})\,.$

###### Example 2

The configuration tree in Fig. 2 is associated to line 5 of the table in
Example 1. Note that the configuration tree does not have the same shape as
$t$.

Figure 2: The term $t=+(+(+(0,s(0)),s(0)),s(0))$ and a partial configuration
tree.

Define the abbreviation
$\mathsf{completed}(t)=\mathsf{completed}(s_{0},\epsilon,t)$. A completed
configuration tree is a one-to-one correspondence between configurations and
the function symbols of a term, assigned to it by a set automaton.

###### Theorem 3.1

Let $M=(S,s_{0},L,\delta,\eta)$ be a set automaton generated from the TRS
$\mathcal{R}$. Then $\mathsf{N}(s,p,cts)\mapsto p.L(s)$ is a bijection from
the subtrees of $\mathsf{completed}(t)$ to $\mathcal{D}(t)$.

This correspondence suffices to find every redex in a term as follows. In a
configuration $(s,p)$ the symbol $f=\mathsf{hd}(t|_{p.L(s)})$ yields some
matches as prescribed by $\eta(s,f)$. Define the discovered matches of a
configuration $(s,p)$ and $t$ by

$\mathsf{matches}(s,p,t)=\\{(\ell@p.q)\mid(\ell,q)\in\eta(s,\mathsf{hd}(t|_{p.L(s)}))\\}\,.$

The following theorem states the correctness claim for pattern matching.

###### Theorem 3.2

For every ground term $t$, the set of all redexes of $t$ is given by
$\bigcup\\{\mathsf{matches}(s,p,t)\mid(s,p)\in\mathsf{nodes}(\mathsf{completed}(t))\\}$.

##  4 Construction of a set automaton

We recall from [11] how a set automaton is constructed from a pattern set. The
examples and the explanation overlap largely with the original work. To
understand the rewrite procedures it is not necessary to understand the
construction.

We create the states and the transition function on the fly. To this end we
first give a state encoding that represents its information in the pattern
matching process. The informal explanation follows the formal one.

The _subpatterns of a pattern $\ell$_ are given by
$\mathsf{sub}(\ell)=\\{\ell|_{p}\mid
p\in\mathcal{D}_{\setminus\mathcal{E}}(\ell)\\}$. This function is extended to
sets of patterns $\mathcal{L}$ by
$\mathsf{sub}(\mathcal{L})=\bigcup_{\ell\in\mathcal{L}}\mathsf{sub}(\ell)$.
The sets of _match obligations_ $\mathit{MO}$ and _match announcements_
$\mathit{MA}$ are defined by

$\mathit{MO}=\mathcal{P}(\mathsf{sub}(\mathcal{L})\times\mathbb{P})\setminus\\{\emptyset\\}\qquad\mathit{MA}=\mathcal{L}\times\mathbb{P}\,.$

A _match goal_ is a match obligation paired with a match announcement, i.e. a
pair in $\mathit{MO}\times\mathit{MA}$. To limit the amount of parentheses, we
denote a match goal $(\\{(\ell_{1},p_{1}),\dots,(\ell_{n},p_{n})\\},(\ell@p))$
by $\ell_{1}@p_{1},\dots,\ell_{n}@p_{n}\hookrightarrow\ell@p$. Such a match
goal should be read as: “in order to announce a match for pattern $\ell$ at
position $p$, it remains to observe the (sub)pattern $\ell_{i}$ on position
$p_{i}$, for all $1\leq i\leq n$”. We identify states with non-empty sets of
match goals, i.e.
$S=\mathcal{P}(\mathit{MO}\times\mathit{MA})\setminus\\{\emptyset\\}$. This
encoding formally captures the idea that a state carries every pattern that
still needs to be seen whenever we arrive in this state in the matching
process.

Recall the set automaton from Fig. 1. The initial state $s_{0}$ has one match
goal, namely
$+(+(x,s(y)),s(z))@\epsilon\hookrightarrow+(+(x,s(y)),s(z))@\epsilon$. The
match announcement of this goal is abbreviated to $\ell@\epsilon$ in the
figure. Intuitively, whenever we are matching from $s_{0}$, we still need to
observe every pattern from the root.

State $s_{1}$ can be reached by following the $+$-transition from the initial
state, and it has three match goals. The first goal
$+(x,s(y))@1,s(z)@2\hookrightarrow\ell@\epsilon$ is obtained by reducing the
match obligation of $s_{0}$ to $+(x,s(y))@1,s(z)@2$. The top symbol $+$ has
already been inspected; therefore the subpatterns $+(x,s(y))$ and $s(z)$
should still be observed at their respective positions in order to yield a
pattern match for $\ell$ at the root position. Furthermore there are the goals
$+(+(x,s(y)),s(z))@1\hookrightarrow+(+(x,s(y)),s(z))@1$, and
$+(+(x,s(y)),s(z))@2\hookrightarrow+(+(x,s(y)),s(z))@2$. These are considered
_fresh_ goals on a lower position. Since the purpose of a set automaton is to
yield all pattern matches at every position, these fresh goals are added
throughout the construction.

We give two kinds of match goals a special status. A match goal of the form
$\ell@p\hookrightarrow\ell@p$ is called _fresh_. It represents that we aim to
find a pattern match for $\ell$ on position $p$, but we have not observed any
function symbols of that pattern yet. A match goal of the form
$mo\hookrightarrow\ell@\epsilon$ is called a _root goal_.

###  4.1 Initial state

Consider a non-empty pattern set $\mathcal{L}$. We start the construction of a
set automaton for $\mathcal{L}$ from the initial state, and compute the
transition function and the other states on the fly. From the initial state
all patterns still need to be observed from the root position. In terms of the
state encoding, the initial state is formally defined by
$s_{0}=\\{\ell@\epsilon\hookrightarrow\ell@\epsilon\mid\ell\in\mathcal{L}\\}$.
In other words, the initial state contains every fresh root goal.

###  4.2 State labels

For every state $s$ there must be a position label $L(s)$ in order to
construct the transitions from $s$. It can be chosen from the match obligation
positions, and we demand the extra constraint that this position should be
part of a root match goal. The construction guarantees that every state has a
root goal, which is shown in [11]. Similar to Adaptive Pattern Matching
Automata [24], there might be multiple positions available to choose from. Any
of such positions can be chosen in the construction of the automaton, but this
position needs to be fixed when $s$ is created. For example, the initial state
only has root goals, so it is labelled with the empty position, formally
$L(s_{0})=\epsilon$.

###  4.3 Transitions

From a state $s$ we define $\delta(s,f)$ for every function symbol $f$ in
three steps. First, we compute the so-called $f$-derivative of $s$. This
covers the semantics of subterm pattern matching completely. That is, by only
taking derivatives we obtain a correct matching automaton. However, this
automaton will be infinite since the derivative operation adds more match
goals with longer positions.

To mitigate this problem we perform two more steps after computing the
derivative. To counteract the growing amount of match goals, we partition them
into independent equivalence classes. In Fig. 1 this appears as an arrow going
out of a black dot for every equivalence class. To counteract the growing
positions we maximally shorten all positions in every equivalence class. In
Fig. 1 the positions on the arrows going out of the black dots, indicate which
part of the positions was removed. The shortened equivalence classes of the
derivative are then new states, from which the process of constructing the
automaton proceeds. Eventually one only encounters states that have already
been processed.

####  4.3.1 Derivatives.

To capture the semantics of subterm pattern matching we introduce
$f$-derivatives of states. This terminology is borrowed from Brzozowski
derivatives of regular expressions [5]. Given a state $s$ with state label
$L(s)=p$, and a symbol $f$, we determine $f$-derivative of $s$ in three steps.
Firstly, we look at the match goals of $s$ which have a match obligation with
position $p$. These obligations should be _reduced_. Secondly, we take all
match goals of $s$ which do not have a match obligation with position $p$.
These goals remain _unchanged_. Thirdly, we add _fresh goals_ for every
pattern and every $i$ with $1\leq i\leq\\#f$.

Consider a match goal
$\ell_{1}@p_{1},\dots,\ell_{n}@p_{n}\hookrightarrow\ell@p$, and suppose that
we need to reduce this goal modulo position $p_{i}$ with function symbol $f$.
There are three cases that need to be considered.

  * •

If $i=1$, $n=1$ and $\ell_{1}=f(x_{1},\dots,x_{n})$ for variables
$x_{1},\dots,x_{n}$ then $f@p_{i}$ is the last observation needed to complete
the match goal. Then $\ell@p$ is recorded in the output function of the
automaton and the match goal disappears.

  * •

If $\mathsf{hd}(\ell_{i})\neq f$, the observation $f@p_{i}$ leads to the
conclusion that this pattern cannot match. Then the match obligation is
discarded.

  * •

Otherwise $\ell_{i}=f(t_{1},\dots,t_{\\#f})$ but the match goal is not
completed yet. Then the other pairs $\ell_{j}@p_{j}$ with $i\neq j$ remain
unchanged, the pair $\ell_{i}@p_{i}$ is removed from the obligation and for
all $j$ such that $t_{j}\notin\mathbb{V}$ we add the pair<EMAIL_ADDRESS>to
the obligation of this goal.

Let $\mathsf{pos}(mo)$ be the set of positions in a match obligation $mo$.
Formally, reducing a match obligation is captured by
$\mathsf{reduce}:\mathit{MO}\times\mathbb{F}\times\mathbb{P}\to\mathit{MO}\cup\\{\emptyset\\}$
defined by:

$\displaystyle\mathsf{reduce}(mo,f,p)=\,$ $\displaystyle\\{\ell@q\in mo\mid
q\neq p\\}\ \cup$ $\displaystyle\\{\ell|_{i}@p.i\mid\ell@p\in mo\wedge 1\leq
i\leq\\#f\wedge\ell|_{i}\notin\mathbb{V}\\}\,.$

Using the mapping $\mathsf{reduce}$, define the $f$-derivative of state $s$ by

$\displaystyle\mathsf{deriv}(s,f)$
$\displaystyle=\mathit{reduced}\cup\mathit{unchanged}\cup\mathit{fresh}\,,\text{where}$
$\displaystyle\mathit{reduced}$
$\displaystyle=\\{\mathsf{reduce}(mo,f,L(s))\hookrightarrow ma\mid mo\to ma\in
s\ \wedge$ $\displaystyle\hskip 56.9055pt\exists\ell:\ell@L(s)\in
mo\wedge\mathsf{hd}(\ell)=f\wedge\mathsf{reduce}(mo,f,L(s))\neq\emptyset\\}$
$\displaystyle\mathit{unchanged}$ $\displaystyle=\\{mo\hookrightarrow ma\in
s\mid L(s)\notin\mathsf{pos}(mo)\\}$ $\displaystyle\mathit{fresh}$
$\displaystyle=\\{\ell@L(s).i\hookrightarrow\ell@L(s).i\mid\ell\in\mathcal{L}\wedge
1\leq i\leq\\#f\\}\,.$

###### Example 3

Consider state $s_{1}$ of the set automaton in Fig. 1. The parts of
$\mathsf{deriv}(s_{1},s)$ are computed as follows:

$\displaystyle\mathit{unchanged}$
$\displaystyle=\\{+(+(x,s(y)),s(z))@1\hookrightarrow\ell@1\\}$
$\displaystyle\mathit{reduced}$
$\displaystyle=\\{+(x,s(y))@1\hookrightarrow\ell@\epsilon\\}$
$\displaystyle\mathit{fresh}$
$\displaystyle=\\{+(+(x,s(y)),s(z))@2.1\hookrightarrow\ell@2.1\\}\,.$

Note that the goal $+(+(x,s(y)),s(z))@2\hookrightarrow\ell@2$ disappears
completely since the expected symbol $+$ mismatches with the considered symbol
$s$ at position $2$.

####  4.3.2 Derivative partitioning.

One application of $\mathsf{deriv}$ creates new match goals with longer
positions. Repeated application of $\mathsf{deriv}$ therefore results in an
automaton with an infinite amount of states. We first mitigate the issue of
new match goals by partitioning the computed derivative with respect to a
dependency relation on match goals.

Note from Example 3 that the derivative has two match obligations at position
$1$, and one match obligation at position $2.1$. To obtain an efficient
matching algorithm, it is important that goals with overlapping positions end
up in the same equivalence class. When observing a function symbol at this
relative position $1$, both goals should be reduced simultaneously.
Conversely, sets of goals that are independent from each other can be
separated to form a new state with fewer match goals. When evaluating a set
automaton this creates the possibility of exploring parts of the subject term
independently. Given a state $s$, define the _direct dependency relation_
$R_{dep}$ for all goals $g_{1}=mo_{1}\hookrightarrow\ell_{1}@p_{1}$ and
$g_{2}=mo_{2}\hookrightarrow\ell_{2}@p_{2}$ by $g_{1}\mathrel{R_{dep}}g_{2}$
if, and only if, $\mathsf{pos}(mo_{1})\cap\mathsf{pos}(mo_{2})\neq\emptyset$.
Note that $R_{dep}$ is reflexive, since match obligations cannot be empty, and
$R_{dep}$ is also symmetric. But $R_{dep}$ is not transitive, since for the
obligations $mo_{1}=\\{t_{1}@1\\}$,$mo_{2}=\\{t_{1}@1,t_{2}@2\\}$ and
$mo_{3}=\\{t_{2}@2\\}$ we have
$\mathsf{pos}(mo_{1})\cap\mathsf{pos}(mo_{2})=\\{1\\}$ and
$\mathsf{pos}(mo_{2})\cap\mathsf{pos}(mo_{3})=\\{2\\}$, but
$\mathsf{pos}(mo_{1})\cap\mathsf{pos}(mo_{3})=\emptyset$. To obtain an
equivalence we simply take the transitive closure ${\sim}=R_{dep}^{*}$, which
we refer to as (indirect) dependency.

We partition $\mathsf{deriv}(s,f)$ with respect to $\sim$. Each equivalence
class then corresponds to a new state. The set of equivalence classes of the
derivative is denoted by $[\mathsf{deriv}(s,f)]_{\sim}$. We use $K$ to range
over equivalence classes.

###### Example 4

Consider the $s$-derivative of Example 3. Partitioning yields

$\displaystyle K_{1}$
$\displaystyle=\\{+(+(x,s(y)),s(z))@1\hookrightarrow\ell@1,\quad+(x,s(y))@1\hookrightarrow\ell@\epsilon\\}$
$\displaystyle K_{2}$
$\displaystyle=\\{+(+(x,s(y)),s(z<EMAIL_ADDRESS>
###### Example 5

Consider the $+$-derivative of $s_{2}$, which is exactly $s_{3}$. Note that
the goals $s(y)@1.2\hookrightarrow\ell@\epsilon$ and
$+(+(x,s(y)),s(z<EMAIL_ADDRESS>are not directly dependent, but
the goal $+(x,s(y))@1.1,s(z)@1.2\hookrightarrow\ell@1$ is directly dependent
to both goals. Therefore we obtain a singleton partition.

####  4.3.3 Lifting the positions of classes.

After partitioning, we shorten the positions of every equivalence class to
mitigate the problem of growing positions. Let $\mathsf{pos}_{\mathit{MA}}(K)$
denote the positions of the match announcements of $K$. We want to ‘lift’
every position in every goal of $K$ by the greatest common prefix of
$\mathsf{pos}_{\mathit{MA}}(K)$. To ease the notation we write
$\mathsf{gcp}(K)$ instead of $\mathsf{gcp}(\mathsf{pos}_{\mathit{MA}}(K))$.
Since all positions in a state are of the form $\mathsf{gcp}(K).p^{\prime}$,
we can replace them by $p^{\prime}$. Define $\mathsf{lift}(s)$ by
$\mathsf{lift}(s)=\\{(\mathsf{lift}(mo),\ell@p^{\prime})\mid(mo,\ell@\mathsf{gcp}(s).p^{\prime})\in
s\\}$ where
$\mathsf{lift}(mo)=\\{\ell@p^{\prime}\mid\ell@\mathsf{gcp}(s).p^{\prime}\in
mo\\}$.

For a state $s$ and a function symbol $f$, we fix
$\delta(s,f)=\\{(\mathsf{lift}(K),\mathsf{gcp}(K))\mid
K\in[\mathsf{deriv}(s,f)]_{\sim}\\}$. Note that $\mathsf{gcp}(K)$ is also
recorded in each transition since it tells us how to traverse the term.

###### Example 6

Continuing in Example 4, we compute the greatest common prefix and
corresponding transition for the two equivalence classes. For $K_{1}$ we have
$\mathsf{gcp}(K_{1})=\mathsf{gcp}(\\{1,\epsilon\\})=\epsilon$. Then
$\mathsf{lift}(K_{1})=K_{1}=s_{2}$, and therefore
$(s_{2},\epsilon)\in\delta(s_{1},s)$. Class $K_{2}$ has one goal with
$\mathsf{gcp}(K_{2})=\mathsf{gcp}(\\{2.1\\})=2.1$. Then
$\mathsf{lift}(K_{2})=\\{+(+(x,s(y)),s(z))@\epsilon\hookrightarrow\ell@\epsilon\\}$,
which yields the transition $(s_{0},2.1)\in\delta(s_{1},s)$.

###  4.4 Output patterns

The output patterns after an $f$-transition are simply the match announcements
that accompany the match obligations that reduce to $\emptyset$:

$\eta(s,f)=\\{ma\in\mathit{MA}\mid f(x_{1},\dots,x_{n})@L(s)\hookrightarrow
ma\in s\wedge x_{1},\dots,x_{n}\in\mathbb{V}\\}\,.$

###### Example 7

Consider state $s_{3}$ in Fig. 1. The goal
$s(y)@1.2\hookrightarrow\ell@\epsilon$ can be completed upon observing $s$ at
position $1.2$, so we fix $\eta(s_{3},s)=\\{\ell@\epsilon\\}$.

###  4.5 Construction summary

The following definitions summarize the construction of a set automaton.

  * •

$S$ is the set of all reachable states;

  * •

$s_{0}=\\{\ell@\epsilon\hookrightarrow\ell@\epsilon\mid\ell\in\mathcal{L}\\}$;

  * •

$L(s)\in\mathsf{pos}(mo)$ for some root goal $mo\hookrightarrow ma\in s$;

  * •

$\delta(s,f)=\\{(\mathsf{lift}(K),\mathsf{gcp}(K))\mid
K\in[\mathsf{deriv}(s.f)]_{\sim}\\}$ for all $(s,f)\in S\times\mathbb{F}$; and

  * •

$\eta(s,f)=\\{ma\in\mathit{MA}\mid f(x_{1},\dots,x_{n})@L(s)\hookrightarrow
ma\in s\\}$ for all $(s,f)\in S\times\mathbb{F}$.

For the remainder of this paper we assume that instead of patterns, the output
function yields rewrite rules. That is, given the computed output function
$\eta$ and the TRS $\mathcal{R}$ we use $\eta^{\prime}(s,f)=\\{(\ell\to
r)@p\mid\ell\to r\in\mathcal{R}\wedge\ell@p\in\eta(s,f)\\}$.

##  5 Rewriting with configuration trees

We formally define a rewrite procedure that uses set automaton matching to
explore the completed configuration tree step by step. This procedure only
works for left-linear TRSs. An extension for non-linear TRSs will be discussed
in the next section.

Algorithm 1 is the formal foundation for set automaton-based rewriting. It
maintains a set of found redexes, and a configuration tree. Furthermore it
uses some auxiliary manipulations on the configuration tree which we define
below. The strategy determines whether to reduce a found redex, or to continue
matching a bud in $ct$. Formally a strategy is a partial mapping
$\mathsf{select}:\mathcal{C}\mathcal{T}\times\mathcal{P}(\mathcal{R}\times\mathbb{P})\rightharpoonup(S\times\mathbb{P})\cup(\mathcal{R}\times\mathbb{P})$
such that $\mathsf{select}(ct,reds)\in\mathsf{buds}(ct)\cup reds$, for all
pairs $(ct,reds)$ such that $\mathsf{buds}(ct)\cup reds$ is non-empty. Note
that strategies are only partial since they are undefined on budless
configuration trees paired with empty redex sets.

If the strategy selects a bud $\mathsf{B}(s,p)$, we inspect the head symbol of
term $t|_{p.L(s)}$, and grow the configuration tree according to the
transitions given by the set automaton. Formally this growth is defined by

$\displaystyle\mathsf{grow}$ $\displaystyle(ct,s,p,t)=$
$\displaystyle\begin{cases}\mathsf{N}(s,p,\\{\mathsf{B}(s^{\prime},p.p^{\prime})\mid(s^{\prime},p^{\prime})\in\delta(s,\mathsf{hd}(t|_{p.L(s)}))\\})&\text{if
$ct=\mathsf{B}(s,p)$}\\\ \mathsf{B}(s^{\prime},p^{\prime})&\text{if
$ct=\mathsf{B}(s^{\prime},p^{\prime})$}\\\ &\quad\text{with
$(s^{\prime},p^{\prime})\neq(s,p)$}\\\
\mathsf{N}(s^{\prime},p^{\prime},\\{\mathsf{grow}(ct^{\prime},s,p,t)\mid
ct^{\prime}\in cts\\})&\text{if
$ct=\mathsf{N}(s^{\prime},p^{\prime},cts)$}\end{cases}$

Intuitively $\mathsf{grow}(ct,s,p,t)$ replaces every bud $\mathsf{B}(s,p)$ by
a node with the same configuration. The successors of this node are new buds;
their configurations are given by the used set automaton transition. When
matching a part of a complete configuration tree, the grown bud is unique due
to Theorem 3.1. After growing the configuration tree, newly found redexes are
added to the redex set according to the $\mathsf{matches}$ function defined in
Section 3.

If the strategy selects a redex $(\ell\to r)@p$, then the term is rewritten to
$t[(\ell\to r)@p]$. The procedure then _prunes_ the configuration tree as
follows. Since a set automaton inspects the input term in a top-down fashion,
there must be a configuration in $ct$ where position $p$ was inspected. We
call this the _initialization configuration for redex $(\ell\to r)@p$_, more
precisely, the configuration $(s_{i},p_{i})$ such that $p_{i}.L(s_{i})=p$.
Upon applying the rewrite step $t[(\ell\to r)@p]$, only the subterm at
position $p$ changes. Any matching that was not done below position $p$ is
still valid: it suffices to prune the configuration tree up to the
initialization configuration of the used redex. Define
$\mathsf{prune}(\mathsf{B}(s,p),q)=\mathsf{B}(s,p)$ and

$\mathsf{prune}(\mathsf{N}(s,p,cts),q)=\begin{cases}\mathsf{B}(s,p)&\text{if
$p.L(s)=q$}\\\ \mathsf{N}(s,p,\\{\mathsf{prune}(ct^{\prime},q)\mid
ct^{\prime}\in cts\\})&\text{otherwise}\,.\\\ \end{cases}$

Lastly, the set of redexes needs to be updated after a rewrite. All redexes
that were obtained in the pruned configuration tree are no longer valid. Given
$ct$, denote by $ct[p]$ the sub-configuration tree with root configuration
$(s,q)$ in $ct$ such that $p=q.L(s)$. Note that $ct[p]$ does not necessarily
exist, but if it exists and $ct$ is a fragment of a completed tree, then
$ct[p]$ is unique by Theorem 3.1.

Algorithm 1 A rewrite procedure that remembers part of the matching
information by pruning a part of the configuration tree. We assume the
availability of a set automaton $(S,s_{0},L,\delta,\eta)$ constructed for the
TRS at hand.

1:procedure Normalize(Term $t_{0}$, Strategy $\mathsf{select}$)

2: $t\leftarrow t_{0}$

3: $reds\leftarrow\emptyset$ $\triangleright$ Redexes

4: $ct\leftarrow\mathsf{B}(s_{0},\epsilon)$ $\triangleright$ Configuration
tree

5: while $\mathsf{buds}(ct)\neq\emptyset\vee reds\neq\emptyset$ do

6: $action\leftarrow\mathsf{select}$ from $\mathsf{buds}(ct)\cup reds$

7: if $action$ is a configuration $(s,p)$ then

8: $ct\leftarrow\mathsf{grow}(ct,s,p,t)$

9: $reds\leftarrow reds\cup\mathsf{matches}(s,p,t)$

10: else if $action$ is a redex $(\ell\to r)@p\in reds$ then

11: $reds\leftarrow
reds\setminus\bigcup\\{\mathsf{matches}(s,q,t)\mid(s,q)\in\mathsf{nodes}(ct[p])\\}$

12: $ct\leftarrow\mathsf{prune}(ct,p)$

13: $t\leftarrow t[(\ell\to r)@p]$ return $t$

###### Example 8

Consider the TRS $\mathcal{R}_{if}$ given by the five rules

$\displaystyle R_{1}:if(true,x,y)\xrightarrow{}x$ $\displaystyle
R_{2}:if(false,x,y)\xrightarrow{}y$ $\displaystyle
R_{3}:not(true)\xrightarrow{}false$ $\displaystyle
R_{4}:not(false)\xrightarrow{}true$ $\displaystyle\qquad
R_{5}:not(not(x))\xrightarrow{}x\,.$

In Fig. 3 there is a set automaton generated for $\mathcal{R}_{if}$. Contrary
to the automaton in Fig. 1, this simpler one only produces configuration trees
that have the same shape as the terms that it is executed on. In Fig. 4 there
is the term $t=if(not(not(true)),false,true)$ on the left, and in the middle
there is a partially explored configuration tree of $t$. It is obtained by
growing $\mathsf{B}(s_{0},\epsilon)$ with selected configurations
$(s_{0},\epsilon)$, $(s_{1},\epsilon)$ and $(s_{2},1)$.

The last configuration yields a match for $R_{5}$ at position $1$. A rewrite
with this redex yields $t^{\prime}=if(true,false,true)$ and the configuration
tree on the right. The symbol $if$ does not need to be inspected again, since
the initialisation configuration of $R_{5}@1$ is $(s_{1},\epsilon)$.

Figure 3: A set automaton for $\mathcal{R}_{if}$. To limit clutter,
$\delta(s_{2},if)$ is not displayed.

Figure 4:  The term $t=if(not(not(true)),false,true)$, a partial configuration
tree leading to the discovery of $R_{5}@1$ and the result of pruning.

###  5.1 Correctness

We prove that Algorithm 1, satisfies a simple invariant. Intuitively, we show
that the maintained configuration tree remains a fragment of the completed
configuration tree of the current term, and the redex set correctly maintains
all redexes that can be derived from the observations in the current
configuration tree. First we need some formalities on configuration trees.

The ‘is fragment of’ relation $\sqsubseteq$ on $\mathcal{C}\mathcal{T}$ is the
smallest relation such that

  * •

$\mathsf{B}(s,p)\sqsubseteq\mathsf{B}(s,p)$ and
$\mathsf{B}(s,p)\sqsubseteq\mathsf{N}(s,p,cts)$ and

  * •

$\mathsf{N}(s,p,cts)\sqsubseteq\mathsf{N}(s,p,cts^{\prime})$ if and only if
there is a bijection $\varphi:cts\to cts^{\prime}$ such that
$ct\sqsubseteq\varphi(ct)$ for all $ct\in cts$.

This definition makes $\langle\mathcal{C}\mathcal{T},\sqsubseteq\rangle$ a
partial ordering. Intuitively we have $ct_{1}\sqsubseteq ct_{2}$ whenever we
can change $ct_{1}$ into $ct_{2}$ by zero or more applications of
$\mathsf{grow}$. In particular we are interested in fragments of completed
configuration trees.

######  Lemma 1 ()

The following properties hold for operations on configuration trees.

  * •

if $ct\sqsubseteq\mathsf{completed}(t)$ then
$\mathsf{grow}(ct,s,p,t)\sqsubseteq\mathsf{completed}(t)$ for all
$(s,p)\in\mathsf{buds}(\mathsf{completed}(t))$;

  * •

if $ct\sqsubseteq ct^{\prime}$ then
$\mathsf{prune}(ct,p)\sqsubseteq\mathsf{prune}(ct^{\prime},p)$;

  * •

$\mathsf{prune}(ct,p)\sqsubseteq ct$;

  * •

if $t\xrightarrow{(\ell\to r)@p}t^{\prime}$, then
$\mathsf{prune}(\mathsf{completed}(t),p)=\mathsf{prune}(\mathsf{completed}(t^{\prime}),p)$;
and

  * •

if $ct[p]$ exists then
$\mathsf{nodes}(\mathsf{prune}(ct,p))=\mathsf{nodes}(ct)\setminus\mathsf{nodes}(ct[p])$.

######  Lemma 2 ()

Let $t_{0}$ be a ground term. Then the invariant given by

$t_{0}\xrightarrow{}^{*}t\wedge ct\sqsubseteq\mathsf{completed}(t)\wedge
reds=\bigcup\\{\mathsf{matches}(s,p,t)\mid(s,p)\in\mathsf{nodes}(ct)\\}\,,$

is initialized and maintained by Normalize.

###### Proof

For initialization, since $t=t_{0}$ we trivially have
$t_{0}\xrightarrow{}^{*}t$. Moreover
$\mathsf{B}(s_{0},\epsilon)\sqsubseteq\mathsf{completed}(t)$ by definition of
$\mathsf{completed}(t)$. Lastly since
$\mathsf{nodes}(ct)=\mathsf{nodes}(\mathsf{B}(s,p))=\emptyset$ we have
$reds=\emptyset=\bigcup\\{\mathsf{matches}(s,p,t)\mid(s,p)\in\mathsf{nodes}(ct)\\}$.

For invariant maintenance, consider $t$, $ct$ and $reds$ such that they
satisfy the invariant and suppose that $\mathsf{buds}(ct)\cup
reds\neq\emptyset$. We prove that both cases of the if-statement preserve the
invariant.

  * •

Suppose that $\mathsf{select}(ct,reds)=(s,p)$, some configuration in
$\mathsf{buds}(ct)$, and let $f=\mathsf{hd}(t|_{p.L(s)})$. Since $t$ is
unchanged, $t_{0}\xrightarrow{}^{*}t$ holds by assumption. Moreover
$\mathsf{grow}(ct,s,p,t)\sqsubseteq\mathsf{completed}(t)$ by Lemma 1. Conclude
by the calculation:

$\displaystyle reds^{\prime}$ $\displaystyle=reds\cup\mathsf{matches}(s,p,t)$
$\displaystyle=\bigcup\\{\mathsf{matches}(s^{\prime},p^{\prime},t)\mid(s^{\prime},p^{\prime})\in\mathsf{nodes}(ct)\\}\cup\mathsf{matches}(s,p,t)$
$\displaystyle=\bigcup\\{\mathsf{matches}(s^{\prime},p^{\prime},t)\mid(s^{\prime},p^{\prime})\in\mathsf{nodes}(ct)\cup\\{(s,p)\\}\\}$
$\displaystyle=\bigcup\\{\mathsf{matches}(s^{\prime},p^{\prime},t)\mid(s^{\prime},p^{\prime})\in\mathsf{nodes}(\mathsf{grow}(ct,s,p,t))\\}\,.$

  * •

Otherwise suppose that $\mathsf{select}(ct,reds)=(\ell\to r)@p$, some redex in
$reds$. Let $t^{\prime}=t[(\ell\to r)@p]$. By
$ct\sqsubseteq\mathsf{completed}(t)$ and Theorem 3.2 it follows that $(\ell\to
r)@p$ is a redex of $t$. Therefore
$t_{0}\xrightarrow{}^{*}t\xrightarrow{(\ell\to r)@p}t[(\ell\to
r)@p]=t^{\prime}$, hence $t_{0}\xrightarrow{}^{*}t^{\prime}$ as needed. Next
we show that $\mathsf{prune}(ct,p)\sqsubseteq\mathsf{completed}(t^{\prime})$.
By assumption $ct\sqsubseteq\mathsf{completed}(t)$. Then Lemma 1 enables the
calculation:

$\displaystyle\mathsf{prune}(ct,p)$
$\displaystyle\sqsubseteq\mathsf{prune}(\mathsf{completed}(t),p)$
$\displaystyle=\mathsf{prune}(\mathsf{completed}(t^{\prime}),p)$
$\displaystyle\sqsubseteq\mathsf{completed}(t^{\prime})$

Hence $\mathsf{prune}(ct,p)\sqsubseteq\mathsf{completed}(t^{\prime})$ as
required. Next, let

$reds^{\prime}=reds\setminus\bigcup\\{\mathsf{matches}(s,q,t)\mid(s,q)\in\mathsf{nodes}(ct[p])\\}\,.$

Then:

$\displaystyle reds^{\prime}$
$\displaystyle=reds\setminus\bigcup\\{\mathsf{matches}(s,q,t)\mid(s,q)\in\mathsf{nodes}(ct[p])\\}$
$\displaystyle=\bigcup\\{\mathsf{matches}(s,q,t)\mid(s,q)\in\mathsf{nodes}(ct)\\}$
$\displaystyle\hskip
8.5359pt\setminus\bigcup\\{\mathsf{matches}(s,q,t)\mid(s,q)\in\mathsf{nodes}(ct[p])\\}$
$\displaystyle=\bigcup\\{\mathsf{matches}(s,q,t)\mid(s,q)\in\mathsf{nodes}(ct)\setminus\mathsf{nodes}(ct[p])\\}$
$\displaystyle=\bigcup\\{\mathsf{matches}(s,q,t)\mid(s,q)\in\mathsf{nodes}(\mathsf{prune}(ct,p))\\}\,.$

Therefore
$reds^{\prime}=\bigcup\\{\mathsf{matches}(s,q,t)\mid(s,q)\in\mathsf{nodes}(\mathsf{prune}(ct,p))\\}$
as needed.

Lemma 2 states that Algorithm 1 produces valid rewrite steps. Of course,
termination depends on the TRS and the strategy, which we have abstracted from
so far and will remain to do so until Section 7. We conclude with the
corollary of partial correctness.

###### Corollary 1

If $\textsc{Normalize}(t_{0},\mathsf{select})$ returns $t$, then $t$ is a
normal form of $t_{0}$.

###### Proof

Suppose that the procedure terminates with values $t$, $ct$ and $reds$. By
Lemma 2 the invariant is satisfied. By termination,
$\mathsf{buds}(ct)=\emptyset$ and $reds=\emptyset$. Since $ct$ has no buds,
$ct=\mathsf{completed}(t)$. By Theorem 3.2 and $reds=\emptyset$ there are no
redexes in $t$. To conclude, $t_{0}\xrightarrow{}^{*}t$, hence $t$ is a normal
form of $t_{0}$.

##  6 Supporting non-linear rewrite rules

We extend Algorithm 2 to support non-linear TRSs using simple subterm
comparisons. Before we address the problem, some remarks on the literature are
in order. It is well-known that non-linear patterns cannot be matched by a
regular tree automaton [10]. The proof for this claim is a textbook pumping
lemma application. To support these patterns, tree automata with equality and
disequality constraints were introduced [3, 10]. These feature transitions
that are guarded by finite constraints on subterms, and traverse terms in a
bottom-up fashion. Little is known about the efficiency of this approach
however. Tree automata with constraints can check some equalities and
disequalities multiple times as the guards on the transitions can be
arbitrarily large.

The interplay between linear pattern matching and subterm equality is also
interesting in the root pattern matching case. Subterm (dis)equalities may
rule out pattern matches, and vice versa, function symbol observations may
rule out the necessity for checking (dis)equality. Similar automata/decision
trees have been used in the root pattern matching case featuring decision
nodes with only a single equality check per transition [12, 17, 27]. These
approaches are susceptible to redundant equality checks as well; an optimal
solution is unknown to exist.

Originally, set automata do not support non-linear pattern matching. Since
patterns with repeating variables appear to be much-requested whereas an
optimal solution is a significant theoretical challenge, we simply deploy
_consistency checks_. Whenever a non-linear pattern is yielded by the set
automaton, we need the required subterm equalities to hold before it can be
used as a redex. This simple solution suffices to support non-linear matching,
but we need to take more care in adapting Algorithm 1 for non-linear
rewriting.

We proceed with the following formal definitions. Let $\ell$ be a pattern, and
recall that $\mathcal{E}(\ell)$ is the set of positions where $\ell$ has a
variable. Define $\pi(\ell)$ as the unique partition of $\mathcal{E}(\ell)$
such that for all sets $P\in\pi(\ell)$, for all $p,q\in\mathcal{E}(\ell)$ we
have that $p,q\in P$ if, and only if $\ell|_{p}=\ell|_{q}$. In other words,
$\pi(\ell)$ contains the sets of positions where $\ell$ has the same variable.
Note that linear patterns only have singleton partitions, and therefore
$|\pi(\ell)|=|\mathcal{E}(\ell)|$. Non-linear patterns have at least one set
in their partition of size at least two, and therefore
$|\pi(\ell)|<|\mathcal{E}(\ell)|$. We say that _$t$ is consistent with
$\pi(\ell)$_ iff for all $P\in\pi(\ell)$, for all $p,q\in P$ we have
$t|_{p}=t|_{q}$. Lastly, we say that _$t$ pre-matches $\ell$_ iff for all
$p\in\mathcal{D}_{\setminus\mathcal{E}}(\ell)$ we have that
$\mathsf{hd}(t|_{p})=\mathsf{hd}(\ell|_{p})$.

###### Proposition 1

A term $t$ matches the pattern $\ell$ iff $t$ pre-matches $\ell$ and $t$ is
consistent with $\pi(\ell)$.

For linear patterns, pre-matching coincides with matching since since the
consistency check is satisfied vacuously. A set automaton checks exactly pre-
matching for all patterns and all subterms of $t$ simultaneously. It does not
check for consistency though. We opted to outsource these checks to the
rewrite procedure, and have set automata yield the non-linear patterns in a
separate set.

A _non-linear set automaton_ for $\mathcal{L}$ is a structure
$(S,s_{0},L,\delta,\eta_{L},\eta_{NL})$ where $S,s_{0},L$ and $\delta$ are
defined as in set automata, and
$\eta_{L},\eta_{NL}:S\times\mathbb{F}\to\mathcal{P}(\mathcal{L})$ yield a set
of linear patterns and a set of non-linear patterns respectively. Given a set
automaton $(S,s_{0},L,\delta,\eta)$ for $\mathcal{L}$ we obtain a non-linear
set automaton $(S,s_{0},L,\delta,\eta_{L},\eta_{NL})$ for $\mathcal{L}$ where
$\eta_{L}(s,f)=\\{\ell\in\eta(s,f)\mid|\pi(\ell)|=|\mathcal{E}(\ell)|\\}$ and
$\eta_{NL}(s,f)=\\{\ell\in\eta(s,f)\mid|\pi(\ell)|<|\mathcal{E}(\ell)|\\}$.
Define $\mathsf{matches}_{L}$ and $\mathsf{matches}_{NL}$ (for
$X\in\\{L,NL\\}$) by

$\mathsf{matches}_{X}(s,p,t)=\\{(\ell\to r)@p.q\mid(\ell\to
r)@q\in\eta_{X}(s,\mathsf{hd}(t|_{p.L(s)}))\\}\,.$

Algorithm 2 rewrites a term by using a non-linear set automaton. When applied
to a linear TRS it behaves exactly the same as its linear counterpart. In the
case of non-linear patterns more bookkeeping comes into play.

  * •

All non-linear patterns yielded by the set automaton are first stored in a set
of ambiguous matches, for they need to be checked for consistency before they
can be used to reduce the term.

  * •

We add the option to check an ambiguous match for consistency to the same pool
of options as the choice of whether to match a symbol or reduce a redex. When
a match is consistent then it is _enabled_ , and can be chosen in the future
to reduce the term. Otherwise it is stored in a set of _disabled_ matches.

  * •

When a reduction is applied, we need to remove all redexes that were obtained
below the pruning point as in Algorithm 1. Additionally, some disabled matches
may be enabled by the change, and vice versa. This applies to all enabled and
disabled matches that have a repeating variable above the position where the
rewrite step was applied. The procedure moves those matches to the set of
ambiguous redexes, so they can be checked again at some later point.

Algorithm 2 A rewriting procedure that supports non-linear patterns. We assume
the availability of a non-linear set automaton
$(S,s_{0},L,\delta,\eta_{L},\eta_{NL})$ constructed for the TRS at hand.

1:procedure NormalizeNonLinear(Term $t_{0}$, Strategy $\mathsf{select}$)

2: $t\leftarrow t_{0}$

3: $reds_{L}\leftarrow\emptyset$ $\triangleright$ Linear redexes

4: $am,dis,en\leftarrow\emptyset$ $\triangleright$ Ambiguous, disabled and
enabled pre-matches

5: $ct\leftarrow\mathsf{B}(s_{0},\epsilon)$ $\triangleright$ Configuration
tree

6: while $\mathsf{buds}(ct)\neq\emptyset\vee reds_{L}\neq\emptyset\vee
en\neq\emptyset\vee am\neq\emptyset$ do

7: $action\leftarrow\mathsf{select}$ from $\mathsf{buds}(ct)\cup
am\cup(reds_{L}\cup en)$

8: if $action$ is a configuration $(s,p)$ from $\mathsf{buds}(ct)$ then

9: $ct\leftarrow\mathsf{grow}(ct,s,p,t)$

10: $reds_{L}\leftarrow reds_{L}\cup\mathsf{matches}_{L}(s,p,t)$

11: $am\leftarrow am\cup\mathsf{matches}_{NL}(s,p,t)$

12: else if $action$ is an ambiguous redex $(\ell\to r)@p$ from $am$ then

13: $am\leftarrow am\setminus\\{(\ell\to r)@p\\}$

14: if $t|_{p}$ is consistent with $\pi(\ell)$ then

15: $en\leftarrow en\cup\\{(\ell\to r)@p\\}$

16: else

17: $dis\leftarrow dis\cup\\{(\ell\to r)@p\\}$

18: else if $action$ is a redex $(\ell\to r)@p\in reds_{L}\cup en$ then

19: $reds_{L}\leftarrow
reds_{L}\setminus\bigcup\\{\mathsf{matches}_{L}(s,q,t)\mid(s,q)\in\mathsf{nodes}(ct[p])\\}$

20: Update$(am,dis,en,ct,t,p)$

21: $ct\leftarrow\mathsf{prune}(ct,p)$

22: $t\leftarrow t[(\ell\to r)@p]$ return $t$

23:

24:procedure Update($am$, $dis$, $en$,$ct$,$t$,$p$)$\triangleright$ Updates
$am$,$dis$ and $en$ after a rewrite

25: $en\leftarrow
en\setminus\bigcup\\{\mathsf{matches}_{NL}(s,q,t)\mid(s,q)\in\mathsf{nodes}(ct[p])\\}$

26: $dis\leftarrow
dis\setminus\bigcup\\{\mathsf{matches}_{NL}(s,q,t)\mid(s,q)\in\mathsf{nodes}(ct[p])\\}$

27: $rem\leftarrow\\{(\ell\to r)@q\in en\cup dis$

28: $\mid\exists P\in\pi(\ell):|P|\geq 2\wedge\exists q^{\prime}\in
P:q.q^{\prime}\leq p\\}$

29: $en\leftarrow en\setminus rem$

30: $dis\leftarrow dis\setminus rem$

31:
$am\leftarrow(am\setminus\bigcup\\{\mathsf{matches}_{NL}(s,q,t)\mid(s,q)\in\mathsf{nodes}(ct[p])\\})\cup
rem$

###### Example 9

We demonstrate Algorithm 2 with the TRS given by the rules

$R_{1}:f(x,x,y)\to y\quad R_{2}:f(x,y,y)\to x\quad R_{3}:f(x,y,x)\to x\quad
R_{4}:h(a)\to a\,,$

and the term $t_{0}=f(a,h(a),h(a))$. If we match $t_{0}$ before doing any
consistency checks, we obtain $reds_{L}=\\{R_{4}@2,R_{4}@3\\}$ and
$am=\\{R_{1}@\epsilon,R_{2}@\epsilon,R_{3}@\epsilon\\}$. Consistency checking
results in $am=\emptyset$, $dis=\\{R_{1}@\epsilon,R_{3}@\epsilon\\}$, and
$en=\\{R_{2}@\epsilon\\}$.

Suppose that we apply the redex $R_{4}@2$ to get $t_{1}=f(a,a,h(a))$. The
update function reorganizes the non-linear pre-matches. The disabled pre-match
$R_{1}@\epsilon$ and the enabled pre-match $R_{2}@\epsilon$ are moved to $am$,
since their consistency status depends on a subterm that changed due to the
rewrite step. The disabled pre-match $R_{3}@\epsilon$ remains disabled.

###  6.1 Correctness

Partial correctness of Algorithm 2 can be shown similarly to how we proved
partial correctness of Algorithm 1. The most notable difference is the
administration that the update function facilitates. The following proposition
states that (in)consistency is preserved for all some pre-matches under a
certain condition.

###### Proposition 2

Let $t$ be a term such that $t|_{p}$ pre-matches $\ell$, and let
$t^{\prime}=t[u]_{p^{\prime}}$ for some $u$ and some $p^{\prime}\geq p$. If
$t^{\prime}|_{p}$ pre-matches $\ell$, and there is no $P\in\pi(\ell)$ and no
position $q^{\prime}\in P$ with $|P|\geq 2$ and $p^{\prime}\leq q^{\prime}$,
then $t|_{p}$ is consistent with $\pi(\ell)$, if, and only if,
$t^{\prime}|_{p}$ is consistent with $\pi(\ell)$

###### Lemma 3

Let $t_{0}$ be a ground term. The invariant given by the conjunction of

  1. 1.

$t_{0}\xrightarrow{}^{*}t$

  2. 2.

$ct\sqsubseteq\mathsf{completed}(t)$

  3. 3.

$reds_{L}=\bigcup\\{\mathsf{matches}_{L}(s,p,t)\mid(s,p)\in\mathsf{confs}(ct)\\}$

  4. 4.

$am\cup dis\cup
en=\bigcup\\{\mathsf{matches}_{NL}(s,p,t)\mid(s,p)\in\mathsf{confs}(ct)\\}$

  5. 5.

$reds_{L}$, $am$, $dis$, and $en$ are disjoint

  6. 6.

$\forall(\ell\to r)@p\in en:\text{$t|_{p}$ is consistent with $\pi(\ell)$}$

  7. 7.

$\forall(\ell\to r)@p\in dis:\text{$t|_{p}$ is not consistent with
$\pi(\ell)$}$

is initialized and maintained by Algorithm 2.

###### Proof

We only highlight the differences with the proof of Lemma 2. For Item 1, since
Algorithm 2 can also pick non-linear redexes from $en$, we need Lemma 1 and
Item 6 of the invariant to show that $t_{0}\xrightarrow{}^{*}t$ is maintained.
Items 3 and 4 are shown similarly to Lemma 2, but the proofs are more
cumbersome. Item 5 is a standard exercise in set theory and program
correctness. Items 6 and 7 are preserved due to Proposition 2.

###### Corollary 2

If NormalizeNonLinear($t_{0}$, $\mathsf{select}$) returns $t$ then $t$ is a
normal form of $t_{0}$.

##  7 Implementation

As a proof of concept, we have implemented the set automaton construction and
an instance of Algorithm 2 in the Rust programming language. We have dubbed
the implementation SABRE: Set Automaton Based Rewrite Engine. For comparison
we have also implemented a Simple Innermost Rewrite Engine (SIRE) using
adaptive pattern matching automata from [24]. Both rewriters use maximal
subterm sharing, just like mCRL2. This allows compact representation of terms
and cheap term duplication. Moreover, checking the equality of subterms is a
constant time operation. The binaries, along with instructions on how to
replicate our benchmarking results are available on
Zenodo222https://doi.org/10.5281/zenodo.7197261.

##### Configuration stack.

SABRE uses a stack to explore the configuration tree depth-first. An element
on the stack consists of a configuration and a pointer to the remaining set
automaton edges in a hypertransition. Another optimisation is that a
configuration does not store the absolute position and the top-level term.
Instead it stores the subterm and the positional difference compared to the
configuration one layer higher in the stack. This positional difference stems
from a transition in the set automaton; the tool stores a pointer to this
position. These measures ensure that we can store a configuration with a fixed
amount of memory, i.e. no heap allocations are needed. Moreover, with an
additional trick, the prune operation described in Section 5 can be done in
constant time. This trick in the set automaton construction involves keeping
track of the amount of function symbols that have been inspected since the
creation, for every match goal.

##### Outermost matching.

Recall that set automata enable many traversals of the configuration tree. We
implemented a different dependency relation to construct the set automaton so
that the aforementioned depth-first traversal yields outermost matches first.
On match goals $g_{1}=mo_{1}\to\ell_{1}@p_{1}$ and
$g_{2}=mo_{2}\to\ell_{2}@p_{2}$ we use the _outermost preserving dependency
relation_ $R_{op}$ defined by $g_{1}\mathrel{R_{op}}g_{2}$ if, and only if,
$p_{1}\leq p_{2}\vee p_{2}\leq p_{1}$. This relation is coarser than the
relation $R_{dep}$ described in Section 4, and intuitively maintains look-
ahead on patterns until they are not guaranteed to be outermost. Additionally
it preserves all the correctness properties of pattern matching and has the
additional advantage that a depth-first traversal of the configuration tree
yields outermost matches first, unless the first discovered redex is a subterm
of an outermost match that may be discovered at a later point. For example,
given the patterns $f(g(h(x)))$ and $g(x)$, we will always discover $g(x)$
first. A drawback of this relation is that it yields a bigger automaton. We
refrained from presenting this relation thus far since the problem is subtle
and yields set automata that are too complex to explain. An in-depth study of
these dependency relations is left as future work.

##### Strategy.

SABRE has a baked-in, mostly outermost strategy. In principle SABRE applies a
rewrite rule at the moment a match is found, with three exceptions that we
will explore. Firstly, the tool has special treatment of _duplicating_ rewrite
rules, i.e. rules for which application duplicates subterms, e.g. $f(x)\to
g(x,x)$. Such rewrite rules are parked on a separate strategy stack, forming a
data structure to remember matching rewrite rules that are not applied upon
discovery. The rule is applied at the moment the entire subconfiguration tree
below the node where the duplicating rule was found has been explored. This
means that when the rule is applied, its subterms (that are duplicated) are
guaranteed to be in normal form. Secondly, non-linear rewrite rules are not
always performed in outermost fashion. Upon discovery, equivalence of subterms
is checked. If the equivalences do not (yet) hold the match is parked on the
strategy stack until the rest of the configuration subtree has been explored.
Finally, our implementation also supports conditional rewrite rules which is
needed as they are part of the chosen benchmarks. The implementation is ahead
of the theory in this regard. Conditional rewrite rules are always first put
on the strategy stack. The conditions are evaluated once the entire
subconfiguration tree of the conditional pre-match is explored.

##### Benchmark selection.

We have turned to a set of benchmarks used in the recurring Rewriting Engine
Competition (REC). This competition has its own format for TRSs: the REC
format. Translations exist from this REC format to a multitude of popular
rewrite engines. The REC format does not support non-linear rewrite rules, as
not all tools in the competitions support it. We use the benchmarks available
on the
webpage333https://sourcesup.renater.fr/scm/viewvc.php/rec/2019-CONVECS/, which
contains benchmarks in preparation for a next REC. Some TRSs are excluded.
Some rewrite specifications include a “META” section containing code to
generate a part of the specification, we do not support this feature yet. We
have also excluded the benchmarks “langton6” and “langton7” as they implicitly
assume a priority order on the rewrite rules based on the order in which they
are listed, which we intentionally do not support (and which is not mentioned
in [14]). In total we use 74 benchmarks, which are listed in the Zenodo
repository.

##### Tool selection.

We decided to benchmark SABRE, SIRE, mCRL2, Maude and Haskell. There are two
rewriters in the mCRL2 toolset: jitty (just-in-time) and jittyc (compiling
jitty). The jittyc rewrite engine generates and compiles C++ code specific to
the TRS. Haskell and Maude were selected because they won the last competition
(REC 2018); Haskell was the fastest rewrite engine overall, and Maude was the
fastest rewriter among the algebraic languages.

##### Benchmark setup.

There are multiple decisions to be made in measuring rewriting performance. We
have opted to split preprocessing time and rewriting time wherever possible.
The context of the development of SABRE is model checking, where we typically
need to rewrite millions or billions of terms, making preprocessing time less
relevant. For jitty and Maude we were not able to split the preprocessing and
running times. They therefore have a (slight) handicap in the running time
benchmark. As not every tool is able to solve every benchmark in a reasonable
time frame we use a timeout of 5 minutes, just like in the REC. As performance
metrics we use both the number of problems solved and the total time spent.
All benchmarks are performed on a 2018 MacBook pro equipped with an 2.6GHz i7
processor and 32GB of RAM.

Benchmark | SABRE | SIRE | jitty | jittyc | Maude | Haskell
---|---|---|---|---|---|---
benchsym22 | 9.45 | 5.51 | 31.27 | 0.67 | 3.76 | 0.54
benchtree10 | 0.70 | DNF | DNF | 41.00 | 0.51 | 0.22
benchtree20 | 11.53 | DNF | DNF | DNF | 6.29 | 1.24
benchtree22 | 50.28 | DNF | DNF | DNF | 23.20 | 6.27
binarysearch | 11.97 | 12.52 | 61.13 | 1.58 | 24.50 | 1.93
bubblesort1000 | 47.18 | 5.70 | 92.17 | 0.75 | 3.46 | 0.49
evalsym | 33.71 | 54.43 | DNF | 8.44 | 148.85 | 8.58
evaltree | 1.33 | 2.22 | 32.67 | 32.05 | 16.13 | 1.40
fib32 | 9.33 | 5.45 | 30.66 | 1.44 | 12.67 | 0.99
maa | 136.44 | 27.29 | 42.59 | 1.80 | 22.32 | 0.95
mergesort100 | 0.80 | DNF | DNF | DNF | 0.47 | 0.24
mergesort1000 | 0.35 | DNF | DNF | DNF | 0.29 | 0.12
quicksort100 | 0.34 | DNF | DNF | DNF | 0.55 | 0.23
quicksort1000 | 76.11 | DNF | DNF | DNF | 7.23 | 2.30
revnat10000 | 56.37 | 31.51 | 33.33 | 2.97 | 14.18 | 6.69
sieve2000 | 20.78 | 5.31 | 93.20 | 0.24 | 2.87 | 0.38
sieve10000 | DNF | DNF | DNF | 13.54 | 221.90 | 26.35
Total successes | 73 | 66 | 65 | 68 | 74 | 74
Total failures | 1 | 8 | 9 | 6 | 0 | 0
Percentage | 98.7% | 89.2% | 87.8% | 91.9% | 100.0% | 100.0%
Total time | 813 | 2576 | 3257 | 1909 | 553 | 73
Table 1: Running times in seconds to solve a given benchmark, preprocessing
omitted where possible. DNF = Did Not Finish. DNF is counted as 300 seconds in
the computation of the total time spent.

##### Benchmark running time results.

Table 1 shows the time it takes to solve the REC problems. There is not enough
space to show the results of all benchmarks. The table lists all benchmarks
where at least one of the tools took more than 30 seconds to finish. SABRE
comfortably beats SIRE, jitty and jittyc, but is beaten by Maude and Haskell.
SABRE does beat Maude in 4 benchmarks by some margin: ‘binarysearch’,
‘evalexpr’, ‘evalsym’ and ‘evaltree’. In some benchmarks it appears that the
innermost strategies of SIRE, jitty and jittyc are inferior by a large margin:
‘benchtree’, ‘mergesort’ and ‘quicksort’.

##### Preprocessing evaluation.

As mentioned, the preprocessing time is of secondary value to us.
Nevertheless, it is important that the preprocessing time is not excessive.
Table 2 presents statistics on the preprocessing time and the size of the set
automaton. Only the benchmarks with at least 50 rewrite rules are presented in
the table. Constructing the set automaton for the ‘maa’ benchmark is rather
expensive. The determining factor for the cost of set automaton construction
seems to be the number of transitions, which is determined by the equation
$\text{\\#transitions}=\text{\\#symbols}\times\text{\\#states}$. The number of
states does not directly correlate to the number of symbols or rewrite rules.
Currently we do not know a method to compute the size of a set automaton
without generating it. The determining factor seems to be the pattern depth
and overlap in the pattern set.

Benchmark |  #symbols/ #rules |  #states/ #transitions | SABRE | SIRE | jittyc | Haskell
---|---|---|---|---|---|---
benchexpr10 | 92/155 | 47/4,324 | 0.13 | 0.50 | 9.81 | 0.81
binarysearch | 43/86 | 1,282/55,126 | 3.50 | 0.30 | 10.36 | 0.78
evalexpr | 27/70 | 24/648 | 0.23 | 0.20 | 8.48 | 0.75
fib32 | 33/69 | 1,036/34,188 | 1.76 | 0.30 | 9.43 | 0.79
fibfree | 27/232 | 101/2,727 | 0.22 | 0.30 | 9.16 | 0.87
maa | 708/750 | 831/588,348 | 389.69 | 0.73 | 92.94 | 2.32
Total time |  |  | 406.402 | 5.43 | 697.24 | 55.48
Table 2: Statistics on the preprocessing time needed by the tools.

##### Rewrite path comparison.

An interesting question is why certain tools are faster than others on certain
benchmarks: is the rewriting path shorter or is the number of rewrites per
second higher? Table 3 shows the number of rewrite steps needed by SABRE, SIRE
and Maude, for the same benchmarks listed in Table 1. The other tools do not
report the number of rewrite steps. The overall picture is that SABRE needs
fewer rewrite steps than SIRE and Maude, with some exceptions. SABRE needs
fewer symbol inspections per rewrite step, which is expected as the set
automaton remembers all the symbols it has inspected whilst matching. SABRE is
comparatively slow in terms of rewrite steps per second.

Benchmark | SABRE | SIRE | Maude
---|---|---|---
benchsym22 | 90,303,766 | 90,303,766 | 90,303,764
benchtree10 | 47,213 | DNF | 26,717
benchtree20 | 72,356,522 | DNF | 25,170,576
benchtree22 | 310,384,073 | DNF | 100,668,845
binarysearch | 107,501,220 | 265,511,947 | 310,310,897
bubblesort1000 | 167,670,646 | 167,670,646 | 168,171,144
evalsym | 361,204,694 | 1,438,834,118 | 1,664,833,899
evaltree | 15,208,759 | 62,407,963 | 104,614,038
fib32 | 84,116,962 | 108,788,784 | 137,416,567
maa | 392,119,718 | 441,111,164 | >395,558,243+
mergesort100 | 28,278 | DNF | 43,395
mergesort1000 | 4,199,124 | DNF | 6,454,547
quicksort10 | 695 | 40,645 | 959
quicksort100 | 207,982 | DNF | 384,630
quicksort1000 | 170,679,654 | DNF | 338,346,151
revnat10000 | 50,046,171 | 50,046,171 | 50,046,168
sieve2000 | 63,273,997 | 124,110,525 | 124,308,194
sieve10000 | DNF | DNF | 9,898,601,115
Total rewrite steps∗ | 1,579,878,114 | 3,149,524,528 | > 3,3 $\times 10^{9}$
Total symbol inspections∗ | 4,001,712,359 | 9,286,297,430 | unknown
Symbol inspections/
rewrite steps∗ | 2.53 | 2.95 | unknown
Rewrite steps/second∗ | 4,236,813 | 17,866,702 | >11,513,173,21
Table 3: Rewrite steps per benchmark. DNF = Did Not Finish. ∗For these metrics
we only selected the benchmarks for which SABRE, SIRE and Maude finished in
time. + The ‘maa’ benchmark consists of many terms that need to be rewritten,
of which Maude reports the number of rewrite steps per term individually. The
figure in the table represents the number of rewrite steps it takes to rewrite
the last term, which dominates the benchmark.

##### Bottleneck SABRE.

Profiling SABRE revealed that its bottleneck is constructing terms using the
maximally shared term storage. A lookup hash table is used to check if a term
already exists in the storage. For each rewrite step several lookups in this
hash table are needed. An optimisation implemented in SIRE and mCRL2s
rewriters is to not store the term that is currently being rewritten in the
maximally shared storage. Suppose that you have the following rewrite rule for
subtraction $sub(s(x),s(y))\to sub(x,y)$. This rewrite rule will be executed
in a large sequence if $x$ and $y$ represent large numbers. SABRE will call
the term storage for every intermediate result. SIRE, jitty and jittyc will
locally store the head symbol $sub$ and the list of subterms. Applying this
rewrite rule can be done by simply updating the list of subterms locally,
avoiding the lookup table. It is likely that something similar can be done for
SABRE, though the control flow is more difficult than with simple innermost
rewriters.

##  8 Conclusion, discussion and future work

In this paper we established a formal framework for rewriting based on set
automaton matching. We discussed a general rewrite procedure and proved its
correctness, and provided an extension that allows non-linear TRSs. We also
discussed a specific instance of the general rewrite procedure that runs an
outermost rewrite strategy by saving the configuration tree as a stack. Our
benchmarks show that this method is competitive among existing tools. There
are many optimizations left to explore, some of which require more theoretical
exploration and some of which are more implementation-based.

##### Evaluation benchmarks.

Besides being fast, rewriters must obviously also rewrite correctly. We have
checked the output of every REC benchmark and compared it to the output of
other rewriting engines, revealing that the langton benchmarks are not
suitable as they assume priority. For 50 ‘quick’ benchmarks we have validated
and stored the result; they form a suite of regression tests.

For any benchmark suite it is the question how representative it is of real
world specifications. We have opted to use the rather large and well known
benchmark suite from the rewriting engine competitions. Most benchmarks do not
have a lot of rewrite rules, making construction of the set automaton
relatively easy. For comparison, there are 478 rewrite rules in the standard
datatype specification of mCRL2, and industrial models can contain thousands
of rewrite rules. An omission in the REC benchmarks is the lack of non-linear
rewrite rules, we have thus not benchmarked SABRE in the presence of non-
linear rules.

##### Future work.

In the future we want to expand the set automaton rewriting technique to
minimize the information lost upon performing a rewrite step. For instance,
the structure of the right-hand sides is not used in our procedures. A
theoretical optimization is to precompile the configuration tree fragments
that arise from the right-hand sides, ensuring that we do not have to match
the function symbols of the right-hand side after subterm replacement.

Building upon this optimization, this new configuration tree fragment can
yield redexes straight away. This results in another rewrite, and another
precompiled fragment that can be attached to an even higher pruning point. If
such a rewrite sequence is long, then it gives rise to the following
algorithmic problem. Suppose that there exists a sequence $\\{t_{i}\\}_{1\leq
i\leq n}$, such that
$t_{0}\xrightarrow{R_{1}@p_{1}}t_{1}\xrightarrow{R_{2}@p_{2}}\dots\xrightarrow{R_{n}@p_{n}}t_{n}$.
How do we compute $t_{n}$ efficiently, without necessarily computing every
intermediate $t_{i}$? Seeing as a lot of time is spent executing rewrite
steps, including many queries to the maximally shared term storage, it might
be beneficial to investigate this problem.

Our benchmarks revealed that there is a great performance difference between
rewriting strategies. Rewriting strategies have been subjected to extensive
study, both of practical and theoretical nature [20, 21, 22, 25, 26].
Strategies are usually defined as functions that yield a reduction path for a
term, or as subsets of the rewrite relation $\xrightarrow{}^{*}$. The works
that focus on strategies typically abstract from the fact that pattern
matching is a non-trivial algorithmic problem. We intend to integrate the
existing work on strategies with our methods. A requirement is that deciding
which step to take next can be done efficiently in unison with matching using
the set automaton.

The proof of concept implementation of the set automaton is competitive with
existing tools but is beaten by Maude, the fastest rewriter in its class.
Haskell is still an order of magnitude faster but imposes different
restrictions on the rewrite rules. Constructing the set automaton can be slow
for larger rewrite systems. Compared to innermost rewriters (such as jittyc)
SABRE is much faster when the outermost rewriting path is shorter. When the
innermost and outermost paths are equal in length it comes down to raw
rewriting performance, where SABRE is currently beaten. We reckon there is
still room to optimize the raw rewriting performance, especially considering
it is still an experimental prototype. More specifically, as suggested in
Section 7, we could minimize the number of lookups in the maximally shared
term storage by first rewriting terms locally.

#### Acknowledgements

We want to thank Hubert Garavel for sending us the benchmark set used in
Rewrite Engine Competition.

## References

  * [1] Aho, A.V., Corasick, M.J.: Efficient string matching: An aid to bibliographic search. Commun. ACM 18(6), 333–340 (1975). https://doi.org/10.1145/360825.360855, https://doi.org/10.1145/360825.360855
  * [2] Baader, F., Nipkow, T.: Term rewriting and all that. Cambridge University Press (1998)
  * [3] Bogaert, B., Tison, S.: Equality and disequality constraints on direct subterms in tree automata. In: Finkel, A., Jantzen, M. (eds.) STACS 92, 9th Annual Symposium on Theoretical Aspects of Computer Science, Cachan, France, February 13-15, 1992, Proceedings. Lecture Notes in Computer Science, vol. 577, pp. 161–171. Springer (1992). https://doi.org/10.1007/3-540-55210-3_181, https://doi.org/10.1007/3-540-55210-3_181
  * [4] Brus, T.H., van Eekelen, M.C.J.D., van Leer, M.O., Plasmeijer, M.J.: Clean: A language for functional graph writing. In: Kahn, G. (ed.) Functional Programming Languages and Computer Architecture, Portland, Oregon, USA, September 14-16, 1987, Proceedings. Lecture Notes in Computer Science, vol. 274, pp. 364–384. Springer (1987). https://doi.org/10.1007/3-540-18317-5_20, https://doi.org/10.1007/3-540-18317-5_20
  * [5] Brzozowski, J.A.: Derivatives of regular expressions. J. ACM 11(4), 481–494 (1964). https://doi.org/10.1145/321239.321249, https://doi.org/10.1145/321239.321249
  * [6] Bunte, O., Groote, J.F., Keiren, J.J.A., Laveaux, M., Neele, T., de Vink, E.P., Wesselink, W., Wijs, A., Willemse, T.A.C.: The mCRL2 toolset for analysing concurrent systems - improvements in expressivity and usability. In: Vojnar, T., Zhang, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part II. Lecture Notes in Computer Science, vol. 11428, pp. 21–39. Springer (2019). https://doi.org/10.1007/978-3-030-17465-1_2, https://doi.org/10.1007/978-3-030-17465-1_2
  * [7] Christian, J.: Fast Knuth-Bendix completion: Summary. In: Dershowitz, N. (ed.) Rewriting Techniques and Applications, 3rd International Conference, RTA-89, Chapel Hill, North Carolina, USA, April 3-5, 1989, Proceedings. Lecture Notes in Computer Science, vol. 355, pp. 551–555. Springer (1989). https://doi.org/10.1007/3-540-51081-8_136, https://doi.org/10.1007/3-540-51081-8_136
  * [8] Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: specification and programming in rewriting logic. Theor. Comput. Sci. 285(2), 187–243 (2002). https://doi.org/10.1016/S0304-3975(01)00359-0, https://doi.org/10.1016/S0304-3975(01)00359-0
  * [9] Cleophas, L.G., Hemerik, K., Zwaan, G.: Two related algorithms for root-to-frontier tree pattern matching. Int. J. Found. Comput. Sci. 17(6), 1253–1272 (2006). https://doi.org/10.1142/S012905410600439X, https://doi.org/10.1142/S012905410600439X
  * [10] Comon, H., Dauchet, M., Gilleron, R., Löding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications. Available on: http://www.grappa.univ-lille3.fr/tata (2007), release October, 12th 2007
  * [11] Erkens, R., Groote, J.F.: A set automaton to locate all pattern matches in a term. In: Cerone, A., Ölveczky, P.C. (eds.) Theoretical Aspects of Computing - ICTAC 2021 - 18th International Colloquium, Virtual Event, Nur-Sultan, Kazakhstan, September 8-10, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12819, pp. 67–85. Springer (2021). https://doi.org/10.1007/978-3-030-85315-0_5, https://doi.org/10.1007/978-3-030-85315-0_5
  * [12] Erkens, R., Laveaux, M.: Adaptive non-linear pattern matching automata. Log. Methods Comput. Sci. 17(4) (2021). https://doi.org/10.46298/lmcs-17(4:21)2021, https://doi.org/10.46298/lmcs-17(4:21)2021
  * [13] Fokkink, W.J., Kamperman, J., Walters, P.: Within ARM’s reach: Compilation of left-linear rewrite systems via minimal rewrite systems. ACM Trans. Program. Lang. Syst. 20(3), 679–706 (1998). https://doi.org/10.1145/291889.291903, https://doi.org/10.1145/291889.291903
  * [14] Garavel, H., Tabikh, M., Arrada, I.: Benchmarking implementations of term rewriting and pattern matching in algebraic, functional, and object-oriented languages - the 4th rewrite engines competition. In: Rusu, V. (ed.) Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, Thessaloniki, Greece, June 14-15, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11152, pp. 1–25. Springer (2018). https://doi.org/10.1007/978-3-319-99840-4_1, https://doi.org/10.1007/978-3-319-99840-4_1
  * [15] Hoffmann, C.M., O’Donnell, M.J.: Interpreter generation using tree pattern matching. In: Aho, A.V., Zilles, S.N., Rosen, B.K. (eds.) Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, San Antonio, Texas, USA, January 1979. pp. 169–179. ACM Press (1979). https://doi.org/10.1145/567752.567768, https://doi.org/10.1145/567752.567768
  * [16] Hoffmann, C.M., O’Donnell, M.J.: Pattern matching in trees. J. ACM 29(1), 68–95 (1982). https://doi.org/10.1145/322290.322295, https://doi.org/10.1145/322290.322295
  * [17] Hondet, G., Blanqui, F.: The new rewriting engine of Dedukti (system description). In: Ariola, Z.M. (ed.) 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference). LIPIcs, vol. 167, pp. 35:1–35:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020). https://doi.org/10.4230/LIPIcs.FSCD.2020.35, https://doi.org/10.4230/LIPIcs.FSCD.2020.35
  * [18] Huet, G.P., Lévy, J.: Computations in orthogonal rewriting systems, II. In: Lassez, J., Plotkin, G.D. (eds.) Computational Logic - Essays in Honor of Alan Robinson. pp. 415–443. The MIT Press (1991)
  * [19] Jones, S.P.: Haskell 98 language and libraries: the revised report. Cambridge University Press (2003)
  * [20] O’Donnell, M.J.: Computing in Systems Described by Equations, Lecture Notes in Computer Science, vol. 58. Springer (1977). https://doi.org/10.1007/3-540-08531-9, https://doi.org/10.1007/3-540-08531-9
  * [21] Ogata, K., Futatsugi, K.: Implementation of term rewritings with the evaluation strategy. In: Glaser, H., Hartel, P.H., Kuchen, H. (eds.) Programming Languages: Implementations, Logics, and Programs, 9th International Symposium, PLILP’97, Including a Special Track on Declarative Programming Languages in Education, Southampton, UK, September 3-5, 1997, Proceedings. Lecture Notes in Computer Science, vol. 1292, pp. 225–239. Springer (1997). https://doi.org/10.1007/BFb0033847, https://doi.org/10.1007/BFb0033847
  * [22] van de Pol, J.: Just-in-time: On strategy annotations. Electron. Notes Theor. Comput. Sci. 57, 41–63 (2001). https://doi.org/10.1016/S1571-0661(04)00267-1, https://doi.org/10.1016/S1571-0661(04)00267-1
  * [23] Ramakrishnan, I.V., Sekar, R.C., Voronkov, A.: Term indexing. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 1853–1964. Elsevier and MIT Press (2001). https://doi.org/10.1016/b978-044450813-3/50028-x, https://doi.org/10.1016/b978-044450813-3/50028-x
  * [24] Sekar, R.C., Ramesh, R., Ramakrishnan, I.V.: Adaptive pattern matching. SIAM J. Comput. 24(6), 1207–1234 (1995). https://doi.org/10.1137/S0097539793246252, https://doi.org/10.1137/S0097539793246252
  * [25] Terese: Term rewriting systems, Cambridge tracts in theoretical computer science, vol. 55. Cambridge University Press (2003)
  * [26] Visser, E.: Stratego: A language for program transformation based on rewriting strategies system description of Stratego 0.5. In: Middeldorp, A. (ed.) Rewriting Techniques and Applications, 12th International Conference, RTA 2001, Utrecht, The Netherlands, May 22-24, 2001, Proceedings. Lecture Notes in Computer Science, vol. 2051, pp. 357–362. Springer (2001). https://doi.org/10.1007/3-540-45127-7_27, https://doi.org/10.1007/3-540-45127-7_27
  * [27] van Weerdenburg, M.: An account of implementing applicative term rewriting. Electronic Notes in Theoretical Computer Science 174(10), 139–155 (2007)
  * [28] de Wit, P.: Een systematische afleiding van een reductiemachine voor taalexperimenten. Master’s thesis, Eindhoven University of Technology, The Netherlands (1988)