Adaptive Non-Linear Pattern Matching Automata

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review


    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 languageEnglish
    Title of host publication5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
    EditorsZena M. Ariola
    PublisherSchloss Dagstuhl - Leibniz-Zentrum für Informatik
    Number of pages21
    ISBN (Electronic)978-3-95977-155-9
    Publication statusPublished - 28 Jun 2020
    EventInternational Conference on Formal Structures for Computation and Deduction - Virtual, Paris, France
    Duration: 29 Jun 20205 Jul 2020

    Publication series

    NameLeibniz International Proceedings in Informatics (LIPIcs)
    ISSN (Electronic)1868-8969


    ConferenceInternational Conference on Formal Structures for Computation and Deduction
    Abbreviated titleFSCD
    Internet address


    • Pattern matching
    • Term indexing
    • Tree automata


    Dive into the research topics of 'Adaptive Non-Linear Pattern Matching Automata'. Together they form a unique fingerprint.

    Cite this