paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Relational e-matching

关系式 e-matching
POPL 6(POPL)2022匹配度 3/10 · 论文属于形式验证/定理证明中的 e-matching 与 e-graph 技术,虽与程序分析和形式化验证相邻,但没有涉及用户核心关注的 LLM/Agent 与静态分析/形式化验证的交叉,也不涉及浮点程序分析或贝叶斯程序分析。引用 12 inbox
Yihong Zhang, Yisu Remy Wang, Max Willsey, Zachary Tatlock
crossref: 2026-09-10

AI 速览

一句话:提出基于关系连接与查询计划的 e-matching,保证最坏情况最优运行时间,并在 egg 中大幅加速。

e-matching 是 e-graph 上等式饱和等技术的核心操作,传统回溯方法通常自顶向下搜索,难以充分利用模式结构,且缺乏数据复杂度分析。本文将其重新表述为关系连接,借鉴数据库查询执行技术,按照优化查询计划在 e-graph 中搜索,从而保证最坏情况最优运行时间。作者还给出首个 e-matching 数据复杂度结果,将运行时间限制为 e-graph 大小与输出大小的函数。在 state-of-the-art 的 egg e-graph 框架中原型实现并评估,相比传统基线更易实现,实际中快几个数量级。

问题
传统 e-matching 多采用自顶向下回溯,不能充分利用模式结构,且缺少数据复杂度保证。
方法
将 e-matching 转化为关系连接,使用数据库查询执行与优化查询计划在 e-graph 上进行匹配。
评估
在 egg e-graph 框架中原型实现,与传统基线比较,证明更易实现且实践中快数个数量级。
原文摘要(Abstract)

We present a new approach to e-matching based on relational join; in particular, we apply recent database query execution techniques to guarantee worst-case optimal run time. Compared to the conventional backtracking approach that always searches the e-graph "top down", our new relational e-matching approach can better exploit pattern structure by searching the e-graph according to an optimized query plan. We also establish the first data complexity result for e-matching, bounding run time as a function of the e-graph size and output size. We prototyped and evaluated our technique in the state-of-the-art egg e-graph framework. Compared to a conventional baseline, relational e-matching is simpler to implement and orders of magnitude faster in practice.

链接与引用

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

BibTeX
@article{paperbot1592,
  title = {Relational e-matching},
  author = {Yihong Zhang and Yisu Remy Wang and Max Willsey and Zachary Tatlock},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {6},
  number = {POPL},
  year = {2022},
  doi = {10.1145/3498696}
}