机器编织的代数语义 (Algebraic Semantics for Machine Knitting)

文章元数据

作者 Nat Hurtig 发布日期 2025年3月31日

作为编程语言研究人员，我们在编写和分析语言时，有权要求一定的数学严谨性。编程语言具有 语义 ，即语言中语句含义的定义。我们可以使用这些语义来做各种有用的事情，比如错误检查、高效编译、代码转换等等。

这篇博文是关于一个编程领域，该领域在其语义方面尚未享有同等程度的严谨性：机器编织。人们编写程序来控制大量的针阵列，这些针阵列将纱线操作成有用的 3D 对象。在这篇博文中，我将介绍为机器编织寻找“正确的”语义的过程，涉及我们为什么需要语义、与传统编程语言的联系，以及我们将来可能将这些语义用于什么。在我们的搜索中，令人惊讶的是，编程语言之外的研究领域多次客串：代数拓扑、群论、纽结理论、范畴论，甚至量子计算！

我将用一个玩具问题来激发语义：两个给定的语句可以彼此交换吗？这是一个他们可以交换的例子：

x = a + b;
y = c + d;

“交换”的意思是，如果我交换了这些行的顺序，程序会做同样的事情。交换问题很重要：编译器可能会移动指令的顺序，通过批量处理相关指令来优化内存使用；分析器可能想看看两个程序是否等价；我们可能还想知道是否可以并行运行两个指令。在上面的例子中，我们知道这些语句可以交换，因为这些语句隐含了 语义 ——它们没有任何共同之处，所以不应该互相影响！

这里有更多的例子。这些语句不能交换，因为存在数据依赖性：

x = y + 4;
y = c + d;

如果我们交换这两个语句，赋值给 x 的语句将使用 y 的一个可能不同的值。

非交换语句可能因为直接数据依赖性以外的原因发生。想象一下，我们在 C 语言中——这些函数调用可以交换吗？

x = f(a, b);
y = f(c, d);

我们不能确定它们可以交换——也许 f 函数每次被调用都会改变某个计数器变量。

除了显式的可变状态之外，还有一种类似 C 的东西通常会阻止交换：

*x = *x + 3;
*y = *y * 2;

如果 x 和 y 指针相同，这些语句就不能交换。

值得注意的是，在 纯 函数语言中，没有隐藏的可变状态或指针别名。Haskell 是一种流行的语言，它非常接近纯函数语言——因为它支持像打印到控制台和读/写文件这样的 IO 操作，所以它不是纯的。在 Haskell 中，这些函数 可以 交换，只要没有 IO monad 的捣乱：

x <- f a b
y <- f c d

Haskell 的交换结果与 C 不同，原因是它们的语义不同——任何时候我们想要证明一个语言行为的属性，我们都必须求助于该语言的语义。我们知道，证明机器编织程序的属性可能是一个强大的工具：一篇 2024 年的论文 展示了使用优化编译器的大幅加速，仅使用了几个 直观上 正确的程序转换。为了扩展该结果并证明编译器的准确性，我们需要开发机器编织的语义。

机器编织背景

此介绍仅适用于与此博文相关的机器编织的细节。不幸的是，从纱线线轴自动创建有用对象的机器背后的机制非常复杂！如果您想阅读更多关于机器编织的内容，这篇论文 有一个很好的介绍。

编织机有一个由数百根针组成的阵列，称为针床。这类似于传统计算机的内存——寄存器保存值，而针保存纱线环。还有 载纱线 在机器中移动，穿过、围绕和经过针的环，以创建 线圈 ，我稍后将它与传统编程语言中的基本操作进行比较。以下是在编织中形成基本线圈的方式：

一个在环左边的青色载纱线 载纱线已被拉过环，创建了一个新的青色环 一个框被绘制在之前图像的一部分周围；该线圈使用一个青色载纱线和一个金色环，并返回一个青色环和一个青色载纱线

载纱线（青色）被拉过一个环（金色）以创建一个新的环。注意底部的金色环是如何保持原位的，只要顶部的青色环和载纱线被抬起。在线圈之后，编织机放下底部的环，但底部的环保持连接和稳定。这就像一个值超出范围，但由于某些范围内的值指向它，它不会被垃圾回收（重力是机器编织的垃圾收集器！）。

