“在纯表达式片段内，外部搜索也可用等式饱和保留多个等价形状，再用正费用树提取交最便宜代表及覆盖所有候选的距离证书。搜索与提取不替代本页的侧条件和目标语义证明：数学整数恒等式须重新核机器位宽、t…”
形式陈述
类图有环，输出仍须是一棵有限树
输入是等式饱和页定义的clean e-graph：有限非空类集，每类有有限非空节点集合；每个节点带一个固定元数的算子和有效孩子类编号，同一规范节点键不能出现在两处。根是一个有效类。各类的语义等价已经由建图者负责，提取器不另证明任意用户合并是正确等式。
给每个节点n一个严格正整数费用w(n)。选出的有限表达式树T按每个节点出现计费：
同一个孩子类在两个位置出现就收费两次，不能因为编号相同只加一次。本页求根类所表示的有限树中的最小费用；若根类没有任何有限树，输出NO_FINITE_TERM。允许类图循环，不以任意深度截断后“没找到”冒充无解。[1，§2.2；2，CostFunction]
以高度作为真正无环的状态维度
空树不在文法中，叶的高度规定为1。令D₀(c)=∞，并对h≥1定义
孩子为空时和为0；有任一孩子∞时该候选为∞。D_h(c)表示c中高度至多h的最小费用。每一轮必须读取上一轮数组，不能在证明写同步高度、实现却随扫描顺序读本轮结果。
这是一份动态规划：状态为(h,c)，后继在h−1层。类别依赖本身可以成环，但高度状态的依赖严格下降。设类数为C，本页证明只需计算至h=C；实现保留前后两行，不要求先给原类图作拓扑排序。
证书既要实现费用，也要排除更便宜的树
输出每类距离d(c)∈正整数∪{∞}；有限距离的类另选一个节点b(c)。核验器检查：
- 每个节点n∈c都满足d(c)≤w(n)+Σd(child)，以∞按通常扩展顺序比较
- d(c)有限时，b(c)必须属于c，且上式在这个节点取等号
- d(c)=∞时没有选择；不能存在全部孩子有限的节点，否则第一项已经失败
严格正费用使每条被选孩子边的距离都小于父距离，因此选择图不可能有环。第一项给所有候选树统一下界，第二项交出达到该界的树。只验证“输出程序确实属于根类”不能证明最优。
直觉
先知道叶价，再把可能结束的路传上来
考虑一类同时有x与add(本类,0类)。第一次高度迭代就从x得到费用1；沿环走一圈会额外支付add与0，不会更便宜。选x即可结束。
另一类只有loop(本类)，没有任何叶出口。初始∞沿公式一轮轮保持∞。它不是费用为0的程序，也不是可以随意忽略的空代码；这个类根本没有有限项。
图中的有向环属于候选集合，真正选出的结果边严格降费用。把“输入图可有环”误解成“输出时随便选一条出边也能结束”，会让提取器卡在自引用上。
例子与边界
八类距离怎样认证费用5
综合例的冻结图为下表。子编号可重复，所有编号指向类；变量/常量费用1，add为2，mul为4，dbl为1。
| 类 | 节点候选 | 最终距离 |
|---|---|---|
| 0 | x；add(0,1) | 1 |
| 1 | 常量0 | 1 |
| 2 | 常量2 | 1 |
| 3 | mul(0,2)；dbl(0) | 2 |
| 4 | y | 1 |
| 5 | mul(4,2)；dbl(4) | 2 |
| 6，根 | add(3,5)；mul(7,2)；dbl(7) | 5 |
| 7 | add(0,4) | 4 |
第1轮只有叶类0、1、2、4取得1。第2轮类3、5取得2，类7取得4；第3轮根取得5。其后到第8轮数组不再改变。
根的三个候选分别为2+2+2=6，4+4+1=9，1+4=5。证书选择dbl(7)，类7选择add(0,4)，最后到x/y叶。输出dbl(add(x,y))，费用5。核验其余候选的不等式同样重要：若根错误报9，费用6和5的候选会立刻违反下界检查。
纯环与错误证书有可执行的拒绝原因
一类{loop(0),leaf}，费用分别1与3，最优取leaf，距离3；去掉leaf后得到NO_FINITE_TERM。把后一种答案误填到前一种图上，会被有限叶候选的费用3反驳。
若真实最优叶费1，却交d=2，第一项1候选会拒绝过高的下界。若交d=1却选择费用1的自环节点，其候选总费是1+d=2，第二项拒绝不能实现的选择。两个检查分别阻止“比所有合法树还贵”和“凭空声称更便宜”。
零费用不在本合同内。若允许费用0的自环与费用1的叶，数值1可以正确，却可能在并列选择时选自环，距离不再严格下降；需要额外的高度或无环选择策略。负费用循环更可能令有限树费用向−∞下降而没有最小值。本算法在入口拒绝这两类权重，不给它们套正费用证明。
树最优不能冒充共享DAG最优
给一份完整四类图：根R只有pair(A,B)，节点费1；A有叶a费6，或g(Q)费1；B有叶b费6，或h(Q)费1；Q只有叶q费6。语义前提指定a=g(q)、b=h(q)，所以类内候选确实相等。
逐出现树费用下，A选a的6优于g(q)的7，B同理，根最优为1+6+6=13。若目标改为共享DAG，并把同一个q只计算一次，则pair(g(q),h(q))费用为1+1+1+6=9。此前两个局部的“较贵选择”合起来反而更便宜。
因此同一个RecExpr或节点编号在存储上共享，并不自动把树费用改成共享执行费用。要优化DAG，需要显式联合考虑各处的选择和共用；不能复用本页的13最优证书去否定费用9的DAG。[2，重复e-class出现说明]
推论与应用
为什么C轮足够，而不是经验深度
如果某类有有限项，全部合法有限项费用是一组非空自然数，必有最小值。取一棵最优树。假设某条根到叶路径两次经过同一个类c：外层c子树中包含更深的c子树。把外层整棵子树替换为内部那棵，仍是c表示的合法项，也仍满足上层对孩子类的要求。
这次替换至少删除外层路径上的一个正费节点，其他被删旁支费用也为正，故总费用严格下降，与最优矛盾。因此最优树的任意根叶路径不重复类，节点高度至多C。树的不同分支仍可重复同一类，这不与路径结论冲突。
对h归纳，递推恰枚举高度至多h的树：h=1只允许零元节点；更高树由一个根节点和高度至多h−1的孩子组成，所有合法选择都被min覆盖。于是D_C是无高度限制的最优值。若它仍为∞，假设存在有限项便会产生高度≤C的最优项，矛盾。这给出NO_FINITE_TERM的完整理由。
最优距离怎样变成可核验证书
最终d对每个节点都不大于其用最优孩子组合出的费用，否则这份组合会比d还便宜。每个有限类的最优树根必有一个节点取等号，故可选b(c)。严格降费用保证从这些选择重建时不能回到旧类，输出一定有限。
反过来，若外部证书通过三项检查，对任意有限表示树按结构归纳：每个孩子真费用至少为其类的d，根的不等式便给d(c)≤整棵树费用。这证明d是全体候选的下界。对选中图，按严格下降的距离归纳，等号又给一棵真费用恰为d的树，因此达到下界。
∞类若有有限树，则沿该树由叶向上应用第一项，全部类都会有有限上界，和d=∞矛盾。验证器无需重新跑高度DP，就能同时检查最优性和无有限项判断。它检查的是给定图及费用，不认证此前所有合并的语义理由。
时间、数值位数与输出大小分账
设C为类数，N为规范节点数，E为全部孩子出现数。同步C轮各扫描节点和孩子一次，求值阶段需O(C(C+N+E))次整数加法/比较与索引操作；图验证、最终选择和证书核验另需O(C+N+E)。只留两行及选择时工作空间O(C+N+E)。若费用数需β位，整数加法/比较还要乘相应O(β)位成本，不能把任意大整数称作机器字常数。
下载器为教学另外保留每轮完整距离，共O(C²)个数，故它的总空间是O(C²+N+E)，而非只保留两行的界。每类最优树高度≤C仍可能有指数多节点：二叉节点两个孩子都指向下一类时，展开反复复制该类的选择。打印一棵有L个出现的完整树，时间和输出空间至少Ω(L)；附件显式栈重建需O(L+E+C)级别的遍历/结果存储，不把紧凑证书空间当完整树输出空间。
若费用最大W、最大元数d，则最优树节点数不超过1+d+⋯+d^{C−1}，费用位长可由O(C log(d+1)+log(W+1))控制。这里是费用算法的数值界，不是整数程序实际运行时每次乘法的机器费用。
综合练习要求提交八类距离和全部节点不等式，并实际输出费用5的表达式；随后删掉因子规则、去掉叶出口以及改用共享DAG目标，分别定位搜索空间、可生成性和目标函数三个不同变化。
参考资料
- Max Willsey、Chandrakana Nandi、Yisu Remy Wang、Oliver Flatt、Zachary Tatlock、Pavel Panchekha，egg: Fast and Extensible Equality Saturation，POPL2021，§2.2（PDF pp.5–6）：在已表示等价项集合中按费用提取，以及更复杂目标需另用提取过程。
- egg项目，extract.rs官方源码文档，文档0.11.0，2026-10-09读取，CostFunction注释lines110–127与Extractor：重复类的树费用、节点费用严格高于孩子的条件。本页固定正整数可加费用，C轮高度算法、去重复类证明与距离证书为完整给出的教学实现。