𝜆-calculi和函数计算的弦图

𝜆-calculi和函数计算的弦图

String Diagrams for 𝜆-calculi and Functional Computation

https://arxiv.org/pdf/2305.18945

摘要：

本教程给出了关于用于高阶计算的弦图和图语言的高级介绍。主题内容以原则性的方式展开，从关键范畴论概念（如函子、伴随和严格化）的二维语法开始，直至笛卡尔闭范畴，后者是λ演算和函数式编程语言的核心数学模型。这种方法论逆转了从语法进展到范畴论解释的常规方法，而是通过从范畴模型理性地重构语法。结果是一种图语法——更确切地说，是一种分层超图语法——其在许多方面被显示为优于传统的线性项语法。教程的其余部分专注于与编程语言相关的应用：操作语义、类型推断的通用框架，以及复杂的整个程序变换，如闭包转换和自动微分。

关键词：弦图；幺半闭范畴；笛卡尔闭范畴；高阶计算；λ演算；操作语义；程序变换；函数式编程

1 引言

编程语言的语法表示，自然语言更是如此，需要复杂的数据结构。当编写程序、程序规范或编程语言的语法模型（例如操作语义或抽象机）时，习惯以其序列化形式部署语法：一种线性的符号序列，我们称之为文本，或者使用更专业的词汇，称为项。然而，就算法目的而言，项是一种笨拙的数据结构。因此，编译器和其他编程语言工具从不直接处理项，而是通过称为词法分析和解析的过程，立即将它们转换为更有用的数据结构。最常见（即使不是最复杂）的被称为抽象语法树（AST）。

普遍认为，抽象语法树虽然比项有所改进，但远非表示语法的理想数据结构。各种基于图的替代方案已被提出，其中一些已在生产编译器中实现。此类数据结构归于中间表示（IR）的一般标签下。用于表示语法的数据结构的设计空间很大。健全的方法论要求中间表示最好以原则性的方式推导出来，源自更一般的数学概念，并在需要时由实际考虑因素加以指导。

本教程以弦图作为起始数学概念，并展示它们在表示和推理程序方面的效用。弦图起源于范畴论，作为幺半范畴态射的二维（图形）语法。尽管在文献中弦图常与其作为图的具体组合表示混淆，但我们发现保持这种区分并坚持前者是语法（即使是二维或平面的）是有益的。这使我们能够分离出源自弦图语法的中间表示：这些被称为分层超图，并具有独特有益的理论和算法属性。

在图 1 中，我们作为预告展示了我们在后续中将处理的弦图类型。具体而言，它代表了λ演算中柯里化和反柯里化的组合。不过多剧透，在此图中，线代表变量，框代表操作；圆角框是 thunk，它们的绑定变量是附着在框架上的线。

大多数数学语法是一维的或线性的，所以人们可能会合理地问二维弦图语法是否有任何优势。看待这个问题的一个方法是观察语法与其上成立的方程之间的关系。一维语法可以吸收结合律的商化，从而减少括号的不愉快使用。

这提出了一个比较记号法的标准：如果一个记号法能吸收更多的方程，那么它就更好。我们的意思是，在改进后的记号法中，两个项变得在语法上相等，从而不再需要使用显式的方程来标识它们相等。平面记号法相较于线性记号法还有一个额外的优势，即它能使某些记号不变量变得显而易见。例如考虑矩阵，它们最常以二维语法书写：

要么写作行的列表。所有列（或分别为行）具有相同大小这一关键不变量不再由记号强制执行：在平面记号中，不可能写出具有不匹配的行或列的矩阵。

这提出了比较记号法的另一个标准：

优越的记号法吸收更多的不变量，使得格式错误的项无法被这样写出。

矩阵的平面记号法还吸收了等式性质，例如转置是对合这一事实。

在更复杂的语言的情况下，带有变量和绑定，从线性语法转向平面语法可以吸收更多这样的等式性质。考虑以下的项，其中 let 引入并绑定一个变量：

