💻 computer science

Rzk: a Proof Assistant for Synthetic $\infty$ -Categories

本文介绍了 Rzk，这是一个实现了 Riehl 和 Shulman 的单纯型理论（simplicial type theory）的精化计算变体的实用证明助手，旨在实现对 $\infty$ -范畴的合成推理，同时确立了其相对于原理论的忠实性与保守性，并提供了关于其用法与实现的教程。

原作者： Nikolai Kudasov, Violetta Sim, Benedikt Ahrens

发布于 2026-07-15

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Nikolai Kudasov, Violetta Sim, Benedikt Ahrens

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

想象一下，数学的宇宙是一个巨大的、无限的游乐场。很长一段时间以来，这里最受欢迎的游戏是同伦类型论 (Homotopy Type Theory, HoTT)。在这个游戏中，一切都是由“形状”构成的，而且这些形状是完美可变的。如果你有一条从点 A 到点 B 的路径，你总是可以原路返回。这就像一个由橡皮筋组成的世界，每一次拉伸都可以缩回到原始状态。这对于研究“空间”（即那些一切都是可逆的数学对象）非常棒，但对于某些路径是单行道的、更为复杂的范畴（categories）的现实世界来说，它显得过于完美了。

于是，Rzk 登场了——这是一个由 Nikolai Kudasson、Violetta Sim 和 Benedikt Ahrens 构建的新型证明助手。你可以将 Rzk 想象成一个专门设计的构建套件，用于建造有向形状 (directed shapes)。在这个新的游乐场里，你可以拥有一条从 A 到 B 的路径，但这条路径无法被倒着走回去。这就像是用乐高积木进行搭建，其中一些连接是永久性的：你可以把一个零件卡上去，但如果不破坏模型，你就无法将其拆下来。这使得数学家能够对 $\infty$ -范畴 ( $\infty$ -categories) 进行推理，这些复杂的结构中，箭头（态射）具有方向性，且并不总是可逆的。

核心理念：一种全新的构建方式

这篇论文介绍了 Rzk，它是一个实现了由 Emily Riehl 和 Michael Shulman 最初提出的特定理论——单纯类型论 (Simplicial Type Theory, RSTT) ——的工具。

这里是 Rzk 使用的一个巧妙技巧：
在原始理论 (RSTT) 中，有一个特殊的“魔法盒”，叫做扩展类型 (extension type)。这个盒子允许你定义一个函数，该函数在形状（如三角形）的“边缘”上表现出特定的行为，而在“中间”部分则可以随心所欲。它虽然强大，但有点像一个黑盒；关于它如何运作的规则有时隐藏在细则之中。

Rzk 将这个魔法盒拆解开来。

形状 (The Shape)： 它将“形状”部分（三角形或区间）与“边界”部分（边缘的规则）分离开来。
规则 (The Rules)： 它引入了一种新的、显式的规则，称为无强制转换子类型 (coercion-free subtyping)。想象你有一个能放入小盒子的玩具车。在旧系统中，系统会直接假设这辆车能放入更大的盒子，而不会进行检查。在 Rzk 中，系统会显式地检查这辆车是否合适，但它不会强迫你为车穿上额外的包装（即“强制转换”）来使其适配。它只是说：“是的，这辆车也是一个玩具，所以它属于玩具盒。”这使得逻辑更加清晰，也更容易由计算机进行检查。

Rzk 能做什么（以及不能做什么）

作者为这个新系统构建了一个名为 sHoTT 的“标准库”。这个库已经非常庞大，包含超过 25,000 行代码和近 1,500 个顶层声明。该库已成功形式化了复杂的概念，例如 $\infty$ -范畴的 Yoneda 引理（范畴论中的一个基本定理）以及各种类型的“纤维化 (fibrations)”（即如何将范畴堆叠在一起的方法）。

然而，论文对自己的证明结论是非常谨慎的：

它是忠实的 (Faithful)： 作者证明了你在原始理论 (RSTT) 中能证明的一切，在 Rzk 中也同样可以证明。这是一个完美的翻译。
它是保守的 (Conservative)，但有一个前提： 他们证明了 Rzk 不会创造出关于旧理论的任何“新真理”。如果 Rzk 证明了关于旧形状的某件事，那么旧理论也能证明它。但是，这个证明仅适用于特定的“自然推导片段”。作者承认，他们尚未证明这适用于所有可能的奇特情况；他们怀疑这在整个系统中普遍成立，但这目前仍是一个猜想。
它是实用的 (Practical)： 这个工具现在就可以使用。它可以在浏览器中运行，拥有 VS Code 扩展，并已被用于暑期学校和硕士论文的研究中。