有很多线圈的变体，但它们都遵循相同的输入-输出模式：环和载纱线输入，环和载纱线输出。这样，它们有点像我们在计算机科学中使用的基本操作，如加法或按位 AND：值输入，值输出。上面的第三张图片在线圈周围画了一个框，以显示其输入和输出：载纱线和环输入，环和载纱线输出。

机器编织中还有一项技术细节：为了执行涉及某些值的线圈，这些值必须彼此相邻。在下面的示例中，我们不能立即将最左侧的青色载纱线与最右侧的金色环编织在一起——相反，我们必须在创建线圈之前将这些值移动到彼此相邻。

一个青色载纱线、红色环和一个金色环 青色载纱线越过红色环，并与金色环做一个线圈

对于传统的计算来说也是如此——为了计算两个比特的布尔 AND，我们需要将这两个比特连接到一个 AND 门，使它们紧挨在一起。计算机架构师使用像多路复用器这样复杂的路由机制来做到这一点；当我们在传统的编程语言中编码时，我们不必担心这些约束，因为计算机架构师已经慷慨地为我们处理了它。

用于机器编织的语言不包括许多使代码难以分析的传统编程语言功能：没有 if 语句（分支）或 for 循环，也没有函数。机器编织代码只是一系列执行线圈和移动载纱线和环的操作。这应该使分析机器编织更容易：与传统编程语言相比，复杂性要小得多。事实上，对于我们关于两个操作是否可以交换的特定问题，这个问题似乎几乎是微不足道的：与纯函数式编程语言类似，机器编织中没有全局状态或别名。然而，机器编织中隐藏着一些棘手的东西，这在传统的计算环境中并不令人担忧：由于编织是在 3 维中完成的，当线交叉时，一个在线的上面，另一个在线的下面。这会导致操作相互阻碍，即使没有线直接连接它们。我将用一些图表来说明这一点。

图表

让我们首先仔细分析传统计算的核心内容：组合布尔电路。这是一个简单的示例 myfunc，它将 3 个比特映射到 3 个比特。

fn myfunc(x1, x2, x3) {
  y1, y2 = dup(x2); // 将导线分成两根
  y3 = and(x3, x1);
  return y1, y2, y3;
}

当电路被绘制出来时，通常更容易推理（请原谅我在绘制图表时所做的非常奇怪的选择；一旦我们开始编织，一切都会变得清晰）：

上述代码的电路图

我提出同样的问题：dup 和 and 操作可以交换吗？在这里，答案是肯定的：不存在全局状态和别名，也没有数据依赖性。这是同一个函数，但操作被交换了：

fn myfunc(x1, x2, x3) {
  y3 = and(x3, x1);
  y1, y2 = dup(x2);
  return y1, y2, y3;
}

上述代码的电路图

确定组合电路中的两个操作是否可以交换很容易——当且仅当没有连接它们的有向路径时，它们才可以交换，就像只要 Haskell 中的两个函数之间没有数据依赖性且没有 IO 技巧，它们就可以交换一样。

编织图

现在，让我们为编织尝试类似的事情。为简单起见，我们将使用一种虚构的机器编织语言，该语言隐藏了对这篇文章并不重要的一些技术细节。我们的编织函数以三根线作为输入，执行两个线圈，并返回三根新线。我冒昧地简化了图表，没有绘制线圈的“内部结构”（现在它们只是盒子），并且我将环和载纱线都绘制为单根线。

fn myknit(s1, s2, s3) {
  t1, t2 = stitch1(s2);
  cross t1 over s1;
  cross s3 over t2;
  cross s1 over s3;
  t3 = stitch2(s3, s1);
  cross t2 over t3;
  return t1, t2, t3;
}

上述编织代码的图表。stitch1 和 stitch2 盒子没有被一根线直接连接，但由于线交叉的方式，没有办法将 stitch2 移动到 stitch1 下面

嗯，这个图看起来几乎与电路图相同，但是现在每次两根线交叉时，我们都必须指定哪一根在线的上面。这在代码中尤其明显：线之间的所有交叉都列出并注释。我们小心地记录和显示机器编织中的这些上下交叉，因为它们是在物理介质中工作的一个特性：线交叉的方式会影响编织对象的外观和感觉，并且它会彻底改变最终对象的形状！

