The Unrealized Potential of String Diagrams for ZKVMs

树木有害

到本帖结束时，我希望说服读者，存在比抽象语法树更好的语法形式；即图形化的语法。我还会谈到这可能如何影响更好的 ZKVM 设计。

首先，树到底有什么问题？从历史上看，数学中的大多数语言都是使用抽象语法树（或 AST）构建的。在大多数计算机科学语境中，语法的定义假设任何语言中的任何术语都必须像树一样结构化。大多数情况下，这似乎没什么问题，但一个世纪以来，人们不得不发明各种技巧来弥补树的缺陷。

我认为最容易看到这一点的地方是在组合演算中。变量一直是理论中的一个持续问题，人们已经花费了大量笔墨试图对变量，或者说变量名，进行一致的处理。与作用域和遮蔽相关的问题在形式上使数学的句法方面变得复杂，而这些方面通常被我们简单地视为理所当然。

管理它们最早的方法之一是简单地消除它们。由此，我们得到了由摩西·肖恩菲尔克发明的原始组合演算。在过去的世纪中，出于类似的原因，人们发明了概念上相似的系统，例如谓词函子逻辑。这些系统允许人们在不使用命名变量的情况下通过符号操作进行推理，但人们必须花费巨大的努力处理复杂的折纸，才能让树的各个部分进行通信。

消除一阶逻辑中量词创建的变量的另一种方法是关系代数。这个系统非常有趣，并且近年来在很大程度上以编程代数的名义得到了发展。

*图组件和 acyclicity。一项结合精确性和简洁性的练习*

然而，它存在一些明显的缺点。核心的关系代数在表达能力上不如全一阶逻辑。当限制为三个变量时，它与一阶逻辑等价。可以通过手动引入元组的概念，并添加一些描述元组操作（如分裂、投影等）的关系来缓解这个问题。这让人处于与组合逻辑类似的位置，在那里人们被迫使用一种不自然的点无操作符的组合来处理在一阶逻辑中具有变量绑定功能的环境下理所当然的事情。

这是为了变量消除而必须的不便吗？答案是"不"，但似乎历史假设是"是"，因此我们看到了变量绑定器的出现。组合演算的最流行的替代方案是λ演算。在这个系统中，变量不会被消除，而是通过改变语法，允许语法树的叶子节点连接到树中的其他叶子节点。这种修改后的树被称为"抽象绑定树"。这种树出现在很多地方。带有量词的一阶公式也是 ABT 的例子。更早的这种语法例子是积分，它绑定其积分变量。

抽象绑定树是一个更明显的"hack"的例子。这是一个从树到图的不彻底的步骤。ABT 是希望它们是图的树。

ABTs 也带来一些奇怪的概念问题。变量绑定总是作用域化的。这对于量化、积分等有预期语义的内容很重要，但对于 lambda 表达式来说则不太合理。为什么 lambda 演算中的绑定是作用域化的？它只是一个重写系统；只要每个 lambda 绑定都有一个唯一命名的变量，允许所有变量被全局处理是完全一致的。当然，做唯一名称检查有点复杂，但正如后面将要看到的，这是使用树而不是图而导致的缺陷。

量词也存在一些奇怪的作用域问题。在经典的一阶谓词逻辑中，所有量词都可以移到公式的最外层。只要量词的所有变量都在作用域内，量词的确切位置实际上并不重要。从这个意义上说，量词可以被认为相对于公式中不含量词的部分是自由浮动的。然而，树结构要求表达式中的所有元素都必须通过根节点连接，因此量词总是被固定在某个任意位置。树结构常常迫使人们跟踪比实际存在的更多结构。

树木也鼓励那些处理和推理资源时有害的方法。考虑重写规则：

`b(x,y) ↦ x`

`x ↦ b(x,x)`

第一条规则删除任意量的信息，y，而第二条规则复制任意量的信息，x。这些规则完全一致，但无法用这些类型的规则有效捕获资源使用情况。修正这些问题并不难；可以通过对 x 和 y 进行模式匹配，并引入一个中间的复制/解压缩结构来逐个处理组件。这类结构既笨拙又丑陋；但我想要说的是，在处理树结构时最自然、最容易的做法会导致技术债务。

