This presentation builds on a previous presentation by Maurice Laveaux that was titled ‘adaptive non-linear pattern matching automata’.

Pattern matching is a fundamental problem in many areas of computing science, both practical and theoretical. Given a large finite set of first-order patterns and a term t, we are interested in an efficient way to find all pattern matches for t. In the previous presentation we proposed adaptive non-linear pattern matching automata (ANPMA) as an extension of earlier work on adaptive pattern matching automata by Sekar et al. By preprocessing the given pattern set and constructing an automaton, it is possible to solve the matching problem by only inspecting every position of term t at most once. In a setting where the pattern set is fixed and the matching problem has to be decided many times, it is crucial for performance to have such an automaton. The method that we proposed is not optimal yet. The construction algorithm can yield states that are redundant. These redundancies are due to the fact that function symbol checks can give information about consistency checks and vice versa. The relation between these two kinds of checks is not clear yet. In this presentation I will talk about a solution that we have in mind to compute an optimal ANPMA on the fly. The work on ANPMA will be presented at FSCD 2020. The extension that I will talk about next thursday is still a work in progress.