这些项都是等价的。前两个项之所以等价，是因为绑定变量可以被系统地重命名，即 x 变为 u，y 变为 v。第二个和第三个项之所以等价，是因为互不依赖的定义可以交换。在线性语法中，这些等价性都不明显。第一个是众所周知的 α 等价，第二个则是带有显式替换的演算中较不为人知的图等价。在数学上处理这些等价性并不困难，但困难之处在于它们应当是同余关系，也就是说，项需要按照这些等价关系进行商化，使得定义应用于项的等价类而非项本身。另一方面，正如我们在后文中将看到的，在二维图语法中，所有这些项将对应同一个图，或者更确切地说，对应同构的图，即：

在这种表示中，绑定变量是图边，而常量和操作是框，因此直观上应该很清楚，图同构吸收了我们上面提到的两种等价性。

为了结束这次关于二维语法的简短偏离，希望现在可以接受从线性转向平面具有某些非平凡的优势。然而，从语法表示转向组合图状表示将具有更进一步、更深层的优势，我们将在本教程的其余部分探讨这些优势。不过，项、弦图和图并没有完全相互取代。它们都是有用的语法形式，适用于不同的目的。

1.1 语法三位一体主义

本教程的最终目标是说服读者接受一种新的、多层面的语法愿景，我们（相当宏大地）称之为语法三位一体主义：项、弦图、图。它们最终都是某种抽象的、如果你愿意可以说是柏拉图式的语法理想的可互换表示，各自扮演着不同的角色：

项。尽管图形语法具有明显的吸引力，特别是对初学者而言，项语法仍然是正式写作的主力，无论是编程、数学还是逻辑。符号的串行序列，容易被大脑分组为标记，环绕页面末尾，饰以空白和字体变化，仍然是正式文本经过检验的存储库。我们人类在这种表示法上的便利能力，可以说可以追溯到语言本身最初作为一种口语交流形式的演变：一种听觉符号的串行序列，饰以音高和音调，由音量和速度调节。从几十行的学生项目到数百万行代码的软件基础设施（如操作系统或编译器）等各种程序，都可以使用这种格式编写、理解（在某种程度上）和演进。尽管有种种缺点，但语法仍将长期存在。

图。算法在项上运行得不太好。它们是一种笨拙的数据结构。但图是高效的，与列表般的项相比，允许更多样化的结构。它们可以表示共享，并且可以通过跟随边允许从一个区域到另一个区域的快速访问。然而，更具表现力的结构是以概念成本为代价的。当修改图时，保持正确的不变量是困难的。编写算法和推理图的属性更加困难，因为它们缺乏归纳结构。甚至为一个问题想出正确的图结构也是困难的，因为设计空间可能很广阔且没有明显的约束。

弦图。项和图之间的概念桥梁是弦图。作为一项新发展，根植于理论物理和范畴论，弦图理想地适合此目的。它们在某种意义上是语法的，即它们可以由文法生成，但它们是二维的而不是线性的，就像矩阵的标准记号是一种二维语法一样。二维语法，如果以某种方式书写，使得图表示直观且其形式化不足为奇。

连接弦图和图的特定概念是叶状化（foliation），我们将在第 2.6 节专门讨论此概念。一个弦图的叶状化是通过首先将其表示为图，然后将该图重新表示为特定形式的弦图而获得的，我们可以将其视为一种准范式。这些不是真正的范式，因为它们不是唯一的，但它们有助于极大地简化弦图的结构，最终允许在本质上非归纳的数据结构上制定归纳算法。这些算法效率不高，但可以使用方便的归纳方法进行推理。此外，这些算法本质上是可执行规范，可以进一步细化为高效的图算法。

我们的表述假设读者对相关范畴论概念有基本理解，特别是为了激发整个项目的动机。对编程语言理论基础（例如操作语义和抽象机）以及基本编译器开发的一些理解，应能进一步增强对内容的领会。尽管有理论基础，但此处的表述应能引导读者实际理解分层图作为一种现实且有用的数据结构，用于在编译器、解释器和程序分析工具中表示语法。

表述的风格既不是纯粹理论的也不是纯粹实践的，而是一种“技术转移”。具有范畴论背景的读者应该能够找到真正的实际应用，希望这将启发他们的工作并允许他们与编译器编写者交流和协作。具有编译器开发背景的读者应该发现自己被提醒使用范畴论的可能性，不仅作为语义框架，不仅作为类型论框架，而且作为语法框架。最后，本作旨在作为教程阅读，而非综合综述或参考手册。为了最小化干扰，我们将把所有参考文献和讨论留到特殊的子章节中。

