💻 computer science

Constructing (Co)inductive Types via Large Sizes

本文提出了一种将大小的大类型与参数化量词一致地扩展至内涵类型论的方法，以构建归纳类型和共归纳类型，从而克服先前方法的局限性以及 Agda 当前大小类型实现的不一致性。

原作者： Bastiaan Laarakker, Daniël Otten, Benno van den Berg

发布于 2026-05-01

📖 1 分钟阅读☕ 轻松阅读

原作者： Bastiaan Laarakker, Daniël Otten, Benno van den Berg

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

想象你正在构建一座庞大且自指的知识图书馆。在这座图书馆中，每一本书（即一个“类型”）都可以包含对其他书的引用，而有时一本书甚至会引用它自己。为了防止这座图书馆陷入混乱或无限循环，你需要制定严格的规则，规定这些书该如何编写和阅读。

本文旨在为一种名为“证明助手”（如 Agda 或 Lean）的特定图书馆设计一套更优的规则。这些工具帮助数学家和程序员编写保证能运行的代码，以及保证为真的证明。

以下是用简单类比对该论文思想的拆解：

1. 问题所在：“停止标志”与“速度表”

目前，证明助手采用一种“停止标志”方法（称为语法检查）来确保程序不会无限运行。它们检查代码的形态。如果一个函数调用自身，计算机会检查：“你是否将更小的数据片段传递给了下一次调用？”如果是，则是安全的。如果代码过于复杂，计算机可能会感到困惑并回答：“不行，我无法证明这会停止”，即使它实际上确实会停止。

本文的解决方案：作者提出不再查看代码的形态，而是给每一块数据赋予一个大小标签（就像速度表或高度标记）。

归纳类型（如数字列表）被标记为“高度”。递归函数必须始终在高度上向下移动。
共归纳类型（如无限数据流）被标记为“深度”。递归函数必须始终更深地移动，以体现其生产性。

2. 当前系统的缺陷：“魔法无穷大”

在现有系统（Agda）中，有一个特殊的标签称为无穷大（ $\infty$ ）。它本应是涵盖一切的“最大可能大小”。

类比：想象一把尺子，其最末端有一个“无穷大”的标记。问题在于，本文作者发现，如果你试图用这把尺子去测量事物，你可能会意外地证明“无穷大比无穷大更小”。这会破坏数学逻辑，使整个系统变得不一致（就像一把尺子声称一米比一米短）。

3. 新方法：“参数化群体”

作者提出了一种处理这些大小的新方式，不再使用单一的“无穷大”标签。他们引入了两个特殊工具：参数化存在量词（ $\exists$ ）和参数化全称量词（ $\forall$ ）。

可以将它们视为观察人群（即各种大小）的两种不同方式：

归纳类型（“存在性”群体）：
- 理念：一棵有限树（如家谱）具有特定高度，但在使用它时，我们无需确切知道它有多高。我们只需要知道，在某处存在一个高度限制。
- 隐喻：想象你在人群中寻找特定的人。你不需要看到所有人；你只需要知道人群中存在一个符合描述的人。“大小”被保持为抽象且隐藏的状态。你无法窥探具体的数字；你只知道存在一个限制。这防止了“无穷大比无穷大更小”的悖论。
共归纳类型（“全称性”群体）：
- 理念：无限流（如直播视频）可以在任意时长内被观察。
- 隐喻：想象你在观看一场戏剧。要断言这场戏剧是“无限”的，你必须能够按照你选择的任意时长观看它。这里的“大小”是一个承诺：无论你看多深，数据都能成立。

4. 魔法技巧：构建图书馆

作者展示了如何利用这些“群体”工具来构建这些复杂类型（即图书馆的书籍）：

第一步：他们在每一个可能的大小上构建类型的“近似值”（就像在 1 英尺高、2 英尺高等不同高度上构建房屋模型）。
第二步：他们使用存在性工具，将所有“有限高度”的近似值打包成一个真实的归纳类型。
第三步：他们使用全称性工具，将所有“无限深度”的近似值打包成一个真实的共归纳类型。

为什么这更好？
先前的尝试只能构建“有限分支”的树（如每个人只有有限数量子女的家谱）。而这种方法可以构建无限分支的树（即一个节点可以拥有无限数量的子节点），这要强大和灵活得多。

