A Set Automaton to Locate All Pattern Matches in a Term

TL;DR

This paper introduces a novel set automaton approach for term pattern matching that efficiently finds all pattern matches by visiting each function symbol once, supporting various traversal patterns and parallel search.

Contribution

The paper presents a new set automaton based on match set derivatives for efficient term pattern matching, enabling parallel search and flexible traversal.

Findings

Efficient algorithm visits each symbol once.

Supports various traversal patterns.

Suitable for parallel search implementations.

Abstract

Term pattern matching is the problem of finding all pattern matches in a subject term, given a set of patterns. Finding efficient algorithms for this problem is an important direction for research [19]. We present a new set automaton solution for the term pattern matching problem that is based on match set derivatives where each function symbol in the subject pattern is visited exactly once. The algorithm allows for various traversal patterns over the subject term and is particularly suited to search the subject term in parallel.