相比之下，这些规则在图形环境中根本毫无意义。不能简单地删除一个 y，因为它可能连接回 x。不能简单地复制 x，因为它可能连接到图形表达式中其他地方的其他事物。要在处理图形时协调地处理删除和复制，必须创建局部重写规则，我们会看到这些规则非常简单。如果我们关心资源，图形迫使我们做正确的事，而树结构则鼓励我们做错误的事。

别再抱怨了。解决方案是什么？嗯，是图，但不仅仅是图。想想把一棵树变成图意味着什么。

*b(x,y) 示例：简单、嵌套、复杂、混合*

如果我们有一个像 b(x, y) 这样的表达式，我们会创建一个标记为 b 的节点，该节点连接到对应于 x 和 y 的图。b 节点还会有一个额外的边指向它出现的表达式的根。在原始表达式中，x 和 y 是有序的，并且明显不同于表达式的根；但在图表示中则不是这样。仅仅使用一个普通图，我们就丢失了重要的结构。因此，我们需要一个每个节点都能排序其边的图。当一个结构化图具有具有特定数量和固定顺序边的节点时，我们将节点的边称为"端口"。这也允许我们在一种合理的方式下推广树文法，方法是限制我们的图仅由具有特定类型端口的节点构建。

*b(x,y) 示例：简单、嵌套、复杂、混合*

这种图就是我在说"字符串图"时脑海中的图。正是在这个意义上，字符串图可以被视为"树状"（树形）语法的"图形化"推广。

*计算机科学家对字符串图的介绍*

实际上，字符串图在实践中往往具有稍微更多的结构。主要是将每个节点的边划分为"源"和"目标"集合，以便每个节点可以充当单形范畴的态射。然而，这对本文来说并非必要，因此我不会过多讨论。

*单形范畴的图形语言综述*

字符串图如何解决树引起的问题

回顾我之前遇到的问题。让我们从删除和重复开始。对于删除，我们需要一个橡皮擦节点 e，以及一条类似以下的重写规则：

*[图示：橡皮擦重写规则]*

这样，橡皮擦可以扩散，扫描并逐步删除遇到的图节点。在实践中，会有一些限制，即橡皮擦的重写操作只有在它与 n 的某个"原则"端口相连时才会应用。这可以防止橡皮擦在存在的情况下简单地删除整个图。

复制稍微复杂一点：

*[图示：复制器重写规则]*

可以将橡皮擦视为一种特殊情况，即复制器正在复制到 0 个子图中。

有了这些，我们就能看到如何改进 Lambda 演算。有了内置的复制器和擦除器，我们只需要在我们的语言中添加线性 Lambda 绑定器。这最终变得相当简单。我们只需要指定代表线性 Lambda 绑定器的节点如何与代表应用操作的节点交互。我们可以将重写 `(λx.y)z ↦ y[x/z]` 转换为：

*[图示：Lambda 应用重写规则]*

这也无法重现命名问题。在字符串图中没有变量的名称。所有变量都变成连接节点的字符串/边，而这些变量通过它们在图中的位置来"命名"。这消除了对名称的需求，而没有消除变量本身。因此，我们完成了组合演算的原始目标，而没有其低效性。

这也消除了不必要的作用域。

*apply(lam(x. f(x)), a) 示例：简单、重复、多绑定、非作用域、复杂*

将这视为一种计算模型，我们得到对称交互组合子和它的变体：

*观察等价与对称交互组合子的完全抽象*

使用字符串图，可以更优雅地展示"无量词"的一阶逻辑。我在引号中加上这个说法，因为量词仍然作为特定的节点结构存在，但底层演算与关系代数非常相似，只是没有点无关语法的低效性。这里无法详细说明，但请参见：

*一阶逻辑的图式代数*