这些上下交叉是使机器编织的交换问题变得困难的原因。在上面的示例中，两个操作之间没有数据依赖性（即，没有连接线）。然而，由于它们的线交叉的方式，这些操作“阻碍”了彼此，因此它们无法交换。对于人类来说，很容易查看上面的图并决定两个操作是否相互阻碍，但是我们如何编写一个准确的算法来对这些事情应用自动分析？我们需要某种方法来形式化这些想法，以便计算机可以对它们进行推理……啊哈，就是我们之前提到的那些语义。

现在是时候提到实际上存在机器编织的语义：一篇 2023 年的论文 为所有机器编织设置了严格的数学语义。然而，这些语义是在纽结理论的 tangles 中定义的。这是定义编织对象的自然方式——它们确实是 3D 空间中的一团线！然而，纽结理论的等价性是由连续变形定义的——只要我们可以拉伸、移动、展开和收缩一个纽结到另一个纽结中而不撕裂线，两个纽结就是等价的。由于目标是编写分析机器编织的计算机程序，因此提出的语义对计算机没有直接用处。计算机没有任何“连续变形”的概念，并且它们特别不擅长做任何涉及连续量的事情。这些语义对人类进行基本的手写证明很有用，并且是一个很好的起点，但是我们希望扩展它们，以便我们可以使用计算机执行自动分析。

题外话：量子计算

应该注意的是，如果我们通过将导线插入有形的逻辑门来实际构建早期的组合电路，我们也必须为每个交叉点做出一些决定，即哪根导线在上面。然而，这根本不是计算机科学家关心的问题：哪根导线在上面并不重要，因为电子不关心它们是在其他电子之上还是之下——它不会改变产生的计算。

量子物理学中的模型允许一些粒子 会 记住它们是如何上下穿过的。这可能对量子计算产生重大影响，其中使用这些粒子的所谓的拓扑量子计算机可能比传统的量子计算更耐退相干。微软的一个团队 最近发表了一些关于拓扑量子计算的实验结果，使用一种设置将准粒子在 2+1 维空间和时间中编织在一起。方法、设置和目标当然与机器编织不同，但是看到机器编织和量子计算这两个看似无关的主题被相似的数学思想联系在一起，真是令人满意。

将我们的拓扑代数化

正如我之前暗示的那样，我们希望形式化之前的图表，以便我们可以研究它们的属性，使用比纽结理论更易于计算机使用的东西。实际上，这是一个代数拓扑的练习——用代数来表示拓扑（比如我们 3D 空间的变形），这更容易处理。 辫群 是数学家如何用代数表示拓扑对象的一个很好的入门示例。

辫群

对于熟悉群论的人来说，n 根线的辫群是

Bn=⟨σ1,…,σn−1|σi;σi+1;σi=σi+1;σi;σi+1,σi;σj=σj;σi⟩

对于 |i−j|≥2，它表示在环境同痕下的 n 根线的等价类。对于那些被这一大堆符号搞糊涂的人，请继续阅读！

群是一组元素 G={x1,x2,…}，其中

  1. 有某种 组合 或 构成 元素的方法，我将用分号表示。对于任何 x,y∈G，我们有 x;y∈G。
  2. 有某种代表“无”的单位元。我们将该元素称为 id∈G，它具有属性 id;x=x=x;id。
  3. 有某种 反转 元素的方法：对于任何 x∈G，存在一些 x−1∈G，其中 x;x−1=id=x−1;x。

我们都熟悉的一个群是加法下的整数：整数的构成是加法，单位元是 0，反转是取反。

对于任何自然数 n（假设 n=5），n 根线的辫群 是这些群之一。该群中有无限个元素，每个元素都是 5 根线，从下到上定向，相互上下穿过。最好将辫子视为在两端钉住或粘住，并且只要可以通过移动线、保持钉住的末端固定，将一个辫子转换为另一个辫子，两个辫子就是 等价的。以下是 5 根线上的两个辫子的示例；我将左边的那个称为 x，右边的那个称为 y：

