自适应非线性模式匹配自动机
Adaptive Non-linear Pattern Matching Automata
AI总结：
本文扩展自适应模式匹配自动机，通过交错变量一致性检查与模式匹配阶段，减少查找所有匹配的步骤，并证明正确性。
摘要：
高效的模式匹配对于实用的项重写引擎至关重要。通过将给定的模式预处理为有限确定性自动机，可以在对输入项相关部分的单次遍历中判定匹配模式。大多数基于自动机的技术仅限于线性模式，其中每个变量最多出现一次，并且需要额外的后处理步骤来检查所谓的变量一致性。然而，我们可以证明，将变量一致性检查与模式匹配阶段交错进行可以减少找到所有匹配所需的步骤数。因此，我们采用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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
