🔢 mathematics

Categorical E-Graphs for Lambda Calculi

本文将 e-graph 的范畴框架扩展到闭对称单子范畴，以原生支持 $\lambda$ -演算中的变量绑定，引入了一种具有双推压重写机制的分层超图表示，并证明了其与标准项重写是等价的。

原作者： Aleksei Tiurin, Dan R. Ghica, Nick Hu

发布于 2026-06-26

📖 1 分钟阅读🧠 深度阅读

原作者： Aleksei Tiurin, Dan R. Ghica, Nick Hu

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下你正在试图解开一个巨大的拼图，但每当你移动一块拼图时，你都会不小心破坏掉已经放置好的部分。这就是计算机科学家在尝试优化复杂计算机程序时面临的问题。他们使用一种叫做 e-graph（等价图）的工具，它就像是一个超级高效的档案柜。它不会在发现更好的版本时就丢弃旧版本，而是将所有版本都保存在同一个柜子里，并将含义相同的部分归为一类。这使得计算机能够同时探索数百万种可能性而不会迷失方向。

然而，这里有一个难点：e-graph 在处理变量（比如数学方程中的 “x”）时历来表现挣扎。在程序中，变量就像是一个可以到处移动的标签。如果你移动了标签，程序的含义可能会改变，或者两个完全相同的程序仅仅因为标签的位置不同而看起来不同。这使得 e-graph 很难意识到它们实际上是同一个东西。

核心理念：从文本到图像

本文作者提出了一种处理这些变量标签的新方法。他们不再将程序视为文本（像你读的一句话），而是将其视为弦图（string diagrams，类似于流程图或地图）。

旧方法（文本）： 想象你在写一份食谱。如果你在第 1 步写了“加盐”，在第 5 步又写了“加盐”，计算机看到的将是两个独立的句子。即使它们意思一样，计算机也必须做额外的工作才能意识到它们是相同的。
新方法（弦图）： 想象这份食谱是一个物理流程图，其中导线连接着食材和动作。如果你有两个“加盐”步骤，它们在物理上就是同一根连接到两个不同位置的导线。你不需要去比较文本；图像本身就展示了它们是相同的。

“魔术盒”解决方案

为了让这种方法在处理变量（即那些被“绑定”或锁定在函数特定部分内的变量，如局部变量）时奏效，作者使用了来自高级数学的概念——范畴论（Category Theory）。

把程序想象成一台机器，它有输入和输出。

盒子： 他们将一个函数（例如 lambda 抽象 λx）表示为一个圆角矩形框。变量 x 是进入这个框的一根导线。
共享： 他们使用虚线框来表示一组等价的事物。如果两个部分的程序在数学上是相等的，它们就会位于同一个虚线框内。
结果： 通过组合这些盒子，他们创建了一种被称为 Closed E-Hypergraph（封闭 e-超图）的结构。这是一个时髦的名字，指的是一种“拼图地图”，它能自动识别出两个部分是相同的，即使它们被包裹在不同的盒子中或拥有不同的变量名。

它是如何工作的：“重新布线”技巧

在传统的 e-graph 中，要修改一个程序，你必须删除旧的部分并粘贴一个新的部分。这样做是有风险且缓慢的。

在这种新系统中，修改程序就像是在重新连接电路板上的导线。

想象一次 “Beta-reduction”（编程中的基本规则，指将一个值代入一个函数）不仅仅是删除文本，而是简单地将一根导线从一个插座拔出，然后插入到另一个插座中。
因为其结构是建立在这些图表之上的，计算机不需要担心重命名变量或检查变量是否被“捕获”（被错误的作用域窃取）。导线会自然地流动。

这为什么重要（根据论文所述）

作者使用一种特定类型的编程逻辑——线性替换演算（linear substitution calculus，一种处理 “let” 语句和共享的方式）测试了这个想法。