“形状求解器 (The Shape Solver)”

这项数学中最难的部分之一是检查一个形状是否包含在另一个形状之内（例如，这个三角形是否在正方形内部？）。Rzk 使用了一个自动化的“拓扑求解器 (tope solver)”来处理这个问题。

它是如何工作的： 这有点像侦探在解谜题。它观察规则（topes）并尝试判断它们是否匹配。
效果如何？ 在对 sHoTT 库的测试中，求解器处理了超过 25,000 个问题。大多数问题都能瞬间解决（仅需一步）。少数问题非常困难，需要数千步，但求解器最终还是处理了它们。
局限性： 该求解器是不完备的 (incomplete)。它是一个原型。它在处理目前看到的这类问题时表现出色，但作者承认，因为它没有尝试每一种可能的路径，所以它可能会错过一些棘手的解法。他们计划在未来构建一个“完美”的求解器，但目前的版本是“在实践中足够好”的。

Rzk 拒绝什么

论文明确表达了反对这种观点的立场，即认为需要手动证明每一个微小的形状包含关系。在旧系统中，你可能需要写出一段冗长的证明，仅仅为了说明“这个三角形在正方形内部”。Rzk 拒绝这种体力劳动；它将其自动化了。

它同时也拒绝了强制转换 (coercions) 的概念（即为了让事物适配而添加额外的包装层）。作者展示了你可以拥有一个理解子类型、却无需强迫计算机插入那些使数学变得复杂的隐形转换步骤的系统。

总结

Rzk 是一个正在运行且可用的工具，它将有向 $\infty$ -范畴的抽象理论带入了计算机检查证明的现实世界。它将复杂的数学“魔法盒”拆分为更简单、透明的部分，并证明了它在增加新能力的同时，并没有破坏旧有的规则。

作者确信 Rzk 忠实地实现了该理论，并且他们的库是有效的。他们确定该工具在当下的教学和研究中非常有用。然而，对于针对所有可能的边缘情况的完整理论保证（即“完全保守性”猜想），他们并不确定；同时他们也承认，其形状求解器是一个原型，仍有改进空间。他们尚未解决让系统对所有可能的输入都实现终止（归一化/normalization）的问题，这仍然是未来的一个开放性挑战。

简而言之，Rzk 是一个运行中、经过验证且不断成长的数学引擎，它通过全新的设计，在不丢失原始理论魔力的前提下，减轻了计算机的工作负担。

问题陈述
本文探讨了开发一种能够对 $\infty$ -范畴（特别是 $(\infty, 1)$ -范畴）进行综合推理（synthetic reasoning）的证明助手的需求。虽然同伦类型论（HoTT）为 $\infty$ -群组（ $\infty$ -groupoids，其中所有态射都是可逆的）提供了一个综合框架，但它缺乏处理定向态射（directed morphisms）的机制，而这对于范畴论至关重要。Riehl 和 Shulman 提出的单纯形类型论（RSTT）被视为一种解决方案，它引入了“形状”（shapes，如定向区间和三角形）和“扩展类型”（extension types），从而通过定义性地定义态射和高阶胞腔（higher cells）。然而，RSTT 在很大程度上仍是一个理论框架；它尚未在实际的证明助手中实现。实现 RSTT 的主要挑战包括：使类型检查在计算上可行、处理扩展类型复杂的边界条件，以及形式化 RSTT 定理通常在图式化（schematically）层面所依赖的元理论假设（如形状包含关系）。

方法论
作者提出了 Rzk，这是一个实现了 RSTT 计算细化的证明助手。其开发方法涉及三个主要层面的开发：

