{'fraction_non_alphanumeric': 0.04291041056010847, 'fraction_numerical': 0.007816394488644294, 'mean_word_length': 4.241091023095413, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 7, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Term Rewriting Based On Set Automaton Matching

In previous work we have proposed an efficient pattern matching algorithm based on the notion of set automaton. In this article we investigate how set automata can be exploited to implement efficient term rewriting procedures. These procedures interleave pattern matching steps and rewriting steps and thus smoothly integrate redex discovery and subterm replacement. Concretely, we propose an optimised algorithm for outermost rewriting of left-linear term rewriting systems, prove its correctness, and present the results of some implementation experiments.


Introduction
Implementations of term rewriting [2] use efficient pattern matching algorithms to find redexes. They mostly use efficient root pattern matching algorithms, i.e. techniques that 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, can be inspected often when the same matching algorithm is called at a later point from a different root. 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. The original motivation for this research is to develop an optimal rewriter for state space generation in mCRL2 [6]. Over the years more complex rewrite systems have been generated from industrial specification languages. Typically these contain many complex rules as opposed to manually programmed rewrite systems. Additionally these rules may have arbitrary overlap, as opposed to functional programs.
The contribution of this paper is a rewriting procedure based on the set automaton pattern matching technique [12] which generalises the Aho-Corasick algorithm [1] to tree patterns. As a preprocessing step, a set automaton is constructed from the left-hand sides of a rewrite system. Intuitively it represents the matching process for that particular rewrite system, with the important benefit that in order to find all matches for a term, we need to inspect every function symbol only once. The rewriting procedure does not call the pattern matching function as a complex subroutine, but rather integrates pattern matching steps (single function symbol observations) and rewrite steps. We are not aware of any methods that explicitly and formally intertwine these two, even though this idea is not new and dates back to the 80s [15,16]. The rewriting procedure interleaves pattern matching steps with rewriting steps, and maintains a data structure of matching information and available redexes. Based on the available information, a strategy decides to continue searching for redexes (and where) or to rewrite using a previously found redex (and which one).
Our procedure roughly works as follows. Until the subterm term is in normal form, the given strategy selects a function symbol to match, or an available redex to reduce.
Upon inspecting a function symbol, we take transitions as prescribed by the set automaton, and store the successor configurations in a data structure. When every symbol of a pattern has been observed, the set automaton yields a match that is stored in a set of redexes.
Upon applying a rewrite step, we remove a part of the matching information that was stored thus far, and update the set of redexes accordingly. Termination of this procedure depends on the rewrite system and the strategy. The efficiency of rewriting depends on the strategy and the data structures that are used to store the matching information, the found redexes and the subject terms themselves. In Section 6 we discuss how the outermost rewriting strategy can be implemented efficiently by using a stack to store the matching information.
We also present benchmarks of a first implementation of the stack-based set automaton rewriter and compare it to the mCRL2 rewriter and our own implementation of an innermost rewriter with root pattern matching. In some instances outermost rewriting results in a much shorter rewriting path. In other cases, in the presence of rewrite rules that duplicate subterms, innermost rewriting is more effective. The set automaton is consistently faster than the innermost rewriter when the rewriting path has the same length, due to more efficient matching.
The main advantage of using set automata is that they inspect every symbol of a term only once by traversing the term from top to bottom. In tree automata theory it is well-known that top-down deterministic tree automata are not powerful enough to perform pattern matching [10]. There are three drawbacks to using set automata however. Just like set automaton matching, our rewriting procedure is limited by the assumption that the rewrite rules are left-linear (the left-hand sides do not contain repeating variables). Dropping this restriction is left as future work. The second drawback is the issue of look-ahead. In order to observe a symbol it could take d steps to reach it where d is the maximal depth of any pattern. Even though all symbols are observed once, the time complexity of matching a term with n symbols and m matches is O(dn + m). At this point we do not know how to reduce the complexity of matching to O(n + m). The last drawback is that set automata can be exponentially in the size of the rewrite system. In practice however, these automata are small. Moreover we expect that the cost of performing automaton construction as a pre-processing is well worth it if billions of terms must be rewritten using the same rewrite system.

Related work
The idea to use subterm matching for term rewriting and equational reasoning dates back to Hoffmann and O'Donnell [15,16]. In [11] some algorithms are described based on their ideas. Fokkink et al. transform left-linear rewrite systems into so-called minimal rewrite systems with only shallow patterns and right-hand sides [13]. These minimal rewrite systems are then compiled into instructions for an abstract rewriting machine, which uses an innermost rewriting strategy. The transformation on the right-hand sides of the rules is based on one of Hoffmann and O'Donnell's algorithms [16]. In our algorithms we do not transform the rewrite system.
Existing rewrite engines [14] use root pattern matching techniques. Maude, the fastest rewrite engine among the algebraic tools of REC 2018, deploys solutions to several kinds of automata-based pattern matching problems [8]. In particular it uses discrimination nets [7]. An overview of root pattern matching techniques is given in [20].
In functional languages like Haskell [17] and Clean [4] algebraic data types are specified with constructor function symbols which 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 and rewriting is fast, Since our target language is algebraic, we make no distinction between constructors and function-defining symbols, and pose no restrictions like orthogonality.

Structure of the paper
In Section 2 we present some preliminary definitions. In Section 3 we recall the set automaton matching technique from [12]. Then we discuss a basic version of the rewriting procedure based on this matching technique in Section 4. This basic version is shown to correctly implement term rewriting. This algorithm is inefficient since all matching information is forgotten after a rewrite step. In Section 5 we give an improved version that saves some of the matching information upon a rewrite step, and this optimisation is also shown to correctly implement term rewriting. Section 6 presents an implementation that uses a stack to save the rewriting information. We show that this algorithm always performs outermost rewrite steps. Section 7 presents benchmarks on an implementation of the stack-based set automaton rewriter. In Section 8 we present some ideas for further improvements of the technique that we intend to explore in the future.
Sections 9 and 10 appear in this online technical report only. Section 9 covers the construction of a set automaton. The details are mostly copied from [12], but we added additional explanations and most importantly, a method to create a set automaton that enables outermost pattern matching. Section 10 includes a proof of this method.

Preliminaries
A signature is a pair (F, V) where F is finite sequence of disjoint, finite sets of function symbols F 0 , F 1 , . . . , F n where F i consists of function symbols of arity i, and V is a set of variables. We denote the arity of f by #f . The set of constants is F 0 , the entire signature is defined by F = n i=0 F i and the set of non-constants is defined by be the set of terms over signature (F, V), defined as the smallest set such that V ⊆ T(F, V) and F 0 ⊆ T(F, V), and for all f ∈ F >0 , whenever t 1 , . . . , t #f ∈ T(F, V), then f (t 1 , . . . , t #f ) ∈ T(F, V). We write T(F) instead of T(F, ∅) to denote the set of ground terms.
A position is a list of positive natural numbers. We use P to denote the set of all positions and we use to denote the empty list; it is referred to as the root position. Given two positions p, q their concatenation is denoted by p.q. The root position acts as a unit element with respect to concatenation. Given a set X and some A ⊆ X × P, define the positions of A by pos(A) = {p ∈ P | ∃x : (x, p) ∈ A}. We often denote a pair (x, p) in X × P by x@p. The term domain function D : T(F, V) → P(P) maps a term to the set of positions on which it has function symbols or variables. That is, for x ∈ V we have 23:4

Term Rewriting Based On Set Automaton Matching
Technical report D(x) = , for all a ∈ F 0 we have D(a) = , and for all f ∈ F n with n > 0 we have Given a term t and a position p ∈ D(t), A pattern over the signature (F, V) is a term ∈ T(F, V) \ V. Said pattern is linear if no variable occurs more than once in . Denote the head symbol of a pattern by hd(t). A linear pattern matches term t on position p iff for all p ∈ D( ) with [p ] / ∈ V, we have that A rewrite rule is a pattern paired with a term r such that all variables of r occur in as well. A term rewrite system (TRS) is a finite, non-empty set of rewrite rules. A redex of t is a rule → r and a position p such that matches t at position p. Such a redex is often denoted by → r@p.
A context is a term with a single occurence of the hole in it. Given a context C and a term t, the term C[t] is obtained by replacing the hole in C by t.
A substitution is a mapping from V to T(F, V). A ground substitution is a mapping from V to T(F). Term t rewrites to term t by rule → r on position p, denoted by t →r@p −−−−→ t , if and only if there is a context C with a hole on position p, and a substitution σ such that t = C[ σ ] and t = C[r σ ]. We write t → t iff t rewrites to t by some rule on some position. The transitive reflexive closure of → is denoted by → * . A term t is in normal form iff t has no redexes. Given a rule → r and a term t such that matches t at position p, we denote by t[ → r@p] the unique term t such that t →r@p −−−−→ t .

Set automata
We recall set automata from [12]. Space limitations prevent us from recalling and explaining the construction of such an automaton in this article. The reader who is interested in the construction may find it in [12]. In this section we only explain what a set automaton is, how it is used and which properties are necessary for our term rewriting algorithms. Set automata can be seen as a generalisation of Aho and Corasick's string matching automata [1]. They prescribe how to search for patterns in a term 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. Formally a set automaton for the TRS R over the signature (F, V) is a tuple (S, s 0 , L, δ, η) where S is a finite set of states; s 0 ∈ S is the initial state; L : S → P is a state labelling function; δ : S × F → P(S × P) is a transition function; η : S × F → P(R × P) is an output function.
Example 1. Consider the rewrite system R if given by the five rules In Figure 1 there is a graphical presentation of the set automaton generated for this rewrite system. There are three states s 0 , s 1    Generally the set automaton construction algorithm has some choices as to which state label to assign to a state. This influences the automaton size and the order in which we traverse terms. Thus there are multiple set automata that can be constructed for a rewrite system R. For this paper we simply assume the availability of any set automaton, henceforth referred to as a set automaton generated from R.
We informally describe how a set automaton can be used to find redexes in a ground term t. The process consists of traversing through a term, using the set automaton to determine the next position(s) to inspect, and keeping track of whether redexes have been found. To this end, a set of configurations -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). Formally this is the symbol f = hd(t[p.L(s)]). Then we compute the successor configurations and the output as follows.
The successors are given as pairs by δ(s, f ). For all successors (s , q) ∈ δ(s, f ) obtained from configuration (s, p) we add a new configuration (s , p.q) to the configuration set. The output pattern matches are given as pairs by η(s, f ). When (R, q) ∈ η(s, f ) is given as output from configuration (s, p) then there is a match for rule R at position p.q. In all of our examples the position q is just , but in case one pattern is a subpattern of another, then q may be deeper. The positions in the configuration set should be considered absolute positions that also occur in the term under consideration. The positions in the automaton should be regarded relative to some absolute position.