切换到字符串图而不是树也能严格提高表达能力。大多数应用不会注意到这一点，但例如，如果使用树作为其语法的有限自动机的一阶理论，则无法有有限的公理化，但如果使用字符串图，则可以。

*使用字符串图对有限状态自动机进行有限公理化*

字符串图环境是普通代数环境的真正推广。

字符串图为何能高效实现算术化？

是什么让 ZKVM 在算术化方面高效？乍一看，从冯·诺依曼架构来看，这似乎是一项无法逾越的任务。你有一些带有潜在数 GB 内存的 RAM，然后你必须通过时间进行投影，创建一个与空间和时间成乘法比例增长的跟踪。

幸运的是，很容易设计一种缓解这些问题的架构。与其从一个完全明确的状态开始，不如从所有 0 开始。然后，让你的操作码一次只修改一个地址。然后你的跟踪可以是一系列修改，"这个地址变成了这样，因为那个操作码"。需要设置检查以确保正确查找旧值，但这现在与内存大小无关，而仅与时间成比例。由于寄存器可以以更少限制的方式修改，你可能仍然需要在每一步声明它们的值，但这要小得多。

使其高效的原因在于单步计算有固定的工作量。例如在 PLONKish 算术化过程中，我们会将我们的轨迹放入一个大的矩阵中。单步计算的复杂度将决定这个矩阵的宽度。直观上，每一行都需要存储在该步骤中修改的关于状态的所有信息。这迫使我们使用一种计算模型，该模型在单步中不能做无界的工作。

因此，带有 `Sxyz ↦ xz(yz)` 规则的单步复制任意大 z 的 SK 组合子演算是不行的。高度仅仅是轨迹的长度，这是不可预测的。

当然，有很多巧妙的方法可以解决这个问题。最近有人向我指出这种方法，作为用不同于我所建议的方式将组合计算算术化的途径：

EDEN - 一个实用的、SNARK 友好的组合虚拟机（VM）和指令集架构（ISA）

根据我的理解，它使用了一种组合构造方法，该方法利用了树表达式和 Dyck 词之间的同构关系，以更 SNARK 友好的方式将树表达式线性化。我认为使用格路径、避免模式的排列以及其他线性组合对象来创建高维组合结构的有效算术化有很大的潜力。我不想给人留下这种印象，即这篇文章是关于"唯一正确的方法"。我认为它比我所见过的其他替代方案更好，但设计空间中到处都是值得探索的低垂果实。