理论细化（声明式 Rzk）： 作者定义了一个声明式变体 RSTT（dRzk），并引入了两个关键的结构性变化，以使该理论更易于实现：
- 分裂扩展类型（Split Extension Types）： dRzk 没有使用单一的扩展类型算子，而是将概念分离为：一个由形状索引的函数类型（在形状上的 $\Pi$ -类型）和一个类型限制（为一个任意类型附加一个定义性边界）。这使得类型检查器能够处理中间类型，即在函数已被应用但其边界条件尚未完全解析时的状态。
- 无强制转换的子类型（Coercion-Free Subtyping）： 为了处理论文证明中常见的“隐式”等同（例如，将受限类型视为其底层类型），dRzk 引入了一种显式的、无强制转换的子类型关系。这确保了项在子类型检查期间保持不变，从而避免了一致性（coherence）问题。
元理论形式化： 作者形式化了“元理论参数层”（MPL）。RSTT 的定理通常是针对抽象立方体（cubes）、拓扑（topes，立方体上的逻辑公式）和类型族进行图式化陈述的。Rzk 将这些内容内化为定义中的一等公民参数，使得系统能够显式地处理形状包含关系和侧边条件，而不是将其作为隐性的元层假设。
算法实现： 作者实现了一个具有以下特征的算法版本 (aRzk)：
- 双向类型检查（Bidirectional Type Checking）： 一种标准的双向算法，经过适配以携带整个拓扑上下文（tope context）。
- 类型驱动计算（Type-Directed Computation）： 归一化是在填充了类型信息的精化项（elaborated terms）上定义的，因为归约取决于类型信息（特别是某个边界拓扑是否成立）。
- 自动拓扑求解器（Automated Tope Solver）： 一个针对形状逻辑（关于定向区间的直觉主义命题逻辑）的原型求解器，它能自动检查形状包含和边界条件所需的蕴含关系。
- 子类型集成： 子类型通过一个方差标志（variance flag）被整合进定义相等性检查中，从而避免了插入显式的强制转换。

核心贡献

Rzk 证明助手： 第一个用于实现针对综合 $\infty$ -范畴论的单纯形类型论的实现。它使用 Haskell 编写，并提供浏览器端游乐场及 VS Code 扩展。
形式化翻译与保守性： 作者定义了一个从 RSTT 到 dRzk 的翻译 $\tau$ ，以及一个反向翻译 $\sigma$ 。他们证明了该翻译是忠实的（每个 RSTT 证明都能转化为 Rzk 证明）且在自然推导片段上是保守的（dRzk 不会证明关于 RSTT 类型的新结论）。该片段要求“自由站立”（free-standing）的限制（即未附着在形状- $\Pi$ 码值上的限制）不能作为假设，只能作为结论。
sHoTT 库： 作者通过 sHoTT 库展示了 Rzk 的实用性。这是一个标准库，包含超过 25,000 行代码和近 1,500 个声明。该库形式化了综合 $(\infty, 1)$ -范畴论的核心概念，包括 Segal 类型、Rezk 类型、协变族、伴随关系，以及首次对 $\infty$ -范畴 Yoneda 引理的形式化。
实现细节： 论文详细介绍了处理拓扑逻辑、带有拓扑上下文的双向类型检查以及将子类型集成到定义相等性中的特定算法。

结果

正确性： 该系统成功通过了 sHoTT 库的类型检查。作者报告称，尽管拓扑求解器是不完备的，但它能高效处理库中的绝大多数查询（59% 在单步内完成，99% 在 35 步内完成）。
错误修复： 通过对声明式理论与实现之间的严格比较，研究人员发现了先前版本（v0.7.7）中与恒等类型比较和非对称子类型检查相关的两个健全性漏洞，并在 v0.7.8 中进行了修复。
性能： 求解器约占总类型检查时间的 10%。该系统能够处理复杂的证明（如 Yoneda 引理），且无需人工干预形状包含关系。

意义与主张
论文声称 Rzk 是第一个也是唯一的 RSTT 证明助手，填补了 Riehl 和 Shulman 的理论提议与实际形式化之间的空白。其意义在于：

赋能综合 $\infty$ -范畴论： 它允许数学家直接在类型论中对 $(\infty, 1)$ -范畴进行推理，利用扩展类型来定义同伦型（hom-types）和组合，而无需进行命题层面的簿记工作。
实际可用性： sHoTT 的存在证明了该理论不仅在理论上是健全的，而且在处理非平凡数学问题时是具有实际可用性的。
理论严谨性： 通过证明忠实性和保守性，作者确保了 Rzk 是对原始 RSTT 提议的忠实实现，而非一个偏离的分支。

作者对开放问题保持谦逊。他们承认，对于所有 dRzk 推导（包括那些在假设中带有自由站立限制的情况）的完全保守性目前仍是一个猜想。他们还指出，RSTT 的归一化终止性在一般情况下尚不明确，且拓扑求解器是一个虽具备健全性但不完备的原型。未来的工作包括实现元理论的机械化、实现基于评估的归一化（normalization-by-evaluation）后端，以及增加对隐式参数和高阶归纳类型（higher inductive types）的支持。

核心理念：一种全新的构建方式

Rzk 能做什么（以及不能做什么）

“形状求解器 (The Shape Solver)”

Rzk 拒绝什么

总结

类似论文