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 a match all matches. Therefore, we take the existing adaptive pattern matching automata as introduced by Sekar et al and extend it these with consistency checks. We prove that the resulting deterministic pattern matching automaton is correct, and show that its evaluation depth is can be shorter than two-phase approaches.
Original language | English |
---|---|
Title of host publication | 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020) |
Editors | Zena M. Ariola |
Publisher | Schloss Dagstuhl - Leibniz-Zentrum für Informatik |
Number of pages | 21 |
ISBN (Electronic) | 978-3-95977-155-9 |
DOIs | |
Publication status | Published - 28 Jun 2020 |
Event | International Conference on Formal Structures for Computation and Deduction - Virtual, Paris, France Duration: 29 Jun 2020 → 5 Jul 2020 https://fscd2020.org/ |
Publication series
Name | Leibniz International Proceedings in Informatics (LIPIcs) |
---|---|
Volume | 167 |
ISSN (Electronic) | 1868-8969 |
Conference
Conference | International Conference on Formal Structures for Computation and Deduction |
---|---|
Abbreviated title | FSCD |
Country/Territory | France |
City | Paris |
Period | 29/06/20 → 5/07/20 |
Internet address |
Keywords
- Pattern matching
- Term indexing
- Tree automata