论文标题
自适应非线性图案匹配自动机
Adaptive Non-linear Pattern Matching Automata
论文作者
论文摘要
有效的模式匹配对于实际术语重写引擎至关重要。通过将给定模式预处理到有限的确定性自动机中，可以在输入项的相关部分的单个遍历中确定匹配模式。大多数基于自动机技术的技术仅限于线性模式，其中每个变量最多一次一次发生，并且需要一个额外的后处理步骤来检查所谓的变量一致性。但是，我们可以证明，将变量一致性和模式匹配阶段交织在一起可以减少查找所有匹配的所需步骤的数量。因此，我们采用Sekar等人介绍的现有自适应模式匹配的自动机，并通过一致性检查扩展它们。我们证明，由此产生的确定性模式匹配自动机是正确的，并显示了几个可以减少的示例。
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 all matches. Therefore, we take the existing adaptive pattern matching automata as introduced by Sekar et al and extend these with consistency checks. We prove that the resulting deterministic pattern matching automaton is correct, and show several examples where some reduction can be achieved.