表述的结构是线性的，建议读者逐节进行。我们从第 2 节弦图的一般介绍开始，其中我们关注一些在标准文献中通常被忽视的结构，特别是伴随和严格化，但它们对于处理闭幺半结构是必不可少的。在此基础上紧密构建，我们在第 3 节介绍闭幺半范畴和笛卡尔闭范畴的弦图，并立即应用于λ演算的语法和等式理论。弦图的二维语法和图重写直觉之间的联系在第 4 节中被精确化。第 5 节将转向λ演算的操作语义，纯的但也扩展了操作进入更实用的编程语言。最后，在第 6 节我们给出弦图的三个非平凡应用：类型推断、闭包转换和反向自动微分。可以说，它们将提供一些证据，表明弦图导致了一些已知算法的更清晰和更有洞察力的版本，这些算法在它们基于项的表述中，被认为有时极其复杂。

1.2 进一步阅读与相关工作

我们仅就语法和中间表示方面提及一些相关工作。还有更多相关工作我们在此不会提及，因为它们将在后续章节中更详细地讨论。

使语法成为具有更好算法属性的数据结构的最早且最具影响力的方法之一是 de Bruijn 的"无名虚拟变量"，被广泛称为"de Bruijn 索引"（De Bruijn, 1972）。在这种记号法中，变量名被自然数替换，这些自然数使用一个考虑绑定器深度的确定性方案进行分配。这种记号法在λ演算的形式化中被广泛使用，但它有一个缺点：变量需要在应用之后重新索引。这是其非组合性的一个症状，因为整数分配方案对整个项而言是全局的。

对于语法的表示，有两种替代方法具有重要意义。第一种方法由 Pitts、Gabbay、Urban、Cheney 等人推广，基于所谓的"名义技术"（nominal techniques）（Pitts, 2013）。这里的关键目标是使按α等价的商化与递归定义和归纳证明相协调。这一目标是通过将名字作为一种数据结构引入来实现的，该数据结构仅配备两种操作：一种是局部的，用于测试相等性；另一种是全局的，用于生成一个新名字。因为名字除了其身份之外不可区分，所以被称为"原子"（atoms）。一个重要的结果是，名义数据结构是"等变的"（equivariant），这意味着如果底层原子被系统地改变，那么两个元素是不可区分的。

基于图的表示也隐式地是等变的，因为图同构涵盖了节点和边的实际身份的等变性。然而，名义技术为绑定提供了一个很好的语法模型，这在图表示中并未出现，因为在图表示中似乎并不需要它。弦图表示提供的不是名义表示所支持的标准结构归纳或递归，而是一种在"叶状化"上进行归纳或递归的新方法。

另一种语法方法是"高阶抽象语法"（HOAS）（Pfenning & Elliott, 1988）。这是一种在使用本身支持绑定的元语言时，将绑定概念纳入抽象语法树的方法。这对于将编程语言编码到（例如）证明检查器中很有帮助，但作为数据结构使用并不理想，而我们的目标是将其用作编译器中的中间表示。HOAS 和 de Bruijn 记号法互为补充，可以一起使用（Hickey, Nogin, Yu, & Kopylov, 2006）。

编译器中中间表示的方法与使用 de Bruijn 或 HOAS 记号法截然不同，这表明了理论与实践之间的裂痕。有时还存在"中间表示"和"中间语言"之间的混淆，我们将在继续之前澄清这一点。前者是一种（编程）语言，并非供人类程序员使用。它要么是对象语言的激进去糖化，例如 OCaml 的 FLambda 中间语言的情况（Leroy et al., 2022），要么是对汇编细节的抽象，例如 LLVM 的情况（Lattner & Adve, 2004）。在这两种情况下，中间语言都具有大大简化的语法，这使得规范不那么繁琐。

