提升E-Graphs

# 提升 E-Graphs 来源：https://www.philipzucker.com/lifting_egraph/ 我向 EGRAPHS 研讨会提交了一篇演讲，并被接受了：https://pldi26.sigplan.org/details/egraphs-2026-papers/13/Lifting-E-Graphs-A-Function-Isn-t-a-Constant 从提交摘要到现在，虽然“这里有点东西”的核心没有改变，但我对这个东西的理解和最佳解释已经得到了完善。 整个设计源于一种直觉，这种直觉来自对`R^n \-\> R`函数进行系统性操作的语义模型。我现在将我先前称为“瘦化 e-graph”（Thinning e-graph，参见 https://www.philipzucker.com/thin_egraph/）的东西改称为“提升 E-Graph”（Lifting E-Graph），因为“提升”（lift）这个词更能体现主要操作对`R^n \-\> R`函数所做的事情。 ## 显式名称有什么问题？ 显式名称有三个问题： 1. 生成性过程（如 eqsat）可能失控。有时我们需要新名称。例如，`P \-\-\> forall x, P \| where x fresh` 对命题来说基本上是一个有效的重写。有时这样的重写是有用的。如果我们只是用 gensym 生成它们，可能会以不同的名称重复多次冗余推导。我们可以玩斯科伦游戏和自由变量分析游戏来推导出我们知道是新鲜的且可重复的名称，但这（主观上）不优雅。 2. 丢失了共享。`f(g(h(x)))` 与 `f(g(h(y)))` 不共享任何存储。随着项越来越深、越来越大，丢失的存储机会也会增多。这两件事 **并不相等**，所以我并不是在抱怨丢失了 **相等性**。我是在抱怨丢失了一种可以用于推理和压缩的 **关系**。 3. 共享太多。这是令人惊讶的一点。我认为，如果不小心使用显式名称，实际上会将不相同的对象混为一谈。符号 `sin(x)` 实际上可能指代不同的数学对象，我们至少应该意识到可能存在歧义并加以消除。 我认为更令人惊讶的是问题 #3。让我们对此展开讨论。 ## 原罪：X 从普通角度看，`sin(x)` 是没问题的。我们已经使用这种符号数百年了。它行得通。我们看到它时就知道它是什么意思。 但从另一个角度看，它极其模糊，甚至可能合并了不同的实体。我们似乎在模糊地指代函数 `sin`，但具体是指 `x \|\-\> sin(x) : R \-\> R`， 还是指 `x,y \|\-\> sin(x) : R^2 \-\> R`？ 根据简单类型化的世界观，这是不同的东西，实际上由于类型不匹配甚至无法进行相等性比较。这两个函数的图像完全不同。然而，抑制上下文 `x,y \|\-\>` 或将其隐含的符号却将这两者混为一谈。至少值得担心的是，在某些微妙的方式下，这种混淆实质上是在断言 `R^2 = R^1`，并由此引发混乱。 从这个观察中，可以得出今天设计哲学的一条口号： **上下文不是术语的 *位置*，而是术语 *是什么* 的一部分** 对于“上下文”这个概念的某些理解，情况并非如此，但这就是我今天想要做的。 我们将选择 **永远不** 省略 `x,y \|\-\>` 的信息。它是我们所讨论事物的一个组成部分。今天，我们认为谈论一个“裸露的” `sin(x)` 基本上是不连贯的。 ## 朴素的匿名表示 有一种朴素的方法可以使用普通的 e-graph / 普通的一阶项来实现这种设计哲学。 我们可以为每个可能使用的维度/上下文创建每个函数符号的不同副本，并通过 (维度, 索引) 对 $x_{di}$ 来引用变量，而不是使用名称。例如，$x_{10}$（大小为1的上下文中的第0个变量）就是之前我会称之为 `x \|\-\> x` 的东西；$x_{21}$（大小为2的上下文中的第1个变量）就是之前我会称之为 `x,y \|\-\> y` 的东西。 同样，我们也可以根据参数类型将所有的 `sin` 消歧义为不同的版本 $\sin_d$。如果 $x_{21}$ 的类型是 $R^2 \rightarrow R$，那么如果 `sin` 打算接受它，它就需要接受该类型的参数。于是我们有 $sin_0 : (R^0 \rightarrow R) \rightarrow (R^0 \rightarrow R)$，$sin_1 : (R \rightarrow R) \rightarrow (R \rightarrow R)$，$sin_2 : (R^2 \rightarrow R) \rightarrow (R^2 \rightarrow R)$，等等。 实际上，所有这些都来自常规 `sin` 函数的逐点应用，并且这是一种参数多态构造，因此这种消歧义其实并不是必需的（索引 `n` 可以从 `sin` 参数的维度推导出来）。不过，如果我们想保持在简单类型的框架内，这就是我们必须做的。 好，这很好。这种谨慎确实解决了问题 #3（共享太多）。同时，对于问题 #2（共享太少），我们既有所改善也有所恶化。 因为我们现在通过整数来引用变量，从而实现了匿名化，`x \|\-\> f(g(h(x)))` 在语法上与 `y \|\-\> f(g(h(y)))` 相同，因为两者都变成了 `f1(g1(h1(x10)))`。从这个意义上说，共享变得更好了。 另一方面，现在 `f1(g1(h1(x10))) : R \-\> R` 和 `f2(g2(h2(x20))) : R^2 \-\> R` 完全不共享任何存储，尽管它们非常相似（同样，它们 **不相等**，因为甚至类型都不同）。也许以前我们可以将两者都称为 `f(g(h(x)))`，所以对于这两种情况，我们共享存储的能力反而变差了。 那该怎么办呢？ 好吧，我们来讨论一下 `f1(g1(h1(x10))) : R \-\> R` 和 `f2(g2(h2(x20))) : R^2 \-\> R` 在语义上关联的方式。 后者是前者的提升版本。 如果你给我一个对象 `f1(g1(h1(x10))) : R \-\> R`，我可以通过简单地丢弃第二个参数并传播第一个参数来生成对象 `f2(g2(h2(x20))) : R^2 \-\> R`。作为 Python 函数，这个提升组合子可以写成 `lambda f: lambda x,y: f(x)`。这是一个提升操作，提升操作有一个可处理的代数与之关联：https://www.philipzucker.com/thin1/ 我完全可以不存储 `f2(g2(h2(x20))) : R^2 \-\> R`，而是存储 `lift_10(f1(g1(h1(x10)))) : R^2 \-\> R`。`lift` 上的下标是一个位向量，如果应该保留该参数则为1，如果丢弃则为0。同样，这一切都是完全一阶语法且简单类型的。我可以在常规 e-graph 中将其作为一种编码来实现。由于这两个语义上不同的事物现在共享大的子项，因此实现了子结构的共享。 提升具有一些有用的性质，可以将其编码为规则。像 `sin` 这样的典型逐点派生组合子的“参数多态性”表现为一条重写规则：`sin(lift_i(X)) = lift_i(sin(X))`。这表示 `lift` 相对于典型函数符号是同态的 / 它某种意义上与它们交换。 此外，还有一种类似于常量传播的提升规则：`lift_i(lift_j(X)) = lift_k(X)`，其中 `k = i . j`。 简而言之，我们正在讨论的系统可以编码为显式的一阶 `lift` 组合子，并带有 1. `lift_i(lift_j(X)) = lift_k(X)` —— 提升压缩规则 2. `f(lift_i(X), lift_i(Y)) = lift_i(f(X,Y))` —— 提升提拉规则 ## 将提升融入核心 提升的这些性质是如此简单、普遍且具有结构性，以至于将其直接融入术语或 e-graph 本身的核心定义可能是有意义的。这一点因提升/瘦化可以表示为紧凑的位向量而更加诱人。 提升可以很容易地用位向量（一种瘦化）表示，其中1表示保留变量，0表示丢弃变量。 这是一种非常紧凑的数据，而且我认为窃取几个位来将其与典型的 eid（e-class 标识符）打包在一起并非完全疯狂。 ## 提升的智能构造函数 同态规则可以定向为尽可能将提升向上提拉：`f(lift_i(X), lift_i(Y)) \-\> lift_i(f(X,Y))`。这是一种自然的重写排序，因为右侧的项更小。Knuth-Bendix 序可以实现这一点。你还应该将 `lift` 的优先级设低，以处理单目情况 `f(lift(X)) \-\> lift(f(X))`。 智能构造函数操作将确保，每当你使用比必要更提升的参数 eid 构建一个节点时，无论额外的提升如何，你都能得到一个指向相同内部数据的“胖” eid 句柄，从而实现减少内存使用和更快的提升关系比较。 每当你构建一个新的 enode 时，智能构造函数应该检查其参数胖 eid 的共同提升，剥离这个提升，将 enode 内部化，然后在返回胖 eid 给用户之前再将被剥离的共同提升加回去。这是一种在 e-graph 内部机械地实现提升上拉规则的方法。 如所述，这种机制及其背后的重写规则对我来说似乎相当基本且不神秘。但要达到这种感觉，需要一些时间和解释的转变。 在没有并查集的情况下，这种提升上拉智能构造函数加上胖 ID 构成了一种有趣的“α-感知”哈希压缩：https://www.philipzucker.com/thin_hash_cons_codebruijn/ 将提升向上提拉以一种有趣的方式对应于 co-De Bruijn 风格，即 McBride 在《Everybody's Got to Be Somewhere》（https://arxiv.org/abs/1807.04085）中描述的对 lambda 项进行规范化和表示的方法。到目前为止我还没有讨论过 lambda。我认为这篇文章的考虑更为基本，而 lambda/绑定形式是应该加在这个更基本层之上的一层。 还要注意，通过尽可能保持瘦化，维度可以进行一种匿名的自由变量分析。通过使其成为术语本身所“是”的结构的一部分，在做出一些冒险的变量重写之前，确保自由变量分析是最新的就不会那么成问题。 ## 提升并查集 但我们想要一个 e-graph。我们需要为那个哈希压缩添加一个并查集。 如何实现一个接受提升后的胖 eid 的并查集呢？ 因为提升是语义上的单射函数，当你合并两个提升后的 eid `lift_i(a) = lift_i(b)` 时，你可以剥离它们提升的共同部分，并得出 `a = b`。 这类似于在语法合一中或从代数数据类型之间的相等性中可能采取的步骤，这些也是单射函数。`cons(a, c) = cons(b, c)` 隐含 `a = b`。 如果剩下的只是裸 eid `e6 = e47`（因为两个提升相同），那么这时就是普通的并查集操作。 如果合并的两个对象具有不同数量的变量，那么类型检查都无法通过——如果提升不匹配是由于这个原因，那么是用户错误。 然而，仍然存在合法的情况，即不同的瘦化被合并。 ### `x * 0 = 0` 与冗余 对于任何关于 e-graph 中变量的讨论，一个令人担忧的反例是 `x * 0 = 0`。如果这是一个真正的双向等式，它允许 `x` 潜入任何使用 `0` 的位置。这感觉像是一种不卫生的作用域外溢，因为 `0` 可以出现在任何地方，包括 `x` 可能不在作用域中的地方。考虑使用一个朴素的一阶 lambda 编码： ``` lam(y, y * 0) = lam(y, 0) 通过 y * 0 = 0 = lam(y, x * 0) 通过 0 = x * 0 ``` 感觉不好。 也许可以争论一种语义，其中访问不在作用域中的 `x` 不会严重报错，而是只返回任意的（类型正确的？）垃圾。在这种情况下，如果你要通过乘以 0 立即销毁所有信息，那么访问 `x` 在语义上确实是没问题的。 尽管如此，这种语义让我（主观上）感到不适。感觉不优雅。也许我只是个懦夫。 不，不是那样。我 **确实** 是个懦夫。但尚不清楚这种不适是我的懦弱的表现，还是另有原因。 虽然我曾玩味过允许垃圾/转储操作（https://www.philipzucker.com/dump_calculus/）作为提升的伪逆的想法，但我目前的理解是不必这样做，而且我认为避免它会更优雅。 从谨慎的作用域/提升角度来看，所讨论的等式实际上是 `x \|\-\> x * 0 = 0`，它被组合子化为 `x_10 * lift_0(0) = lift_0(0)`。注意，由于 `0` 是一个常量（一个 0 元函数 `[] \|\-\> 0`），它必须被提升到当前的 1-上下文 `x \|\-\>` 中。 `x_10 * lift_0(0)` 和 `0` 实际上都会被内部化为 eid，比方说 `x_10 * lift_0(0) \-\> e47` 和 `0 \-\> e6`，所以发生的合并是 `union(e47, lift_0(e6))`。我们确实在左侧和右侧有不同提升。 并查集可以通过选择方向/父节点为 `e6` 来解决这个问题。这产生规则 `e47 \-\> lift_0(e6)`，该规则可以存储在带有提升注释的 `parents` 表中，类似于在组并查集中如何将 `e48 \-\> e14 + 7` 存储在整数偏移注释的 parents 表中。选择这个方向是必需的，因为它“解出了” `e47`。不存在一个提升可以从 `e47` 解出 `e6`：`e6 \-\> lift_?(e47) 不成立`。处于已解形式使得 `find` 能够简单地通过遍历 parents 表来累积注释。 也可能出现左右两侧都无法相对于对方求解的情况。这种情况幸运地仍然可以通过生成一个公共的新常量来解决，使得左右两侧都可以解出它：`left \-\> annot1(fresh)` 和 `right \-\> annot2(fresh)`。 同样类型的考虑在更基础的层面上来自将整数常量乘法融入并查集，例如 `3 * e47 = 2 * e3`。关于这种轻微不对称的注释并查集的更多讨论见：https://www.philipzucker.com/thin_monus_uf/ 作为一个需要生成新常量的例子，考虑 `x,y \|\-\> x*0 = 0*y`，它被组合子化为 `lift_10(x10 * lift_0(0)) = lift_01(lift_0(0) * x10)`。这种情况应该比较罕见，我几乎倾向于不实现它。两者都无法相对于对方求解，但通过生成一个新的 eid，语义上存在一个两者都应该能求解出的东西。假设右侧的 eid 是 `e14`，`lift_0(0) * x10 \-\> e14`。那么我们推断存在一个新的 `e112`，使得 `e14 \-\> lift_0(e112)` 且 `e47 \-\> lift_0(e112)`。确实，`e112` 在语义上等同于 `0`，并且如果我们先断言等式 `x \|\-\> x * 0 = 0` 和 `x \|\-\> 0 * x = 0`（这可能是更自然的做法），那么初始的示例等式 `x,y \|\-\> x*0 = 0*y` 就会被视为冗余。 这个例子多少有些构造性，只是为了展示不可协调的提升在语义上合法的情况下是如何出现的。我不认为以产生这种情景的方式编写规则是很自然的。 ## E-匹配 提升 e-graph 的所有实现都相当机械，不需要深入思考，直到我遇到 e-匹配。这让我重新审视设计，澄清我正在做的事情的语义和一阶项模型。 一个令人困惑的问题是，我们已将提升融入到核心并使其有些隐式。提升是否应该出现在模式中？应该在什么时候允许插入提升来解决问题？ 我认为我现在理解的是，至少有三个不同的 e-匹配问题你可能想解决。 1. `0 = ?x * ?y` —— 仅匹配未提升的规范 id 2. `lift_010(0) = ?x * ?y` —— 匹配提升后的 id 3. `?lift1 0 = ?lift2 (?x * ?y)` —— 匹配待定任意提升的 id。 最后一个是轻度合一问题（等式两边都有变量），所以也许我们可以认为它超出范围。不过，问这个问题也算是自然。 到目前为止，最简单的做法，而且我认为最合理的，是只支持第一种。你真的可以只匹配规范 id，而将问题#2 留给用户，由他们在模式中明确写出提升。这样，e-匹配器的工作量就大大减轻了。它只需像往常一样匹配 eclass id，并处理胖 id，这可能意味着在胖 id 的表面 eid 下面还有额外的提升。不过，由于我们引入了智能构造函数，即使是在模式中，提升的自动上拉也会发生：当你在一个模式中构造 `f(?x, ?y)` 并通过模式匹配来实例化时，你应该使用智能构造函数，这样任何未显式写入模式的提升都会被向上提拉，从而允许模式匹配成功。 在这个框架下，我尚未充分探索模式与提升之间的相互作用。这很可能是一个丰富的设计空间。 总而言之，提升 e-graph 为处理作用域和变量提供了一种结构上清晰的方法，同时利用提升的代数性质来最大化共享并最小化显式名称的混乱。虽然还有一些细节需要完善，但核心思想看起来很有前景。