自适应非线性模式匹配自动机
摘要：高效的模式匹配对于实际的术语重写引擎至关重要。通过将给定的模式预处理成有限的确定性自动机，可以在与输入术语的相关部分进行单次遍历即可确定匹配模式。大多数基于自动机的技术仅限于线性模式，其中每个变量最多出现一次，并且需要额外的后处理步骤来检查所谓的变量一致性。然而，我们可以证明交错变量一致性和模式匹配阶段可以减少找到所有匹配所需的步骤数。因此，我们采用由Sekar等人引入的自适应模式匹配自动机，并将其扩展为包含一致性检查的自动机。我们证明了产生的确定性模式匹配自动机的正确性，并展示了一些可以实现一定减小的示例。
作者：Rick Erkens, Maurice Laveaux
论文ID：2011.13752
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22