相比之下，中间表示（IR）是一种数据结构，其中最简单的是抽象语法树（AST）。AST 相当简单，例如缺少直接共享的任何概念，并且依赖于复制或辅助数据结构（如符号表）。图表示将所有这些统一在一个方便的单一数据结构中。基于图的 IR 以前在商业编译器中已取得一定成功（Click & Paleczny, 1995），有时被称为"节点之海"（sea-of-nodes）表示（Paleczny, Vick, & Click, 2001），但它们很少得到应有的重视。例如，在机械证明助手中形式化中间语言相对常见（Zhao, Nagarakatte, Martin, & Zdancewic, 2012），但我们不知道有将基于图的 IR 理论作为数据结构进行形式化的努力。尽管我们在此不呈现，但形式化弦图的图表示的工作正在进行中。请注意，必须在 IR 与编译器中使用的其他基于图的表示（如控制流图（CFG）和静态单赋值（SSA）或寄存器分配算法）之间做出重要区分。

最后，需要特别致谢"交互网"（interaction nets），这是一种使用图重写来给出操作语义的编程语言的图形表示（Lafont, 1990）。交互网与我们的弦图之间唯一但本质上的区别在于，前者是扁平的，而后者是分层的。我们将在后文看到，当涉及表示编程语言中常见的绑定结构时，扁平结构为何会有问题。

2 弦图

我们假设读者熟悉范畴论和弦图的基本概念，因此在本第一节中我们将快速浏览材料，仅强调那些特定于本次表述的方面。对于需要更入门级的范畴论表述的读者，有许多教程可供起步，其中许多面向计算机科学家（Pierce, 1991）。特别相关且有用的是关于弦图的教程介绍，参见非常近期的（Piedeleu & Zanasi, 2023）和经典的（Selinger, 2011）。

2.1 范畴及其图形语言

因为复合运算是结合的，所以在书写更复杂的复合运算时省略括号是可以接受的，例如

更具体地说，如果使用无括号形式 f;g;h;i;j，我们如何插入括号并不重要，因为所有的加括号方式都会产生虽然在句法上不同但相等的表达式。因此，无括号表达式代表了按结合律商化后的句法项的等价类。这是数学中针对结合运算非常常见的一种句法技巧，我们自动地使用它，而未曾深思。但是，利用记号约定根据其语义对句法对象（项）的类进行商化的想法是很吸引人的，因为它不可避免地导向更简单、更抽象的记号。在这种情况下，我们说该等价性被记号吸收了。问题是：我们能将这一思想推广到其他句法结构吗？使用即将介绍的弦图，答案是明确的“是”。

定义 2.3 范畴 CC 的图形语言是

图形语言是一种无括号的语法，因此它通过构造预设了复合运算的结合性。正如我们很快将看到的，在图形语言中可以使用括号的等价物（框）来进行消歧。然而，我们的目标仍然是尽可能避免这样做。减少对括号或框的需求是良好语法的标志之一。

这是对我们要耍的一个花招可以提出的有效异议。我们没有具体说明弦图应该如何具体表示。在这个阶段，答案将是非正式的。将图形语言形式化为组合对象是可能的，它将捕捉到这样的直觉：它们是类图对象，具有明确定义（尽管是隐藏的）接口，位于图的右侧和左侧，锚定那些看起来像“悬空”的线。作为图，这些对象将按照适当定义的同构概念进行商化，这使得线的长度和其他属性变得无关紧要，仅关注连通性。这就是为什么上面三条长度递增的线在解释中都是相等的，因为它们可以被形式化为同构的类图结构。我们认为这些形式细节主要是一种合理性检查，因为它们精确地描述了所需的直觉，所以我们将它们推迟到第 4 节。

2.2 函子与框

本节将介绍一些更基本的定义和记号，稍后将用有趣的例子加以说明。

除非为了消歧，否则不绘制内部隔间。既是两个范畴的映射又是函子的被称为双函子。在下文中，除了简要引入幺半范畴的定义外，我们将不使用双函子框，之后就不再需要它们了。

对框的内部和外部使用不同的颜色，以指示两个不同的范畴，也可以增加一个额外的视觉指示器，有助于错误检查，正如我们在下一节中将看到的。

2.2.1 自然变换