找到一个好的算术化可以被视为将你的检查适配到尽可能薄的矩阵中的问题。我们有一个结构，D，我们想用谓词，P，来检查它。我们想创建一个部分函数，f，从矩阵中提取一个 D，并设计一个关于矩阵的谓词，P'，使得 `P'(m) ≡ (f(m) is defined ∧ P(f(m)))`。理想情况下，m 的宽度应该相对于 d 的大小是 O(1)，无论这如何定义。当然，我们也希望 P' 等价于一个低次多项式方程，但我现在要忽略这一点。

让我们更深入地探讨一下什么是字符串图。最简单的情况下，我们有一个节点列表，每个节点都有一个端口列表。布线可以从几个方面来描述。通常，端口会被划分为"输入"和"输出"（或"正"和"负"），而布线只是输入端口和输出端口之间的一个双射。如果没有这样的划分，我们也可以将布线描述为端口上的一个自同构，使得没有端口映射到自身。字符串图通常会有额外的结构，但这基本上就是其核心思想。这将字符串图作为一个简单的组合对象来捕捉。

重写规则由两个子图通过边界连接而成。这个边界被重写规则的两边共享。我们可以将重写规则定义为一个三元组，包括输入节点列表、输出节点列表、具有其自身端口列表的边界，以及两个自同构；一个作用于输入端口和边界端口的和，另一个作用于输出端口和边界端口。我们可能还有其他要求，例如没有边界端口映射到另一个边界端口。

给定一组重写规则，我们可以进一步探讨轨迹的形态。轨迹可以被视为一个字符串图，其中重写规则是节点。规则的输入节点成为节点的输入端口，输出节点成为输出端口。端口由节点的类型决定。轨迹是这种类型节点的字符串图，其中布线是一组双射，对于每种类型的节点 t，是在类型为 t 的输入端口和类型为 t 的输出端口之间的一一对应。轨迹的起始和结束网可以被视为没有输入（分别地，输出）端口的节点。在按时间顺序排列重写规则后，我们可以截取轨迹图的一部分，以获取在该时间点上图中节点的图像。

这就是核心数据结构。但这不足以保证跟踪是有效的，但额外的结构检查在重写数量上是渐近线性的。我们可以观察到，我们可以通过跟踪图中的双射来获得跟踪切片中的端口循环。从输入中的一个端口开始，我们可以通过跟踪布线来获得重写输入中相同类型的节点。如果内部布线连接到边界，我们继续沿着布线跟随到输出节点的端口；否则，我们会最终到达输入节点的端口。然后我们继续通过跟踪布线跟随到一个新的重写规则。

如果我们通过根据产生它的重写规则对每个切片中的每个节点进行编号来区分它们，那么所有重写规则的内部布线在所有切片端口之间产生双射。由于我们也可以跟随切片端口之间的跟踪布线，我们得到第二个切片端口之间的双射。通过组合这些双射，我们得到一个新的双射。因为它是在有限集之间的双射，跟随它最终会把你带回到起点。这意味着我们得到了一个端口循环。我们可以想象这些端口周期定义了填充迹图字符串之间空间的纸片的边界。

为了确保跟踪有效，我们必须进行的核心检查仅仅是：每个端口周期中，输入节点之间必须恰好有一次内部布线重写，并且这次重写在端口周期中高于所有其他内容。当这种情况发生时，这意味着重写正在删除一条边。这个检查只是为了确保每条边只被删除一次，并且之后不再发生。根据图表代表的其他内容，可能还有更多关于结构的检查，但这只是开始。

我在这篇论文中解释了在交互组合子的背景下，这看起来是怎样的：

通过交互网在 Halo 2 中对函数程序执行进行算术化

结语：ZKVM 应该做什么？

如今，字符串图已广泛应用于多种领域，包括量子计算、经典物理学、线性代数、逻辑学以及其他许多方面。通过将这些领域各自的字符串图形式进行算术化，可以创建通用的电路。通过这种方式，我们可能会获得超越仅执行程序的可验证陈述的概念。

作为未来项目的一部分，我计划描述一个用于全一阶逻辑的 ZKVM，其中电路编码了命题的证明。在这样一个设置中，普通的程序追踪可以被表述，但我们有自由进行更广泛的逻辑推导。在定义智能合同时，我们通常想要表达的是命题。将这些命题转化为程序追踪验证是可行的，但这只是设计空间的一部分，可以进一步扩展。

这一想法在一些其他工作中得到了探索，例如在通用真理框架中使用匹配逻辑。在我看来，使用字符串图，我们有多种选项来表述逻辑和代数，这种方式更自然地适用于创建通用电路。

关于字符串图作为语法形式的学习，请参阅相关论文及后续研究。

🔗 相关资源

• •字符串图理论基础：深入理解字符串图的数学基础
• •ZKVM 设计原理：零知识虚拟机的架构设计
• •算术化技术：将计算转换为电路的方法
• •交互组合子：函数式编程的图形化表示

💡 关键洞察

1. 树结构的局限性：传统抽象语法树在处理变量绑定和资源管理方面存在根本缺陷

2. 字符串图的优势：提供了更自然、更高效的语法表示方法

3. 算术化的关键：固定宽度的计算步骤是高效算术化的基础

4. ZKVM 的未来：超越程序执行，支持更广泛的逻辑推理

🎯 技术影响

字符串图不仅解决了传统语法树的问题，还为构建下一代 ZKVM 提供了理论基础。通过将各种数学领域的字符串图形式进行算术化，我们可以创建真正通用的零知识证明系统，支持从程序执行到逻辑推理的广泛应用场景。