Minimal adaptive pattern-matching automata for efficient term rewriting

Abstract

In term rewriting systems, pattern-matching is performed according to a prescribed traversal order. By adapting the traversal order to suit the patterns of the rewriting system, it is often possible to obtain better matching automata in the sense that they have a smaller size and allow term matching in shorter time, compared with the left-toright automaton. They may improve termination properties too. Space requirement is reduced further using a directed acyclic graph automaton that shares all the equivalent subautomata. This is done without altering either the matching time or termination properties. Isomorphic subautomata are duplicated in the tree-based automata. We discuss and develop an efficient approach to space requirement optimisation, matching time and termination properties improvement.