沿着抽象阶梯继续向上攀登，自然变换可以被视为函子之间的映射。它们是由源范畴中的对象索引的态射集合，这些态射在目标范畴上是“均匀”的。均匀性性质定义如下。

从弦图的角度来看，自然变换仅仅是态射的集合，因此不需要引入新的图形记号。但是分量的交换图可以图形化地表示为：

在上文中，为了减少杂乱，我们省略了所有可以从图语境中推断出的信息。为了进一步减少杂乱，我们可以使用颜色编码或通过装饰框的边框来指示函子，例如

并移除更多可以从图语境中推断出的信息（XX 和 YY 可以从 f:X→Y 等恢复出来）。

注记 2.12 我们可以认为，图形记号法此时已经开始显现成效了。弦图更直接地表明，自然性是交换性的推广，它利用函子性和索引作为一种巧妙的方式，使得映射 ff的源和目标与自然变换中精心选择的分量的源和目标相匹配。此外，正如我们稍后将看到的，在使用弦图进行计算时，将更容易识别公式的“可约式”（redexes），即公式中可以应用方程的位置。

2.2.2 伴随

两个彼此处于某种特定关系中的函子被称为伴随的。伴随函子在数学和计算机科学中很常见。我们此刻暂不举例，仅介绍定义和性质，例子将在稍后给出。

伴随可以用几种方式来刻画，但我们将强调最适合在弦图图形语言中进行优美呈现的定义，即所谓的单位-余单位伴随（unit-counit adjunction）。

如果两个函子如上定义是伴随的，我们称 FF 为左伴随，GG 为右伴随，记作 F⊣G。 使用弦图，这两个图方程在图形化呈现中变得极具启发性：

为了使图形更具启发性，我们可以将单位和余单位表示为方向相反的半圆。为避免歧义，如有必要，可以用索引对象对它们进行标注。我们使用不同的颜色来指示两个范畴中的态射，并将函子框涂成与其陪域相同的颜色。有了这些进一步的约定，两个弦图方程就简化为：

颜色（紫色和橙色）用于标识恒等所属的范畴，同时也通过用其陪域范畴的颜色标记这两个函子来标识它们。所有被省略的信息（对象标签等）都可以被无歧义地推断出来。

Hom 集伴随 伴随的单位/余单位表示在使用弦图时可以说是最好的。基于这个定义，我们还可以展示伴随的另一种 Hom 集表述的等价性。

2.3 幺半范畴

一个在数学、物理和计算机科学许多领域特别重要的双函子是幺半张量，⊗ : C × C → C，因为它可以用来建模从更简单的数据类型构建聚合数据类型。幺半张量在同构意义上是结合的，表明数据可以用不同但可以通过规范方式彼此恢复的方式进行聚合。这一性质对积类型和和类型都成立，它们都是幺半张量的实例。如果张量是严格结合的，即同构是恒等映射，则称其为严格的。一旦我们在范畴中引入严格幺半张量，弦图的图形语言才真正开始发挥其全部潜力。

移除严格结合的函子框，是项的一维记号中移除结合运算括号的二维版本。在单位约束的情况下会出现类似的情况，其中自然性条件，用图形表示，是：

在上文中，虚线框仅仅是一种试图突出空白空间存在性的尝试；它没有进一步的意义。

我们现在已经定义了严格幺半范畴的核心图形记号。总结如下，它是一种带标签的框和线的语法，其中框代表态射，线代表对象。态射通过串行连接线进行复合，而幺半张量则是图的并行堆叠。张量单位的恒等可以通过将其表示为空白空间来省略。

在严格幺半范畴中，对象本质上是列表，单位 I 是空列表。我们引入记号来定义列表及列表上的基本操作，这对于处理严格幺半范畴中的态射十分方便。

2.4 严格化与弦图

由于我们的总体意图是为编程语言定义弦图，我们通常不能假设张量是严格的。但如果没有严格性，张量的函子框就失去了其简化性质，因此图形记号也失去了其优雅性。这似乎是一个不可逾越的障碍，但使用严格化存在一种原则性的出路。正如我们将看到的，这种构造以一种导致新范畴的方式引入了一个刻意严格的幺半张量版本，该新范畴与原范畴等价。图形化呈现应该能更清晰地说明正在发生的事情。

