一句话：egglog 将 Datalog 与等式饱和（EqSat）统一为定点推理系统，兼具增量执行、同余闭包与项抽取能力。
论文指出现有两大定点推理范式各有短板：Datalog 擅长高效增量执行、协作分析与基于格的推理，却缺乏项重写、同余闭包与优化项抽取；等式饱和（EqSat）恰好相反。作者提出 egglog，将二者统一在同一个定点推理系统中，使其既能像 Datalog 那样增量执行并支持多分析协作与格推理，又能像 EqSat 那样进行项重写、高效同余闭包以及提取优化后的项。为验证设计，作者选取两个近期应用——Datalog 中基于合一（unification）的指针分析与 EqSat 的浮点项重写器——它们原本各自受限于对方范式的缺失特性，并分别用 egglog 重新实现。结果显示，重写后的系统更快、更简单，并修复了原系统中的若干缺陷。
We present egglog, a fixpoint reasoning system that unifies Datalog and equality saturation (EqSat). Like Datalog, egglog supports efficient incremental execution, cooperating analyses, and lattice-based reasoning. Like EqSat, egglog supports term rewriting, efficient congruence closure, and extraction of optimized terms. We identify two recent applications -- a unification-based pointer analysis in Datalog and an EqSat-based floating-point term rewriter -- that have been hampered by features missing from Datalog but found in EqSat or vice-versa. We evaluate our system by reimplementing those projects in egglog. The resulting systems in egglog are faster, simpler, and fix bugs found in the original systems.
@article{paperbot1982,
title = {Better Together: Unifying Datalog and Equality Saturation},
author = {Yihong Zhang and Yisu Remy Wang and Oliver Flatt and David Cao and Philip Zucker and Eli Rosenthal and Zachary Tatlock and Max Willsey},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591239}
}