旧方法的缺陷： 为了处理 “let” 语句（例如 let x = 1 in...），旧的 e-graph 必须添加特殊的“官僚主义”节点和规则来管理名称。这会让系统变得臃肿且缓慢。
新方法： 在他们的图表系统中，“let” 语句只是自然的连接。系统会自动理解 let x = 1 in (x + x) 与 let y = 1 in (y + y) 是相同的，而无需额外的规则。这种“共享”是内置于图表的几何结构中的。

总结

该论文声称他们为 e-graph 构建了一个新的数学基础，将程序视为拓扑地图而非文本。通过使用“盒子”来隐藏变量，以及用“导线”来连接它们，他们创建了一个系统，其中：

等价性是自动的： 如果两个图在拓扑结构上看起来相同，那么它们就是同一个程序。
重写是安全的： 你可以修改程序的一部分，而不会破坏其余部分。
变量处理更自然： 不再需要混乱的重命名或特殊的“官僚主义”节点。

作者认为，这种方法对于函数式编程语言（如基于 Lambda Calculus 的语言）特别强大，与以往依赖于“槽位式”（slotted）e-graph（将变量视为显式数据插槽）的方法相比，提供了一种更简洁、更高效的代码优化方式。他们提供了数学证明，证明其基于图表的重写与传统的基于文本的重写同样正确，但其优势在于可以直接处理程序的“形状”。

技术摘要：用于 Lambda 演算的范畴论 E-Graph

问题陈述

等价饱和（Equality Saturation）是一种强大的程序优化与推理技术，它利用等价类项（e-graphs）在不破坏性的情况下探索重写规则空间。然而，传统的 e-graph 缺乏对变量绑定的原生支持，而变量绑定是基于 $\lambda$ -演算的函数式编程语言的一项基本特征。

现有的引入绑定机制的方法面临着显著挑战：

文本表示法： 在标准文本语法中， $\alpha$ -等价的项是不同的，无法实现共享。虽然 De Bruijn 指数可以在语法上识别 $\alpha$ -等价，但这些指数依赖于变量作用域，这导致仅在索引分配上不同的项（例如 $\lambda f. f((\lambda x. fx)2)$ ）无法实现共享。
显式替换： 通过添加显式替换节点（例如 $t[x/u]$ ）来处理绑定会引入“官僚主义”（Bureaucracy）。这需要额外的节点和重写规则来管理非交互替换的排列（图形等价性），从而增加了行政开销，而非专注于领域特定的重写。
槽位 E-Graph（Slotted E-Graphs）： 最近的研究（Schneider 等人）引入了将变量视为一等公民的“槽位 e-graph”。虽然这种方法有效，但它依赖于适用于任意语言（如 $\pi$ -演算）的标称技术（Nominal Techniques），可能无法像专门的语义模型那样高效地利用 $\lambda$ -演算的特定结构属性。

核心问题在于缺乏一种原生的、范畴论意义上的数据结构，能够支持带有绑定的 e-graph，从而在无需显式替换节点或复杂重命名规则的情况下，实现对 $\lambda$ -演算的高效等价饱和。

方法论

作者提出了一种基于范畴论语义的解决方案，将 e-graph 的解释扩展为弦图（String Diagrams）。

1. 范畴论框架

本文建立在 Tiurin 等人的工作之上，后者将 e-graph（不含绑定）建模为**对称单子半格富集范畴（SLat-categories）**中的态射。

SLat-富集： 其 Hom-集是半格，其中并运算（ $+$ ）代表子项的等价性（e-graph 类）。
单子闭结构： 为了处理变量绑定，作者将该范畴扩展为单子闭范畴。这引入了内部同态对象（Internal Hom Object, $A \multimap B$ ）以及伴随关系 $- \otimes B \dashv B \multimap -$ 。
弦图： 项被表示为弦图。绑定通过“圆角框”（代表 $\lambda$ -抽象）进行建模，而等价类则通过“虚线框”（代表半格并运算）进行建模。

2. 组合表示：封闭式 E-超图（Closed E-Hypergraphs）

