paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Adaptive Non-linear Pattern Matching Automata

自适应非线性模式匹配自动机
LMCS vol.Volume 17, Issue 42021匹配度 2/10 · 该论文研究项重写中的非线性模式匹配自动机与变量一致性检查,属于逻辑/自动机和形式化方法范畴,但与用户画像中的静态分析×LLM/Agent、浮点程序分析、贝叶斯程序分析等核心方向没有直接交集,仅有较弱的PL/形式化背景关联。引用 1 inbox
Rick Erkens, Maurice Laveaux
crossref: 2026-09-10

AI 速览

一句话:扩展自适应模式匹配自动机以支持非线性模式,通过交错变量一致性检查与匹配来减少匹配步骤。

高效模式匹配是项重写引擎的基础。将模式预处理为有限确定性自动机,可在单次遍历输入项的相关部分后判定匹配。多数基于自动机的方法局限于线性模式(每个变量至多出现一次),并需额外的后处理步骤来检查变量一致性。本文表明,将变量一致性检查与模式匹配阶段交错进行可减少找到所有匹配所需的步骤。为此,我们在Sekar等人提出的自适应模式匹配自动机基础上扩展了一致性检查。我们证明所得确定性模式匹配自动机是正确的,并给出若干示例展示可实现的步骤缩减。

问题
现有基于自动机的模式匹配技术大多局限于线性模式,且需要单独的后处理步骤来检查变量一致性,影响匹配效率。
方法
在Sekar等人的自适应模式匹配自动机基础上加入一致性检查,将变量一致性检查与模式匹配阶段交错进行,并证明所得确定性自动机的正确性。
评估
通过形式化证明确保自动机正确,并给出多个示例展示匹配步骤的缩减。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot1255,
  title = {Adaptive Non-linear Pattern Matching Automata},
  author = {Rick Erkens and Maurice Laveaux},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 17, Issue 4},
  year = {2021},
  doi = {10.46298/lmcs-17(4:21)2021}
}