辫子 x = sigma_1^{-1} ; sigma_2 ; sigma_1 ; sigma_3^{-1} 在 B_5 中 辫子 y = sigma_2^{-1} ; sigma_1 ; sigma_3^{-1} ; sigma_4 在 B_5 中

接下来，我们将定义什么是构成、单位元和逆元：

构成是垂直连接，从下往上阅读。因此 x;y 是将 x 粘贴在 y 的下方，并且线按顺序连接：

辫子 x = sigma_1^{-1} ; sigma_2 ; sigma_1 ; sigma_3^{-1} ; sigma_2^{-1} ; sigma_1 ; sigma_3^{-1} ; sigma_4 在 B_5 中

辫群中的单位元只是 n 根线直线向上：

5 根垂直的线，没有交叉

通过垂直连接来定义构成，希望我们可以同意在任一端粘贴单位元实际上不会改变任何东西，因此该辫子确实是单位元。最后，逆元是关于辫子中间水平线的镜像图像——下面是左边的 x 和右边的 x−1：

辫子 x = sigma_1^{-1} ; sigma_2 ; sigma_1 ; sigma_3^{-1} 在 B_5 中 辫子 x^{-1} = sigma_3 ; sigma_1^{-1} ; sigma_2^{-1} ; sigma_1 在 B_5 中

当我们构成 x;x−1 时，我们得到一个可以解开的辫子，即单位元：

辫子 x = sigma_1^{-1} ; sigma_2 ; sigma_1 ; sigma_3^{-1} ; sigma_3 ; sigma_1^{-1} ; sigma_2^{-1} ; sigma_1 在 B_5 中

这一切都很好，但是我们需要某种方法来写下辫子，以便计算机可以使用它们。我们将通过按顺序（从下到上）列出它们的交叉来做到这一点。我们将使用 σi 来指代从左侧数第 i 根线越过第 (i+1) 根线，并使用 σi−1 来指代在下面。然后我们可以将辫子 x 写成 x=σ1−1;σ2;σ1;σ3−1。

还有一个复杂的问题：有多种方法可以写下辫子。例如，我们可以将 x 写成 x=σ1−1;σ2;σ3−1;σ1 代替——这里是左边的原始 x 图和右边的新图：

辫子 x = sigma_1^{-1} ; sigma_2 ; sigma_1 ; sigma_3^{-1} 在 B_5 中 辫子 x = sigma_1^{-1} ; sigma_2 ; sigma_3^{-1} ; sigma_1 在 B_5 中

x 的此图和原始图是等价的——通过上下移动交叉，我们将一个交叉转换成另一个交叉。因此，辫群具有额外的关系来解释这一点：σi;σi+1;σi=σi+1;σi;σi+1 和 σi;σj=σj;σi。以下是绘制出的那些关系，左侧和右侧在每一行中都相等：

一根红色的线越过一根青色和绿色的线，然后青色越过绿色 青色越过绿色，然后红色越过绿色和青色 红色在青色之上，然后绿色在紫色之上 绿色在紫色之上，然后红色在青色之上

物理学说明：第一个方程被称为 Yang-Baxter 方程，它出现的地点比辫群要多得多！

应该注意的是，关系 σi;σi−1=id 隐含在所有群中：

一根红色的线越过一根青色的线，然后从另一侧越过青色的线 红色和青色的线没有交叉

现在，我们应该对辫群达成共识：符号

Bn=⟨σ1,…,σn−1|σi;σi+1;σi=σi+1;σi;σi+1,σi;σj=σj;σi⟩

对于 |i−j|≥2 告诉我们如何用 σ1,…,σn−1 写下辫子，以及哪些词表示相同的东西。

人们对辫群进行了充分的研究，并带有了一些强大的算法。该表示可以在多项式时间内规范化，这意味着我们可以运行一些算法来有效地判断使用 σi 写下的两个辫子是否等价。对于我们关于机器编织的可计算语义的目标来说，这是一个很好的信号——数学家们已经采用了一个拓扑对象，该对象具有我们想要在机器编织中构建的许多结构，将其归结为计算机友好的东西，甚至编写了一些有用的算法！然而，辫群只能表示没有线圈的机器编织程序的一部分。线圈像作用于线的函数一样运行，带有输入和输出线。输入的计数可能与输出的计数不同，从而改变了我们在执行线圈时线的计数。辫群仅限于一些固定的 n 根线，因此它无法表示线圈。为了获得机器编织的完整图像，我们将需要概括我们的数学假设，以包括代表线圈的盒子。