为了提供具体的数学数据结构，作者定义了封闭式 e-超图。这些是编码了以下内容的层次化超图：

超边（Hyperedges）： 代表操作（生成器）。
层次化边（Hierarchical Edges）： 两种嵌套结构：
- E-类（虚线框）： 代表等价类。
- 抽象框（圆角框）： 代表 $\lambda$ -抽象。
接口（Interfaces）： 该结构使用**扩展余共柄（Extended Cospans）**来管理输入和输出，区分外部接口（顶层）和严格内部接口（嵌套在框内）。

3. 重写系统

作者为封闭式 e-超图定义了一个**带接口的双推出（Double-Pushout with Interfaces, DPOI）**重写系统。

重写规则： 定义为扩展余共柄的 Span。
边界补集（Boundary Complements）： 引入了一种专门的“空洞”（Hole）定义，用于处理移除匹配项后留下的部分，以应对层次化图的特性。这确保了当移除一个子图时，内部接口能得到正确调整（例如，移除嵌套项会更新其父项的严格内部接口）。
可靠性与完备性： 本文证明了在这些封闭式 e-超图上的 DPO 重写，对于对应范畴理论中的封闭 $\Sigma^+$ -项的重写是可靠且完备的。

核心贡献

范畴论扩展： 通过将范畴域从自由对称单子 SLat-范畴扩展到自由闭对称单子 SLat-范畴，构建了一种支持绑定的 e-graph 形式。
封闭式 E-超图： 定义了一种具体的组合表示（封闭式 e-超图），它能自然地吸收对称单子结构的方程以及闭结构的方程（绑定）。
用于绑定的 DPOI 重写： 为这些结构制定了 DPO 重写系统，并证明了其相对于相应范畴理论中项重写的可靠性与完备性。
与槽位 E-Graph 的比较： 通过理论比较表明，虽然槽位 e-graph 通过标称技术提供通用的绑定，但范畴论方法将绑定嵌入到模型的内部语言中，这对于 $\lambda$ -演算特定的优化可能具有优势。

结果

重写的等价性： 本文证明了封闭 $\Sigma^+$ -项的项重写与封闭 e-超图的 DPO 重写是等价的。
处理图形等价性： 该方法能够自然地处理“图形等价性”（即非交互替换的排列），而无需显式的替换节点。在范畴模型中，显式替换被建模为复合（Composition），其结构律吸收了必要的等价关系。
案例研究 ( $\lambda_{lsub}$ )： 作者将该理论应用于线性替换演算 ( $\lambda_{lsub}$ )。他们展示了带有显式替换（如 let-绑定）的项可以直接表示为弦图。
- 与传统 e-graph 需要显式替换节点及处理其排列的重写规则不同，范畴模型将这些视为图的结构属性。
- 本文表明，语义等价的程序（例如重新排序 let-绑定）映射到相同的弦图，从而允许等价饱和在归一化的表示上运行。

意义与主张

本文声称为带有绑定的 e-graph 提供了一个基础性的范畴论语义，而这一领域此前发展不足。

理论证明： 它为 e-graph 在处理绑定时所维持的同余关系提供了严谨的证明，将其根植于闭对称单子 SLat-范畴的性质之中。
效率潜力： 通过将结构方程（如结合律、交换律和替换排列）吸收进图形语法和底层范畴中，该方法旨在减少等价饱和状态空间中的“官僚主义”。这与将这些方程视为显式重写规则的方法形成对比。
范围： 作者明确指出，其方法专门针对 $\lambda$ -演算及其变体，利用了范畴模型元理论的内部语言。他们承认槽位 e-graph 在处理具有绑定（如 $\pi$ -演算）的任意形式语言时可能更具灵活性，但认为其方法在 $\lambda$ -演算特定优化方面更为优越。

这项工作并未在文中展示完整的软件实现或经验基准测试，而是将封闭式 e-超图表示定位为未来构建“用于弦图重写的 e-graph”的可靠基础。