Example 2.
Consider the term t = if (not(not(true)), f alse, true). Table 1  At every stage of the exploration, a configuration from the set should be chosen and removed, and the successors must be added to the set. Term t has two redexes, which are given as an output in the third and fourth column.

Configuration trees
For the purpose of pattern matching it suffices to keep unexplored configurations in a set. Upon exploring one configuration, it is removed and the successors are added to the C V I T 2 0 1 6 23:6  Table 1 The traversal of if (not(not(true)), f alse, true) with the set automaton from Figure 1.
configuration set. For the purpose of our rewriting procedures we add structure, and organise the exploration of the term in a tree.
An unexplored configuration appears as a B-labelled pair 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 N-labelled triple N(s, p, cts) called a node. The component cts of a node is a set of successor trees; when the node is created by growing a bud, it consists of buds, one for every successor state given by δ(s, f ). If there are no successor states given by δ(s, f ) then cts is empty. Hence the trees B(s, p) and N(s, p, ∅) 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 CT is defined as the smallest set such that a bud B(s, p) is a configuration tree for every configuration (s, p), and given a finite, possibly empty, set of children cts ⊆ CT and a configuration (s, p), the node N(s, p, cts) is also a configuration tree.
Define the node configurations of a CT recursively by Define the abbreviation completed(t) = completed(s 0 , , t). The following theorem explains what the completed CT of a term is. Its proof can be found in [12].
Thus, a completed configuration tree is simply a one-to-one correspondence between configurations and the function symbols of a term, assigned to it by a set automaton. This correspondence suffices to find every redex in a term as follows. In a configuration (s, p) the function symbol f = hd(t[p.L(s)]) yields some matches as prescribed by η(s, f ). Define the discovered matches of a configuration (s, p) and the observed symbol f by The following theorem from [12] states the correctness claim for pattern matching.

