Rick Erkens: Optimizing Term Rewriting with Creeper Trace Transducers

Event Details

In a previous talk I discussed our work on algorithms for optimized term normalization. We use a so-called set automaton to find pattern matches efficiently, and upon discovering a reducible subterm we apply the reduction while preserving as much matching information as possible. By integrating the structure of the right-hand sides into the automaton, we can discover a new reducible subterm immediately, and extract a trace of rewrite steps that can be executed in succession without actually executing the steps. In this talk I will discuss a way to exploit this free information by focusing on a subset of traces. From a rewrite system we construct a so-called creeper trace transducer, which reads a creeper trace while producing the term obtained after executing the steps in the trace. The transducer skips overlapping symbols between each pair of subsequent rules, and in some cases a part of the trace can be disregarded altogether.