Adaptive Non-linear Pattern Matching Automata

TL;DR

This paper introduces an extension to adaptive pattern matching automata that integrates variable consistency checks, reducing the number of steps needed for pattern matching in term rewrite engines.

Contribution

It extends existing adaptive automata with combined consistency and pattern matching phases, improving efficiency in non-linear pattern matching.

Findings

Automata extension is correct and deterministic.

Reduction in matching steps demonstrated through examples.

Improved efficiency for non-linear pattern matching.

Abstract

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 automaton-based techniques are restricted to linear patterns, where each variable occurs at most once, and require an additional post-processing step to check so-called variable consistency. However, we can show that interleaving the variable consistency and pattern matching phases can reduce the number of required steps to find all matches. Therefore, we take the existing adaptive pattern matching automata as introduced by Sekar et al and extend these with consistency checks. We prove that the resulting deterministic pattern matching automaton is correct, and show several examples where some reduction can be achieved.