Forgetful rewriting
We define a basic rewriting procedure that uses set automaton matching to explore the completed configuration tree step by step. After a rewrite step, the entire CT is forgotten and matching has to start again from B(s 0 , ). In the next section we show how a part of the configuration tree can be retained. Theorem 4 gives rise to a matching algorithm: compute the completed configuration tree of t and harvest all redexes after observing a function symbol. However, when rewriting a term to normal form, it is not necessary to match the entire term. A pattern match for the rule mult(0, x) → 0 should immediately be used to yield a rewrite to 0; it would be inefficient to continue matching x. Configuration trees give us the necessary control over the matching process so that it may be interleaved with the rewriting process.
Define the growth of a configuration tree ct after inspecting symbol f in configuration (s, p) by Intuitively grow(ct, s, p, f ) replaces every bud B(s, p) by a node with the same configuration. The successors of this node are new buds. When matching a part of a complete configuration tree, this bud is unique due to Theorem 3. Algorithm 1 interleaves matching steps by means of grow, with applying rewrite steps to found redexes, using an arbitrary strategy. It maintains a set of found redexes, and a CT. The strategy determines whether to reduce a found redex, or to continue matching a bud in the current CT. Formally a strategy is a partial mapping select : CT ×P(R×P) (S ×P)∪(R×P) such that select(ct, reds) ∈ buds(ct) ∪ reds, for all pairs (ct, reds) such that buds(ct) ∪ reds is non-empty. Note that strategies are only partial in the sense that they are undefined on budless CTs paired with empty redex sets.
If the strategy selects a bud B(s, p), the algorithm inspects the head symbol of term t[p.L(s)]. Then the bud B(s, p) is replaced according to the grow function specified above. After growing the configuration tree, newly found redexes are added to the redex set according to the matches function. Otherwise if the strategy selects a redex → r@p, then all redexes are forgotten, the CT is reset to B(s 0 , ), and the term is rewritten to t[ → r@p].
Example 5. We rewrite the term t 0 = if (not(not(true)), f alse, true) of Example 2 by using an outermost strategy. To this end we match if at position , then not@1 and then not@1.1, at which point the set automaton yields redex not(not(x)) → x@1. The configuration trees of this sequence is displayed in Figure 2. Then we apply the rewrite, leading to t = if (true, f alse, true), the configuration tree is reset to B(s 0 , ), and the redex set is emptied again.
After this step we observe if at position , we observe true at position 1 and receive the redex if (true, x, y) → x@ . Applying the rewrite to yields t = true, the configuration tree is reset to B(s 0 , ), and the redex set is emptied again.

