“在纯表达式片段内，外部搜索也可用等式饱和保留多个等价形状，再用正费用树提取交最便宜代表及覆盖所有候选的距离证书。搜索与提取不替代本页的侧条件和目标语义证明：数学整数恒等式须重新核机器位宽、t…”
形式陈述
搜索可以先保留两条路
一个优化规则可能让当前表达式更便宜，却遮住下一条规则要匹配的形状。等式饱和不立即丢弃旧形状：它把旧项与新项并入同一个等价类，继续在所有已保留形状上搜索。最终怎样选一份程序，由另一个费用接口回答。[1，§2.2]
先固定语义。本页的项是有限、无绑定的纯整数表达式，叶为变量或整数常量，算子为add、mul、dbl，其中dbl(z)=2z。环境给每个变量一个数学整数；运算总定义，没有读写内存、异常、I/O、poison或资源耗尽观察。每个有限项都终止，唯一观察是整数值。下载器具体接收变量x/y、常量0/1/2及这三个算子；变量赋值仍可为任意数学整数。若移植到机器位宽、浮点或有副作用IR，须重新证明规则满足该层的语义保持合同。
输入还包括有限条有方向的模式规则ℓ→r。模式变量例如?a可代表任意子项；r的变量必须都在ℓ出现。每条规则都承担前提
σ把模式变量替换成合法项。引擎检查模式语法与变量范围，但不会自动证明任意用户规则的这项全称等式。例子使用加零、乘一、乘二改dbl及分配律的反向；它们对本整数模型直接成立。
e-node的孩子是类，不是一份确定程序
一个e-node写作f(c₁,…,cₖ)，孩子是e-class编号。一个e-class含一组被认为等价的e-node。递归地，从类里选一个节点，再从每个孩子类选有限项，就得到这个类表示的有限表达式。类图允许环，环可压缩表示无限多份有限表达式；它不命令生成器输出无限语法或循环求值。[1，定义2.1–2.4]
沿用同余闭包的核心义务：若两个节点算子相同、对应孩子类已相同，它们的结果类也必须相同。这里与固定地面项判定的差别是，规则会不断添加此前未出现的右侧项，待维护的节点集合随搜索增长。
附件用并查集维护类合并。规范节点键为(f,find(c₁),…,find(cₖ))。称图为clean，是说所有同键节点已归入同类，查询看到的类和孩子编号均已规范化；merge之后可能只合并孩子，父节点还没归并，此时图标为dirty。
一轮分成读、写、重建
- 读。 在同一份clean快照中，为每条左模式枚举全部(根类,替换)。替换把模式变量映到类；同一变量重复出现时必须映到同类。例如add(?a,?a)不能匹配孩子类不同的add(x,y)。
- 写。 对刚收集的每个匹配，按替换建立右模式节点，把右侧结果类与原根类合并。搜索期间读到的旧编号仍可用find追到新代表元，但这阶段不再执行模式查询。
- 重建。 规范化全部节点键，合并同键结果类，反复扫描到没有新合并，再发布clean快照。
只有完整一轮没有新增节点、没有新增类合并，才返回saturated。轮数预算耗尽返回iteration-limit；即使这时恰好已经包含最优式，也不能把未做的闭包检查补写成“饱和”。预算为零时返回初始clean图和limit。[1，§3.3，图5]
直觉
一次便宜改写可能挡住共同因子
固定输入
费用规定：变量/常量每个出现收1，add收2，mul收4，dbl收1。原式费用为17。若先把两次乘二直接替换成dbl，再去掉加零，得到dbl(x)+dbl(y)，费用6。
但共同因子规则需要看见add(mul(a,c),mul(b,c))。如果旧乘法形状还在，就能另走到(x+y)×2，再到dbl(x+y)，费用5。等式饱和的价值是两条路线都保留，而不是承诺每一步立即降费用。
费用只是本次选择目标，不是执行时间的普遍预测。真实机器的延迟、吞吐、寄存器压力和共享结果会改变目标函数；算术相等也不自行证明某台机器上更快。
例子与边界
三轮日志中，最后一轮没有新信息
下载器固定四条规则：add(a,0)→a，mul(a,1)→a，mul(a,2)→dbl(a)，以及共同因子规则。右侧中的a、b、c均为模式变量。
| 完整轮 | 匹配数 | 新增原始节点 | 重建后类数 | 本轮含义 |
|---|---|---|---|---|
| 1 | 4 | 4 | 8 | 去加零、两次强度削弱、提取共同因子 |
| 2 | 5 | 1 | 8 | 为新产生的整体乘二添加dbl |
| 3 | 5 | 0 | 8 | 所有匹配右侧已经存在，确认饱和 |
一次“匹配”不是一次有效改善；第三轮仍有5个匹配，但没有新事实。若预算只给1轮，程序真实返回limit，图内最低费用为6；增加预算后才得到费用5并完成无变化轮。
加零合并后，x所在类同时含x和add(该类,0类)，出现自环。它表示x、x+0、(x+0)+0等有限项，所有值相同。提取时不应沿自环无休止展开，而应选择有限的x叶。
没重建的图不能拿来宣布没有机会
另建dbl(x+0)、dbl(x)以及二者各自再乘2。先把x+0类与x类合并，两个dbl的类尚未合并；此刻附件的snapshot会明确拒绝dirty查询。
重建扫描发现两个dbl具有同键，合并它们；上层两次mul也随之同键。附件这个夹具完成2次同余合并，连同确认不再变化的扫描共2遍。仅合并底层DSU、然后把父类暂时不同当作真实不等价，会漏匹配；漏匹配又可能误导饱和检测。
有效等式也能让搜索一直长大
在整数模型中，mul(a,0)→mul(add(a,1),0)始终保值。从x×0出发，它可以产生(x+1)×0、((x+1)+1)×0等项。结果类都合并，但参数x、x+1、x+2并不会因此相等，参数类还会继续增长。
附件只给这条规则3轮预算，新增节点依次3、2、2，重建后类数5、6、7，返回limit。重建在固定节点集合上一定结束，不意味着会不断造新项的外层饱和过程一定结束。
饱和也只针对给定的有方向匹配规则和起始表示。只有f(a)→a时，从a起步不会凭空生成f(a)。不能把方向规则闭包声称为完整等式理论判定器；需要反向探索的规则必须明确提供相应方向。
推论与应用
为什么添加和合并不会改变值
保持不变量：同类表示的所有有限项，在每个环境下都取同一值。初始按相同节点共享建图，这项性质成立。
一次规则匹配把模式变量绑定到类。每个类的任意两个代表项由不变量同值，纯算子的同余性保证替换代表不会影响整个模式值；规则全称等式再保证右模式同值。因此新增右侧和根合并可靠。重建只合并同算子、同孩子类的节点，又由同余性保值。
每次合并取候选并集，旧项仍被表示；规范化和同键去重只改变表示，不删除某份可构造项。所以预算停止时仍可安全选择当前根类中的任意有限项。这里的语义安全以每条规则真实有效为前提；数据结构不会替错误规则兜底。
重建的终止与实际费用
重建期间不增加节点。若一遍扫描发生有效合并，活跃类数至少少1；最多做C−1次这样的合并，再做一遍无变化扫描便停止。最后同键都同类，正好恢复查询需要的不变量。egg用父列表与去重工作队列减少重检；附件采用全表扫描，便于逐步复查，不套用另一种实现的性能结果。[1，§3.2及定理3.1]
设重建开始时已分配N个原始节点/DSU编号，E条孩子出现，活跃类数C。附件按大小合并、不做路径压缩，find为O(1+log(N+1))；哈希表操作取期望常数。每次全表重建保守需O((C+1)(N+E+1)(1+log(N+1)))时间，工作空间O(N+E+1)。重复的旧记录仍占原始表位置，不能只按最终去重后的节点数报这个实现的成本。
写阶段的add为确保dirty期间也正确，直接扫描原始表，比较规范键；一次加入最坏需O((N+E+1)(1+log(N+1)))。它没有声称每次插入都期望O(1)。模式枚举还可能产生大量分支：设单个模式大小P，计入节点检查、分支和完成记录的实际搜索步数为M，复制待办列表/替换及去重的保守工作为O(M(P+1)²)。完整轮须另加全部右侧出现的加入、合并与重建；不能只给DSU的费用便说整个饱和近乎线性。
输出图与输出程序分开验收
有限树费用提取在冻结的clean图上交最优有限代表及可核验证书。它可以对尚未饱和的图运行，但“当前图中最优”与“所有可推导表达式中最优”不是同一句话。
综合练习要求交三轮日志、8类图、费用17→6→5的不同路径及dirty父传播夹具；再移除因子规则和改变预算，解释两种不同的搜索缺口。若目标表达式含效果，先把效果次序放进IR语义与规则前提，不能直接把本纯整数引擎套在load或调用上。
参考资料
- Max Willsey、Chandrakana Nandi、Yisu Remy Wang、Oliver Flatt、Zachary Tatlock、Pavel Panchekha，egg: Fast and Extensible Equality Saturation，POPL2021，arXiv:2004.03082v3，2020-11-07。§2.1定义2.1–2.7及§2.2（PDF pp.3–6）；§3.2重建、定理3.1及§3.3读写分期（PDF pp.7–10）。本页采用独立全表实现及没有除法的整数例子。
- egg项目，官方背景教程，文档0.11.0，2026-10-09读取：e-graph表示、饱和与提取的不同阶段。主文规则可靠性、具体计数和简化实现成本按本页接口独立证明。