幺半范畴及其图表

在编程语言研究中，范畴论最著名的是类型论研究。我已经用完了这篇博文中的所有数学津贴来解释辫群，因此我不会涉及什么是范畴的本质细节——简而言之，它是一个代数对象，如群，但更通用：构成不一定总是定义，并且逆元不一定总是存在。

特别值得注意的是 内部逻辑 和范畴的内部语言的思想：范畴、某些逻辑和某些理论编程语言模型之间的对应关系。Curry-Howard 对应 描述了逻辑和编程语言之间的连接，这些思想将范畴论添加到其中。

一种这样的对应关系存在于 线性逻辑 之间，其中值只能使用一次且必须使用一次，以及 对称幺半范畴。所有范畴都具有构成，我将其解释为垂直连接，如辫群中那样；此外，幺半范畴还具有水平连接（如多个值在范围内、按顺序运行两个电路或保存环的针阵列）。对称幺半范畴可以绘制为由线连接的盒子，其中线的交叉的上下不记录或绘制：正是我们为组合电路绘制的图！对称幺半范畴为我们提供了符号和公理，以严格地研究这些电路，就像辫群为我们提供了符号和公理以研究辫子一样。 对称 幺半范畴是一个很棒的名字，因为它与对称群密切相关。

按照同样的想法，编织幺半范畴 通过记录上下交叉来概括对称幺半范畴，我们像这样绘制我们的图——就像我们的机器编织图一样！早在 1991 年，当编织幺半范畴还很年轻时，Joyal 和 Street 表明，编织幺半范畴的公理与我们用于它们的图的拓扑相对应。由于我们的图确实代表了物理拓扑对象，这意味着编织幺半范畴非常适合机器编织！

实际使用这些语义

现在我们已经确定了机器编织的代数结构，我们希望使用该形式主义来对机器编织程序执行有用的分析。一个直接的目标是程序等价：给定两个机器编织程序，它们是否会产生相同的对象，直到拓扑等价？我们可以将这些程序简化为它们的编织幺半范畴表示，并使用它们。这与我之前提到的辫群规范化密切相关——我们可以将其扩展到编织幺半范畴吗？我已经开发了一种可以在多项式时间内完成此操作的算法，但是它太复杂了，无法放入博文中。借用费马的一些语言，我 发现了一个真正了不起的算法和正确性证明，而这篇博文的页边距太窄，无法容纳。该算法通过使用一些新思想来规范化线圈的位置和顺序来工作，然后使用辫群规范化来规范化线圈之间的交叉。

我们可以使用规范化算法来编译和优化机器编织程序。范式对于编译器来说很重要，因为它们可以大大简化要编译的语言——规范形式在此基础上增加了唯一性保证。编织幺半范畴的公理精确地列出了我们应该考虑的所有程序转换。最后，我也对开发一种面向用户的机器编织编程语言感兴趣，该语言更接近于范畴论提供的抽象。当前的机器编织语言与控制编织机紧密相关，因此它们要求用户指定机器上的哪些针保存线（就像汇编需要用户指定哪些寄存器使用值一样）。除了可用性之外，一种新的编程语言还可能具有性能、制造可靠性或程序模块化的功能。

非常感谢我在 UW 的导师 Gilbert Bernstein 和 Adriana Schulz，因为作为一名一年级博士生，我通过机器编织的视角学习了范畴论和拓扑。这项工作部分是与目前和以前在 CMU 的人员合作完成的，包括 Jenny Lin, Tom Price, Jim McCann, 和 Hannah Fechtner.

延伸阅读

  1. KODA, 优化编织编译器
  2. 拓扑机器编织语义
  3. 微软在拓扑量子计算方面的实验进展
  4. 关于辫群的 Wikipedia 文章
  5. nLab 上关于内部逻辑的页面
  6. Joyal 和 Street 的论文，连接了范畴论图表和拓扑

关键词:

返回到博客文章... 在 GitHub 上编辑 — Computer Science & Engineering 在 University of Washington