23:8 Term Rewriting Based On Set Automaton Matching
Technical report Algorithm 1 A rewriting algorithm based on set automaton matching, that forgets all information about matching after every rewrite step. We assume the availability of a set automaton (S, s0, L, δ, η) constructed for the rewrite system at hand. while buds(ct) = ∅ ∨ reds = ∅ do 6: action := select(ct, reds) 7: if action is a configuration (s, p) then Match the symbol else if action is a redex → r@p ∈ reds then Apply the reduction reds After this step, the set automaton matches true at position resulting in the configuration tree N(s 0 , , ∅). This CT has no buds and the redex set is empty, so the rewriting procedure yields true as a normal form.

Correctness
We prove a partial correctness claim about Algorithm 1, in the sense that it 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. In the next section we give an optimisation and prove its correctness using the same invariant. First we need some formalities on configuration trees.
The 'is fragment of' relation on CT is the smallest relation such that B(s, p) B(s, p) and B(s, p) N(s, p, cts) and N(s, p, cts) N(s, p, cts ) if and only if there is a bijection ϕ : cts → cts such that ct ϕ(ct) for all ct ∈ cts. This definition makes CT , a partial ordering. Intuitively we have ct 1 ct 2 whenever we can change ct 1 into ct 2 by means of zero or more applications of grow. In particular we are interested in fragments of completed CTs. Proposition 6. If ct completed(t) then grow(ct, s, p, hd(t[p.L(s)])) completed(t) for all (s, p) ∈ confs(completed(t)).

Lemma 7.
Let t 0 be a ground term. Then the following invariant on the variables t, ct and reds given by For invariant maintenance, consider t, ct and reds such that they satisfy the invariant. Suppose that buds(ct) ∪ reds = ∅. We distinguish two cases.
Suppose that select(ct, reds) = (s, p), some bud configuration in buds(ct), and let f = hd(t[p.L(s)]). Since t is not changed in this branch of the if-statement, t 0 → * t holds by assumption. Moreover grow(ct, s, p, f ) completed(t) by Lemma 6. Conclude by the calculation: Otherwise suppose that select(ct, reds) = → r@p, some redex in reds. By assumption t 0 → * t. By ct completed(t) and Theorem 4 it follows that → r@p is a redex of t.
Lastly ct and reds are reset to their initial values which satisfy the invariant as already shown. Lemma 7 states that Algorithm 1 keeps producing valid rewrite steps. Of course, termination depends on the rewrite system and the strategy, which we have abstracted from so far and will remain to do so until later sections. We conclude this section with the corollary of partial correctness.
Proof. Suppose that the algorithm terminates with the values t, ct and reds. By Lemma 7 the invariant is satisfied. By termination, buds(ct) = ∅ and reds = ∅. Since ct has no buds, ct = completed(t). By Theorem 4 and reds = ∅ there are no redexes in t. To conclude, we have that t 0 → * t, hence t is a normal form of t 0 .