5. 证明：“实在性”模型

为了证明新系统不会破坏数学，他们构建了一个“实在性模型”（Realisability Model）。

类比：想象法庭上的一位法官。法官不会仅凭律师的口头陈述就采信，而是会将证据与一本特定、极大且极其严格的规则书进行核对。
规则书：他们将“大小”解释为简单的数字，而是解释为不可数序数（这是高等数学中的一个概念，比所有自然数的集合还要“大”）。
结果：通过将大小视为这些巨大的不可数数字，他们证明了其“参数化”规则（隐藏具体大小）完美运作。系统是一致的，这意味着它不会意外地证明“无穷大比无穷大更小”。

总结

本文解决了当前证明助手中的一个漏洞，即“魔法无穷大”标签会导致逻辑矛盾。他们将其替换为一个将大小视为隐藏、抽象限制的系统。

对于有限事物：他们说：“存在某个限制，但我们不会去查看它。”
对于无限事物：他们说：“它适用于你选择的任何限制。”

这使得他们能够安全地构建复杂的无限数据结构，确保证明助手依然是数学和编程中可靠的工具。

以下是 Bastiaan Laarakker、Daniël Otten 和 Benno van den Berg 的论文《通过大尺寸构造（共）归纳类型》的详细技术总结。

1. 问题陈述

证明助手（如 Agda、Lean、Rocq）依赖依赖类型理论来确保一致性和可判定性。一个关键要求是，所有递归函数必须是全的（终止的），且所有共递归函数必须是有产出的。

当前局限性：大多数系统通过语法检查（如结构递归或大小变化终止）来强制全性。这些检查往往具有限制性、非模块化，且对代码重构敏感。
带尺寸的类型（Sized Types）：一种基于类型的替代方案使用“尺寸”（序数）来注解类型，允许通过基于尺寸的良基归纳来证明终止性。
Agda 的不一致性：Agda 实现了带尺寸的类型，但引入了一个最大尺寸（ $\infty$ ）来将完整的归纳/共归纳类型定义为其在 $\infty$ 处的近似。这导致了一个逻辑不一致：系统证明了 $\infty < \infty$ ，违反了严格良序的无自反性。
先前的理论工作：先前尝试使用参数化量词（归纳类型使用存在量词 $\exists$ ，共归纳类型使用全称量词 $\forall$ ）来修复此问题的努力是有限的。具体而言，它们只能构造有限分支的归纳类型，因为尺寸类型被解释为自然数集（ $\mathbb{N}$ ），而自然数集缺乏无穷分支结构所需的极限序数。

目标：构造一个一致的类型理论，利用带尺寸的类型和参数化量词支持所有（共）归纳类型（包括无穷分支类型），而不依赖不一致的最大尺寸。

2. 方法论

作者扩展了 Martin-Löf 类型理论（MLTT），加入了特定功能以实现这一构造，并通过实现模型证明了一致性。

A. 扩展的类型理论

该理论包含标准的 MLTT 功能（宇宙、 $\Sigma$ 、 $\Pi$ 、恒等类型），外加：

尺寸类型（Size）：
- 配备零元（$0 $）和后继（$ \uparrow i$）。
- 由一个预序（ $\leq$ ）排序，该预序被编码为纯命题。
- 关键：Size 是一个大类型（不在宇宙 $U$ 中），但对其进行的量化可以产生小类型。
参数化量词：
- $\exists i. A(i)$ （存在量词）：表示近似值的并集。项是配对 $\langle s, a \rangle$ ，但尺寸 $s$ 被抽象化（无法进行模式匹配）。消去规则被限制在小类型上。
- $\forall i. A(i)$ （全称量词）：表示近似值的交集。函数对任何尺寸都一致地作用。
- 参数化公理：该理论包含公理，声明这些量词与类型构造子交换（例如， $\Pi x:A. \exists i. B(x,i) \simeq \exists i. \Pi x:A. \exists j < i. B(x,j)$ ）。这将尺寸被一致处理的观念内化。
良基归纳（fix）：
- 一个不动点算子，允许基于尺寸进行归纳定义：给定 $f : \forall i. ((\forall j < i. A(j)) \to A(i))$ ，定义 $fix\ f : \forall i. A(i)$ 。
- $\beta$ -规则是命题性的（而非定义性的），以保持类型检查的可判定性。

