Adaptive Non-Linear Pattern Matching Automata

Authors Rick Erkens, Maurice Laveaux

Thumbnail PDF


  • Filesize: 0.64 MB
  • 21 pages

Document Identifiers

Author Details

Rick Erkens
  • Eindhoven University of Technology, The Netherlands
Maurice Laveaux
  • Eindhoven University of Technology, The Netherlands


We would like to thank Jan Friso Groote, Bas Luttik and Tim Willemse for their feedback and discussion. We would also like to thank the anonymous reviewers for their effort and constructive remarks and questions.

Cite AsGet BibTex

Rick Erkens and Maurice Laveaux. Adaptive Non-Linear Pattern Matching Automata. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 20:1-20:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Pattern matching
  • Pattern matching
  • Term indexing
  • Tree automata


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. L. Cardelli. Compiling a functional language. In LISP and Functional Programming, pages 208-217. ACM, 1984. Google Scholar
  2. J. Christian. Flatterms, discrimination nets, and fast term rewriting. Journal of Automated Reasoning, 10(1):95-113, 1993. URL:
  3. Fabrice Le Fessant and Luc Maranget. Optimizing pattern matching. In ICFP, pages 26-37. ACM, 2001. Google Scholar
  4. Albert Gräf. Left-to-right tree pattern matching. In RTA, volume 488 of LNCS, pages 323-334. Springer, 1991. Google Scholar
  5. P. Graf. Substitution tree indexing. In J. Hsiang, editor, Rewriting Techniques and Applications, pages 117-131, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg. Google Scholar
  6. W. McCune. Experiments with discrimination-tree indexing and path indexing for term retrieval. Journal of Automated Reasoning, 9(2):147-167, October 1992. URL:
  7. R. Sekar, I.V. Ramakrishnan, and A. Voronkov. Chapter 26 - term indexing. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, Handbook of Automated Reasoning, pages 1853-1964. North-Holland, Amsterdam, 2001. URL:
  8. R. C. Sekar, R. Ramesh, and I. V. Ramakrishnan. Adaptive pattern matching. SIAM Journal of Computing, 24(6):1207-1234, 1995. URL:
  9. M. van Weerdenburg. An account of implementing applicative term rewriting. Electronic Notes in Theoretical Computer Science, 174(10):139-155, 2007. Google Scholar
  10. A. Voronkov. The anatomy of vampire implementing bottom-up procedures with code trees. Journal of Automated Reasoning, 15(2):237-265, 1995. Google Scholar