5
Rewriting by pruning Technical report automaton inspects the input term in a top-down fashion, there must also be a configuration in ct where position p was inspected. We call this the initialisation configuration for redex → r@p, more precisely, the configuration (s i , p i ) such that p i .L(s i ) = p. Upon applying the rewrite step t[ → r@p], only the subterm at position p changes. Any matching that was not done below position p is therefore still valid. So it suffices to prune the configuration tree up to the initialisation configuration of the used redex. Define prune (B(s, p), q) = B(s, p) and prune (N(s, p, cts) Given ct, denote by ct[p] the 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 CT, then ct[p] is unique by Theorem 3.
Algorithm 2 improves upon the forgetful rewriter by deploying prune. Before applying a rewrite step we prune up to the initialisation configuration of the selected redex, and we remove the redexes that were obtained in the pruned part of the CT.
Algorithm 2 A rewriting algorithm that remembers part of the matching information by pruning a part of the configuration tree. We assume the availability of a set automaton (S, s0, L, δ, η) constructed for the rewrite system at hand.

Correctness
We prove partial correctness of Algorithm 2 by using the same invariant as in Lemma 7. To this end we only have to show that the invariant is maintained in the else-branch of the algorithm, which solely relies on the following properties of prune. Proof. We extend the proof of Lemma 7. Consider t, ct and reds such that they satisfy the invariant, and suppose that select(ct, reds) = → r@p, some redex in reds. Let Since → r@p is a redex of t and t 0 → t we have t 0 → t as needed. Next we show that prune(ct, p) completed(t ). By assumption ct completed(t). Then: by Lemma 10, monotonicity Therefore reds = {matches(s, q, hd(t[q.L(s)])) | (s, q) ∈ nodes(prune(ct, p))} as needed.

Outermost rewriting with a stack
The two algorithms established so far are correct and maintain minimal overhead due to the efficiency of matching. In the end, the efficiency heavily depends on the strategy and the data structures that are used to implement the configuration tree and redex set. A strategy should make decisions based on the available match positions and redexes, but the time spent making such decisions should not defeat the purpose of efficiency. Searching through a big configuration tree and a set of redexes could be too expensive.
We define an instance of the pruning rewriter that implements a depth-first search through the configuration tree, and enforces an outermost rewrite strategy. This instance can be implemented by using a configuration stack: a stack of lists of configurations. Formally, stacks and lists are the same thing, but to avoid confusion we refer to the stack as the main data structure whereas the lists of configurations are elements on the stack. Algorithm 3 is C V I T 2 0 1 6

23:12 Term Rewriting Based On Set Automaton Matching
Technical report Algorithm 3 A rewriting algorithm that represents the configuration tree as a stack. We assume the availability of a set automaton (S, s0, L, δ, η) constructed for the rewrite system at hand, with the additional property that δ yields an ordered list such that if δ(s, f ) has an outermost pair, then it is the head of this list. while cs is not the singleton stack with the empty list do 10: if top(cs) is the empty list then 11: cs := pop(cs) StackPrune(p.q, cs) return t the stack-based version of the pruning rewriter. We use the notation (s, p) ls to represent a non-empty configuration list with head (s, p) and tail ls.
Since a depth-first search through a tree by using a stack is a standard programming technique, we only explain the most important differences with Algorithm 2. Firstly, no redex set is maintained. Instead we apply a rewrite step immediately when the set automaton reports a redex. Secondly, similar to the function prune from Section 5, the function StackPrune pops the configuration stack until the initialisation configuration appears as the head of the list on top of the stack. Lastly, we assume that the set automaton is tailored to find outermost matches first. This requires a subtle change in the set automaton construction algorithm which is not described in [12]. Due to space limitations we cannot establish this result here either. The interested reader may find it in the technical report of this paper [3]. The technical corollary is as follows. This result ensures that Algorithm 3 performs outermost rewrite steps, unless there are rules such as R1 : g(h(a)) → a and R2 : h(x) → x. Any top-down traversal of a term will find pattern matches for h(x) before finding a match for R1. Therefore the stack rewriting procedure can rewrite subterms that overlap with outermost redexes. This issue can be mitigated by an adaptation that maintains a small set of redexes, and does not apply the rewrite steps until these redexes are guaranteed to be outermost.

Implementation
As a proof of concept, we have implemented the set automaton construction and stack-based rewriter in the Rust programming language. For comparison we have also implemented two innermost rewriters: one using Adaptive Pattern Matching Automata from [21] and one using a naive matching algorithm (check every pattern with the observed head symbol one by one). All rewriters use maximal subterm sharing, which allows compact representation of terms and cheap term duplication. The set automaton based rewriter also maximally shares prefixes of positions. The implementation of the configuration stack does not actually store lists of configurations (as explained in the previous section). Instead, it stores the configuration currently being explored and a pointer to the remaining set automaton transitions that would lead to the rest of the configurations in the list. All rewriters make no heap allocations (after initialisation). The binaries, along with instructions on how to replicate our benchmarking results are available on Zenodo 2 . To compare our three rewriters we have used five of the benchmarks from REC 2018 [14], restricting ourselves to benchmarks without conditional rewrite rules: Fibonacci, Factorial and three tautologies. The tautology benchmarks contain rules that duplicate subterms. We added a variant with alternative rewrite rules that do not duplicate subterms. To highlight cases where the set automaton has an advantage over innermost rewriters we have added two more benchmarks: a string matching benchmark which contains twenty large overlapping patterns and an alternative factorial benchmark in which the inequality 3 > 5! is evaluated.
The results of benchmarking can be found in Table 2. The set automaton is comparatively slow when outermost rewriting causes a longer rewriting path due to subterm duplication (factorial and tautologies with duplicating rules). Conversely, the set automaton is comparatively fast when outermost rewriting causes a shorter rewriting path (factorial comparison and tautologies without duplicating rules). The shorter rewriting path is caused by rewrite rules that allow deletion of subterms (without even needing to inspect those subterms), e.g. f alse =⇒ P → true. When innermost and outermost rewriting do not differ with respect to the rewriting path, the set automaton is slightly (Fibonacci) or much (String matching) quicker, depending on the number of the symbols in the patterns and their overlap.
Nesting logical connectives with rewrite rules that duplicate subterms will result in an outermost rewrite path that is exponential in the number of logical connectives of the original term. The innermost rewriting path on the other hand will scale linearly. To test whether the set automaton is also exponentially slower in the factorial benchmark we gathered statistics for 1! up to 9!, see Figure 3. The outermost rewrite path turns out to scale approximately linearly worse compared to the innermost rewrite path. Time performance scales linearly worse up to 6!, after which it plateaus. We conjecture that after some point both rewriters have so many terms in the term pool that most data is no longer stored in CPU caches, making fetching data from RAM the bottleneck.
In order to also compare our work to existing rewrite engines we compare with mCRL2. mCRL2 feautures two rewrites: jitty and jittyc, the latter of which generates and compiles C++ code specific to the rewrite system. We use the Fibonacci benchmark, modified to compute the 32nd Fibonacci number, as it computationally intense enough to collect reliable measurements of mCRL2. The results are listed in Table 3.
The proof of concept implementation of the set automaton is not yet competitive with existing tools. Profiling the stack-based rewriter on the Fibonacci benchmark reveals that 85% of the time is spent in the maximally shared term storage, finding and inserting terms. We reckon that our implementation could be heavily improved, even without adapting the set automaton, by adopting optimizations from other rewrite engines.

Discussion and future work
With a formal foundation and a generic description of rewriting with strategies, we described a proof of concept for rewriting based on set automata. This leaves open many possibilities for optimisation. First off, the structure of the right-hand sides is not used in our procedures. A theoretical optimisation is to precompile the configuration tree fragments that arise from the right-hand side. This fragment depends on state of the configuration where we pruned to, and should be attached to said pruning point. This optimisation ensures that we do not have to match the function symbols of the right-hand side after subterm replacement.
Building upon this optimisation, 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≤i≤n , How do we compute t n efficiently, without necessarily computing every intermediate t i ? Seeing as most of the time is spent executing rewrite steps, it might be beneficial to investigate this problem.
In this paper we did not discuss data structures and storage of terms. In order to compare set automaton rewriting with competitive tools, the first step is to improve the maximally shared term storage, by either designing something ourselves, adapting existing techniques or using existing libraries (such as the ATerm library [24], which is used by mCRL2).
Of the solutions that exist for subterm pattern matching, we chose set automata because they match a term in a top-down fashion, and because of their configuration tree semantics. Other solutions like Hoffmann and O'Donnell's top-down algorithm [16] and the similar tree automata by Cleophas et al. [9] collect stringpath matches that must be merged during the matching/rewriting operation, hence these solutions are a reduction to string matching. This overhead makes it more difficult to create a rewriting algorithm, but in theory these could also be used to maintain matching information.
Our benchmarks revealed that there is a great performance difference between rewriting strategies. We intend to research better strategies that, for example, avoid duplicating subterms that are not yet in normal form. Rewriting strategies have been subjected to C V I T 2 0 1 6

23:16 Term Rewriting Based On Set Automaton Matching
Technical report extensive study, both of practical and theoretical nature [18,19,22,23]. Strategies are usually defined as functions that yield a reduction path for a term, or as subsets of the rewrite relation → * . The works that focus on strategies typically abstract from the fact that pattern matching is a non-trivial algorithmic problem. To achieve an optimised implementation we need to integrate the existing work on strategies with our methods. We expect that every strategy needs suitable data structures to efficiently decide which step to take next.

Set automaton construction
This section only appears in this technical report. It is supplementary material to the corresponding FSCD 2022 submission, and covers: set automaton construction, largely copied from [12], with extended explanations; an additional set automaton construction parameter that gives a degree of freedom on how to partition derivatives; an instance of this parameter, the outermost preserving dependency relation, which is used to build a set automaton that guarantees outermost pattern matching. In the next Section 10 we discuss a proof that enables us to do efficient outermost pattern matching.
The following additional definitions are necessary to follow the construction. Since we only deal with linear patterns and no rewriting in this section, we only consider one variable C V I T 2 0 1 6

23:18 Term Rewriting Based On Set Automaton Matching
Technical report ω which behaves as a don't care symbol. The subpatterns of a pattern are given by sub( ) = { [p] | p ∈ D( ) ∧ [p] = ω}. This function is extended to sets of patterns L by sub(L) = ∈L sub( ). Lastly, a position p is below position q, denoted p ≤ q, iff there is a position r such that p.r = q.

The information described by states
Recall the formal set automaton definition of Section 3. We describe how a set automaton is constructed from a pattern set L by creating 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, which is given as follows. The sets of match obligations MO and match announcements MA are respectively defined by A match goal is a match obligation paired with a match announcement, i.e. a pair in MO ×MA.
To limit the amount of parentheses, we denote a match goal ({( 1 , p 1 ), . . . , ( n , p n )}, ( @p)) by writing 1 @p 1 , . . . , n @p n → @p. Such a match goal should be read as: "in order to announce a match for pattern at position p, we are obliged to observe the (sub)pattern i on position p i , for all 1 ≤ i ≤ n". We identify states with non-empty sets of match goals, i.e. S = P(MO × MA) \ {∅}. This encoding formally captures the idea that all states carry every pattern that still needs to be seen whenever we arrive in this state during the matching process.
State s 1 can be reached by following the f -transition from the initial state, and has three match goals. The first goal f (ω, g(ω))@1, g(ω)@2 → @ is obtained by reducing the match obligation of s 0 to f (ω, g(ω))@1, g(ω)@2. The top symbol f has already been inspected; therefore the subpatterns f (ω, g(ω)) and g(ω) should still be observed in order to yield a pattern match. Furthermore there are the goals f (f (ω, g(ω)), g(ω))@1 → f (f (ω, g(ω)), g(ω))@1, and f (f (ω, g(ω)), g(ω))@2 → f (f (ω, g(ω)), g(ω))@2. In addition to the reduced goal, 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 special status. A match goal of the form @p → @p is called fresh. It represents that we aim to find a pattern match for on position p, but we have not observed any function symbols of that pattern yet. A match goal of the form mo → @ is called a root goal. It represents that when we are looking for matches from a configuration (s, p), the output will be yielded on position p. , which is just position p.

Initial state
Consider a non-empty pattern set L. We start the construction of a set automaton for L from the initial state, and compute the transitions 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 g f (ω, g(ω))@1, g(ω)@2 → ℓ@ǫ f (f (ω, g(ω)), g(ω))@1 → ℓ@1 f (f (ω, g(ω)), g(ω))@2 → ℓ@2 2 s1 f (f (ω, g(ω)), g(ω))@ǫ → ℓ@ǫ ǫ s0 state encoding, the initial state is formally defined by In other words, the initial state contains exactly every fresh root goal. Furthermore, the initial state is labelled with the empty position, formally L(s 0 ) = .

Transitions
From a state s we define its outgoing transition δ(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 Figure 4 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 Figure 4 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.

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 ≤ i ≤ #f .

Technical report
Consider a match goal 1 @p 1 , . . . , n @p n → @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 1 = f (ω, . . . , ω) then f @p i is the last observation that was needed to complete the match goal. Then @p is recorded in the output function of the automaton and the match goal disappears.
If hd( i ) = f then there is a mismatch; the observation f @p i leads to the conclusion that this pattern cannot match. Then the match obligation is discarded.
Otherwise i = f (t 1 , . . . , t #f ) but the match goal is not completed yet. Then the other pairs j @p j with i = j remain unchanged, the pair i @p i is removed from the obligation and for all j such that t j = ω we add the pair t j @p i .j to the obligation of this goal, Formally, reducing a match obligation is captured by the mapping reduce : Using the mapping reduce, we can define the f -derivative of state s by

Derivative partitioning
One application of deriv creates new match goals and new positions represented by longer list of indices. Repeated application of 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 some equivalence relation on match goals. In the original work [12] we only gave one equivalence relation, namely indirect dependency. In this technical report we provide another relation, namely outermost preserving dependency. We first explain indirect dependency.

Dependency due to overlapping match obligation positions
Note from Example 14 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 → 1 @p 1 and g 2 = mo 2 → 2 @p 2 by g 1 R dep g 2 if, and only if, pos(mo 1 ) ∩ pos(mo 2 ) = ∅ .
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 we have pos(mo 1 ) ∩ pos(mo 2 ) = {1} and pos(mo 2 ) ∩ pos(mo 3 ) = {2}, but pos(mo 1 ) ∩ pos(mo 3 ) = ∅. To obtain an equivalence we simply consider the transitive closure R * dep , which we refer to as (indirect) dependency.
We partition deriv(s, f ) into equivalence classes with respect to dependency R * dep . Each equivalence class then corresponds to a new state. The set of equivalence classes of the derivative is denoted by [deriv(s, f )] R * dep . We use the letter K to range over equivalence classes.

Dependency due to comparable match obligation positions
Relation R * dep ensures that goals with overlapping match obligation positions stay together. This ensures that the resulting set automaton can be used for efficient matching in the sense that no symbol is observed twice. We provide a coarser dependency relation that also relates goals that have comparable match announcement positions. By using this relation for partitioning, we always find outermost matches first. Given a state s, define the direct outermost preserving dependency relation R op for all goals g 1 = mo 1 → 1 @p 1 and g 2 = mo 2 → 2 @p 2 by In Example 19 we explain that R * op yields a different automaton, and why this may be desirable in some cases.

Lifting the positions of classes
Partitioning into smaller states is not enough to obtain a finite state machine since the positions of match goals are increasing. As the last part of the construction, we shorten C V I T 2 0 1 6 the positions of every equivalence class. This can be done due to the following observation. Suppose that we are looking at term t on position . If all match goals say something about position 1 or lower, we can remove the prefix 1 everywhere, and start to look at term t from position 1. Inspecting position 1.p from the root is the same as inspecting p from position 1.
Let pos 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 pos MA (K). To ease the notation we write gcp(K) instead of gcp(pos MA (K)). Since all positions in a state are of the form gcp(K).p , we can replace them by p . Define lift(s) by lift(s) = {(lift(mo), @p ) | (mo, @gcp(s).p ) ∈ s} where lift(mo) = { @p | @gcp(s).p ∈ mo}.
This concludes the construction of the transition relation. For a state s and a function symbol f , we fix δ(s, f ) = {(lift(K), gcp(K)) | K ∈ [deriv(s, f )] ∼ }. Note that gcp(K) is also recorded in each transition since it tells us how to traverse the term.
Example 17. Continuing in Example 15, we compute the greatest common prefix and corresponding transition for the two equivalence classes. For K 1 we have gcp(K 1 ) = gcp({1, }) = .

Output patterns
The output patterns after an f -transition are simply the match announcements that accompany the match obligations that reduce to ∅: η(s, f ) = {ma ∈ MA | f (ω, . . . , ω)@L(s) → ma ∈ s} .

State labels
For every state s there must be a position label L(s) in order to construct the transitions from s. It makes sense to only choose a position from one of the match obligations. 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 [12]. Similar to Adaptive Pattern Matching Automata [21], 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.

Construction summary
To formalise the decisions that can be made during set automaton construction, we need a state label selection function sel : S → P such that sel(s) ∈ pos(mo) for some root goal mo → ma ∈ s, and we need a dependency relation ∼ that forms an equivalence on the goals of every state. We provided two dependency relations R * dep and R * op that are both suitable candidates for ∼. A simple state space generation algorithm then yields a set automaton (S, s 0 , L, δ, η) such that: S is the set of all reachable states;

Outermost pattern matching
In Section 6 we claimed that a set automaton constructed with the outermost preserving dependency relation can be used to prioritise the search for outermost redexes when using the stack rewriter.
Example 19. Consider the associativity patterns 1 = f (f (ω, ω), ω) and 2 = f (ω, f (ω, ω)), and suppose that F 0 = {a}, F 1 = {g} and F 2 = {f }. In Figure 5 there is a set automaton created for these patterns by using R * dep , and the automaton in Figure 6 is obtained by using R * op . In Figure 6 not all transitions are displayed. Consider the term t = f (g (G), f (a, a)) where G is a big term. There is an outermost match for 1 at position . Depending on the traversal, the automaton in Figure 5 may first match g. After the observation of f at position , there is a degree of freedom as to whether we explore configuration (s 1 , ) or (s 2 , ). Since algorithm 3 performs a depth-first search on terms, choosing (s 1 , ) is a commitment that results in rewriting g(G). Any redex in G will not be outermost.
We prevent this problem by matching term t with the automaton in Figure 6 instead. After observing f at position , we observe g at position 1 in state s 1 and we move to s 4 .
Example 19 shows that the dependency relation R * dep yields an unsuitable automaton for the stack rewriter if we want to prioritise outermost rewriting. After an f -transition from any state, it is impossible to locally determine the successor that yields an outermost redex. By partitioning with the outermost preserving dependency relation we prevent this problem. In this section we show that R * op is coarser than R * dep , and we show that a depth-first search on the configuration tree indeed yields outermost redexes.
pos(mo 1 ) ∩ pos(mo 2 ). By construction we have that q ≤ p 1 and q ≤ p 2 , by which p 1 ≤ p 2 or p 2 ≤ p 1 . Hence g 1 R * op g 2 and therefore g 1 and g 2 end up in the same equivalence class of [deriv(s, f )] R * op . Lemma 21. Consider a set automaton generated with R * op and let t be a ground term. Let N(s, p, cts) be a subtree of completed(t) and suppose that ct 1 , ct 2 ∈ cts are distinct configuration trees with ct 1 = N(s 1 , p.p 1 , cts 1 ) and ct 2 = N(s 2 , p.p 2 , cts 2 ) and p 1 ≥ p 2 . Then there are no two configurations (s 1 , p.p 1 .p 1 ) ∈ nodes(ct 1 ) and (s 2 , p.p 2 .p 2 ) ∈ nodes(ct 2 ), with matches