这种构造既有趣又强大，并且已被以各种方式解释。最广泛但也相当具有误导性的常见解释是“在自由幺半范畴中，所有由单位子和结合子构成的图都是交换的。”

仅显示图中不同的部分，第一个图可以使用图 2 中的第一个、然后第四个、然后再第一个（两次）方程简化为第二个图：

注记 2.27 中关于该性质证明的重要思想在于，非严格范畴中的任何构造都可以用一个具有以下一般形状的图来表示：

2.5 对称幺半范畴

记住，我们赋予张量 (⊗) 比复合 (;) 更高的优先级，因此我们在后文中将继续这样做。

如前一节所讨论，在严格设定下工作更为简单，并且仅当需要非严格张量运算时，才全局地添加严格化子和去严格化子态射。

弦图语言无需扩展，因此上述两个方程以及自然性方程均在图 3 中给出。

这结束了对称幺半范畴的弦图核心语言的介绍，许多更精细的图形语法都依赖于它。我们遵循的路径与读者在大多数文献中找到的截然不同，重点在于函子框和非严格张量积。希望这种视角本身以及作为文献中现有介绍的补充，在理解弦图核心图形语言方面具有一定的教学价值。我们对函子框和非严格张量积的不寻常强调是出于教学动机，但这些构造本身也将证明是重要的。

2.6 叶状化

与项记号法相比，图形记号法被认为具有几个优势。它更抽象，因为多个项对应同一个图；它自动按变量的系统重命名（α-等价）进行商化；它可以更容易地识别可约式，这使得通过对复制和共享的细粒度控制来推导更高效的抽象机成为可能。

在本节中，我们将看到图形化呈现如何帮助推导项的准范式，从而导致更简单的归纳算法以及对图状数据结构上某些类算法的正确性证明。为了给出具体的例子，我们将使用一种类似 OCaml 的函数式语言的通用语法（传值调用，代数数据类型，模式匹配）。我们在此阐述的技术是弦图研究领域常识的一部分，但一种刻意的且聚焦的，而非附带的，表述可以被认为是新的。

让我们从一个常见的情况开始，即非树状数据结构在算法上是合理的，并审视相关的问题和提出的方法。在函数式语言中，树状数据结构无处不在，因为它们可以表示为代数数据类型。例如，考虑节点中存储（整数）数据的二叉树类型：

请注意，这棵特定的树包含一定程度的重复。在这种情况下，一种常见的节省空间的算法手段是使用有向无环图（DAG）来表示公共子结构的共享。上面的树可以有几种优化的 DAG 表示，其中最小的一种如下所示：

请注意，DAG 拥有与它高效表示的树完全相同的路径。

我们现在面临的问题是，DAG 不是一种归纳数据结构。在 DAG 上的高效算法可以用函数式编写，但它们相当复杂（属性文法和高阶抽象语法是两种实现方式）。

这种表示法的优势在于，现在我们可以为以叶状化形式呈现的有向无环图（DAG）编写一个通用的归纳 map 函数，需记住的是，自由生成的 PROP 的语言还包含恒等（id）和对称（sym）。然而，由于 map 函数保持了 DAG 的形状，它只需保留这些结构态射即可。

其中 List.reverse 是通常的列表反转函数。同样，局部修改 DAG（通过用另一个 DAG 替换一个节点）的函数也很容易实现；它们被留作练习。忽略 DAG 形状的函数也是微不足道的，因为 DAG 可以被展平为一个列表。如果需要，结构元素（恒等和对称）可以被过滤掉。在 DAG 中查找元素 n只需在展平的列表列表中搜索它即可完成：

然而，当有向无环图（DAG）以叶状化形式呈现时，并非所有算法都天然适用。以下是困难的，但并非不可能。

练习 2.42（困难） 将表达式的数据类型（整数、加法、乘法）定义为树，并编写一个简单的求值器。考虑将带有共享子表达式的表达式类型视为有向无环图，并在叶状化上编写求值器。

