Maurice Laveaux: Adaptive Non-linear Pattern Match Automata

Event Details

Efficient pattern matching is fundamental for practical term rewrite engines. By preprocessing the given patterns into a finite deterministic automaton the matching patterns can be decided in a single traversal of the relevant parts of the input term. Most of the existing automaton based techniques are restricted to linear patterns, where each variable occurs at most once, and require an additional post-processing step to check variable consistency. However, interleaving the variable consistency and pattern matching phases can reduce the number of steps required to find a match. Therefore, we introduce consistency automata to determine variable consistency using an optimal number of comparisons. These consistency automata are then combined with existing so-called adaptive pattern match automata as introduced by Sekar et al. We show that the resulting automata can solve the pattern matching problem correctly, and more efficiently then existing approaches.