B. （共）归纳类型的构造

作者将（共）归纳类型编码为多项式自函子（ $F$ ）的初始代数和最终余代数。

序数近似：他们定义了尺寸索引函子 $F[\exists -]$ 和 $F[\forall -]$ 。利用 fix 算子，他们为这些尺寸索引函子构造了初始代数（ $\mu_3 F$ ）和最终余代数（ $\nu_2 F$ ）。这些表示在特定尺寸处截断的类型。
通过量化构造完整类型：
- 归纳类型：定义为 $\mu F := \exists i. (\mu_3 F) i$ 。存在量词收集所有被某个尺寸界限的项。
- 共归纳类型：定义为 $\nu F := \forall i. (\nu_2 F) i$ 。全称量词确保项在任何深度都是可观察的。
处理无穷分支类型：关键创新在于证明多项式函子与存在量词弱交换。这需要极限序数（尺寸序列的上确界）的存在，如果尺寸仅仅是 $\mathbb{N}$ ，则这是不可能的。

C. 一致性证明：实现模型

为了证明该理论是一致的，作者基于 Hyland 的有效拓扑斯（Effective Topos）构造了一个实现模型。

类型的解释：
- 小类型：被解释为自然数（可计算数据）上的部分等价关系（PERs）。
- 大类型：被解释为组装（Assemblies，带有可计算性关系的集合）。
Size 的解释：
- 类型 Size 被解释为 $\nabla \omega_1$ ，其中 $\omega_1$ 是第一个不可数序数（所有可数序数的集合）。
- 它被赋予“完整”的实现关系，意味着态射必须一致地处理所有尺寸（参数化）。
验证：
- 由于 $\omega_1$ 包含极限序数，该模型验证了无穷分支归纳类型所需的参数化公理。
- 该模型验证了非直谓性（对大类型的量化产生小类型）和身份证明的唯一性（UIP），尽管语法并未假设这些性质。这表明语法与更强的理论（如同伦类型理论）兼容，而不受其限制。

3. 主要贡献

（共）归纳类型的一般构造：与先前局限于有限分支类型的参数化方法不同，这项工作构造了所有（共）归纳类型，包括无穷分支类型（例如，Brouwer 序数、构造性集合论模型）。
解决 Agda 的不一致性：通过将不一致的“最大尺寸”（ $\infty$ ）替换为对大尺寸类型的参数化量化，作者为 Agda 当前的实现提供了一种一致的替代方案。
作为机制的参数化量词：他们证明了通过在尺寸上内化 $\exists$ 和 $\forall$ 的参数化，有效地强制了必要的抽象，以防止非终止行为和逻辑不一致。
稳健的实现模型：构造了一个将 Size 解释为 $\omega_1$ 的模型，为该理论提供了严格的语义理由，证明了参数化公理是一致的。

4. 结果

理论健全性：论文证明了对于任何多项式自函子，其初始代数和最终余代数都在扩展理论中存在。
一致性：实现模型确认了该理论是一致的。它表明，当尺寸被解释为不可数序数时，参数化量词的公理成立。
兼容性：这些构造在语法上不依赖 UIP 或非直谓性，使得结果与同伦类型理论（HoTT）兼容，尽管模型满足这些性质。

5. 意义与未来工作

对证明助手的影响：这项工作提供了一条路径，可在证明助手（如 Agda）中实现带尺寸的类型，而无需当前由 $\infty$ 尺寸引起的一致性错误。它允许更模块化和组合式的终止检查。
计算行为：作者承认，尽管理论是一致的，但当前的语法缺乏参数化公理的计算行为（它们是公理，而非归约规则）。未来的工作需要将其与内部参数化（例如，通过桥接类型或立方类型理论）联系起来，以确保实际中的可判定性和典范性。
不等式的可判定性：该模型暗示尺寸上的不等式通常不可判定（由于上确界）。作者建议采用混合方法（定义性不等式与命题性不等式）以进行实际实现。
推广：该模型有可能推广到其他部分组合代数，或与效应及同伦性（univalence）集成。

总之，该论文成功弥合了参数化带尺寸类型的理论需求与一致性实际要求之间的差距，使得在健全的类型理论框架内构造复杂的（共）归纳类型成为可能。