许多在图表示上是标准的算法似乎在叶状化上更难高效或自然地编写，例如按预定顺序（例如前缀、中缀、后缀）的遍历、搜索子图或计算同构。应用操作语义是一个明显不适合叶状化的算法的完美示例，而这将从图表示的更大灵活性中受益。请注意，这里的不适合性不在于表达能力方面，而在于效率方面：标记（token）可以表示为图中的一个节点，重写规则可以以合适的方式表示。然而，恒等态射的遍历在类列表记号中可能需要多个步骤，而不是常规图记号中的单个步骤。一般来说，任何边在类列表记号中都可能由多个恒等态射和对称态射表示，这在时间和空间上很可能效率低下。

注记 2.43 从计算的角度来看，不应将叶状化上的简单归纳算法视为实用的。思考它们的最佳方式是将其视为有向无环图上的简单归纳（且可执行的）规范，与将有向无环图作为原生数据结构进行工作相比，它们更容易形式化并用于证明。这一特性在定义和证明复杂的程序变换（例如（反向）自动微分或闭包转换）时特别有用。然而，关于在叶状化上进行计算而不是使用指针直接实现图所带来的计算开销尚未得到研究。

2.7 叶状化的性质

以下定理是范畴论界的常识：

注意，由于拓扑排序不是唯一的，叶状化也不是唯一的。

2.8 进一步阅读与相关工作

在关于弦图推理的综述中，我们提到三个：(Piedeleu & Zanasi, 2023) 面向计算机科学家，并展示了弦图在几个邻近领域的当代应用；(Selinger, 2011) 提供了许多不同范畴结构的弦图的综合目录，重点关注支配其等价的几何原理；最后，(Baez & Stay, 2010) 在物理、逻辑、拓扑和计算机科学的背景下提出了对弦图的概念性和高层面的理解。我们依赖的特定表述风格，即“函子框”，归功于 (Melliès, 2006)——尽管我们必须指出，有点奇怪的是，这篇文章止步于将该技术应用于伴随，而这正是我们发现它最有用的地方。这些论文共同为理解本节的哲学、动机和一些技术细节提供了最好的基础。它们也是第一作者获得对弦图之美和力量的个人鉴赏的重要灵感来源。同样具有启发性的是 (Coecke & Kissinger, 2017)，它是以 (Abramsky & Coecke, 2004) 开始的一系列论文的高潮，这些论文已牢固确立了图形方法作为幺半范畴及其应用的严肃且有用的语法。

此处展示的图形记号并非唯一存在的弦图种类。无关的，除了精神上，是使用两个 (Marsden, 2014) 和高维结构 (Bar & Vicary, 2017) 的弦图演算。这应该提醒读者，“弦图”一词相当宽泛，可能会引起一些混淆。

一个重要的可能混淆值得阐明，即术语“弦图”作为二维语法与其图表示（作为组合数学对象或具体数据结构）的混淆。这两者之间的区分值得做出，正如本教程的其余部分希望展示的那样。第二位作者关于用于形式化表示为图的弦图等式理论的重写技术的研究工作坚持这种区分，例如见 (Bonchi, Gadducci, Kissinger, Sobocinski, & Zanasi, 2016)。

对于幺半范畴，我们需要提及引入弦图风格图形记号的原始论文 (Joyal & Street, 1991, 1995)。由于这些一般幺半范畴不被假定为对称的，等价的概念不是同构而是“同伦”（homotopy），即嵌入图的基底的平滑形变。在原始论文中也考虑了对称性，并有一个有趣的观察，即同构可以通过增加基底的维度数简化为同痕（isotopy），即 2 维结构的同构可以被视为 3 维空间中的同痕。

原始论文，以及实际上随后的几乎所有文献，都在严格幺半范畴的背景下运作。非严格范畴的问题被相当简略地驳回了：“原则上，大多数在假设张量范畴是严格的情况下获得的结果可以被重新表述并在没有这个条件的情况下被证明。”（第 59 页，出处同上）。在数学上这也许是真的，但如果我们要认真考虑将弦图作为形式语法，细节显然值得详细说明。弦图的严格化的这种仔细说明是在 (Wilson, Ghica, & Zanasi, 2022) 中完成的。

3 Hierarchical String Diagrams and the 𝜆 Calculus