💻 computer science

Well-Scoped Locally Nameless Representation of Syntax

本文提出了一种由 Plotkin 风格绑定签名参数化的、通用的、范围明确的局部命名语法表示法，证明了其相对于模 alpha 转换的朴素命名语法的充分性，并通过示例展示了其效用。

原作者： Andrew M. Pitts

发布于 2026-05-12

📖 1 分钟阅读☕ 轻松阅读

原作者： Andrew M. Pitts

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

想象你是一位图书管理员，试图整理一座庞大而混乱的图书馆，其中的书籍可以在内部引用其他书籍。有些书的封面上写有标题（如《了不起的盖茨比》），而另一些则只是特定区域内的编号书架（如"3 号架，第 2 排”）。

本文由 Andrew Pitts 撰写，介绍了一种更智能的图书馆整理新方法，使计算机（特别是像 Agda 这样的“交互式定理证明器”）能够在不混淆或出错的情况下检查图书馆的规则。

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

1. 问题：“无名”与“有名”的两难困境

当计算机科学家试图教计算机理解语言（如编程语言或逻辑）时，他们必须处理变量。

“有名”方式：你给每个变量起一个名字，如 x、y 或 z。这对人类阅读很友好，但计算机在交换名称时会感到困惑（这被称为"α-转换”问题）。如果你重命名它们，x 和 y 是相同的吗？
“无名”方式（De Bruijn 索引）：你完全停止使用名称。相反，你只说“第 1 个变量”、“第 2 个变量”等，从内向外计数。这对计算机很好，但对人类来说很糟糕，因为它看起来像是一团混乱的数字。

2. 旧方案：“局部有名”

几年前，研究人员提出了一种混合想法，称为局部有名（Locally Nameless）。

自由变量（未在循环或函数内部绑定的内容）保留其名称（如 x）。
绑定变量（循环内部的内容）使用数字（如 0、1）。

陷阱：该系统有一个“陷阱”。它允许你创建“损坏”的项，其中的数字与范围不匹配。想象一本书写着“去第 5 号架”，但你当前所在的房间只有 3 个书架。计算机必须不断检查：“这个项是‘局部封闭’（有效）的吗？”这需要大量的额外证明工作，就像图书管理员在允许任何人借阅之前，必须不断检查书籍是否在正确的过道中。

3. 新方案：“作用域良好的局部有名”

本文提出了一种更好的方法：作用域良好的局部有名（Well-Scoped Locally Nameless）。

计算机不再仅仅使用数字，而是使用类型来强制执行规则。

将图书馆想象成拥有不同的“房间”。
如果你在0 号房间，你只能看到编号为 0 到 0 的书架（这意味着没有书架，只有自由名称）。
如果你在1 号房间，你可以看到 0 和 1 号书架。
如果你在5 号房间，你可以看到从 0 到 5 的书架。

魔法：在这个系统中，你根本无法构建一本“损坏”的书。如果你试图在2 号房间写下“去第 10 号架”，计算机的类型系统会说：“不，那是不可能的。你甚至无法写出那个句子。”

论文认为，这种方法：

消除了“陷阱”：你不需要编写额外的证明来检查项是否有效。项的存在本身就证明了它是有效的。
具有透明性：它看起来仍然主要像人类习惯的“有名”方式，因此不像纯粹的“无名”方式那样令人困惑。
具有通用性：作者构建了一个“库”（一套工具），适用于你想要定义的任何语言，只要使用标准模板描述绑定规则（如 if 语句或 lambda 函数如何工作）。

4. 工作原理（“打开”与“关闭”）

论文描述了两个主要操作，就像在房间之间移动书籍：

抽象（关闭）：将一个自由名称（如 x）转换为一个绑定索引（如 0）。这就像把一本书从书架上取下，放入新房间中特定的编号插槽。
具体化（打开）：将一个绑定索引替换为特定的书（项）。这就像把一本书从插槽中取出，并在其位置放上一本真实的书。

作者证明了他们的“作用域良好”数学完美运作。他们表明，他们的新系统在数学上等同于旧的“有名”系统，意味着它们代表完全相同的概念，只是组织得更加安全。

5. 现实世界的例子

这篇论文不仅仅谈论理论；他们在三种不同类型的语言上测试了他们的“库”：

π-演算（The Pi-Calculus）：一种用于描述计算机程序如何相互通信（如电话通话）的语言。在这里，名称是通信的“通道”。
Martin-Löf 类型理论：一种用于数学证明的复杂系统。他们展示了如何编写自然数和类型的规则，而不会在名称的“新鲜性”中迷失方向。
哥德尔系统 T（Gödel's System T）：一种用于证明计算最终会结束（可判定性）的系统。他们使用他们的方法证明特定算法的正确性。

核心结论

论文指出：“停止手动检查你的变量是否在正确的位置。让计算机的类型系统为你承担繁重的工作。”

通过使用依赖类型（Agda 编程语言的一个特性），他们创建了一个无法写出无效语法的系统。这使研究人员免于编写数千行枯燥的证明代码，仅仅为了说明“是的，这个变量在作用域内”。它使形式化验证（证明软件无漏洞）变得更简单、更安全，也更接近人类对语言的自然思考方式。

技术摘要：作用域良好的局部命名语法表示

问题陈述
在基于依赖类型理论的交互式定理证明器（如 Agda、Lean 或 Rocq）中形式化带有绑定构造的语言（例如 $\lambda$ -演算、类型系统）时，一个核心挑战是管理变量绑定和 $\alpha$ -等价性。“局部命名”方法将自由变量表示为显式名称，将绑定变量表示为 de Bruijn 索引，已被证明能够满足 PoplMark 标准，具有低基础设施开销、透明性和易于入门的特点。然而，标准的局部命名表示存在一个致命缺陷：项的归纳定义允许“悬空”索引（超出当前作用域的索引）。为了确保正确性，必须将定义域限制为“局部封闭”项的子集。这需要重复、手动地证明操作（如替换）保持局部封闭性，从而在形式化开发中造成了显著的负担，并成为潜在错误的来源。

方法论
本文提出了一种“作用域良好”的局部命名表示变体，利用 Agda 的依赖类型系统内在强制局部封闭性，而非将其作为单独的谓词。

索引归纳类型：库不再定义单一的项类型，而是定义了一族由自然数 $n$ 索引的类型 Trm[n]。一个 n-项 是指所有 de Bruijn 索引均取自有限类型 Fin n（小于 $n$ 的自然数）的项。
局部封闭项作为 0-项：在此框架下，“局部封闭”项（即没有悬空索引的项）精确对应于 Trm[0]。带有自由变量的项表示为 Trm[n]，其中 $n$ 对应当前作用域中自由变量的数量。
绑定签名的参数化：该库是通用的，以 Plotkin 风格的绑定签名作为参数。这允许定义算子、它们的元数以及每个参数位置绑定的名称数量。
通过依赖类型实现的操作：
- 作用域弱化：一个函数 Trm[m] -> Trm[n]（其中 $m \le n$ ），用于注入索引，处理进入更大作用域时所需的移位。
- 具体化（打开）：将 (1+n)-项中的索引 $i$ 替换为一个 0-项，以生成一个 n-项。这涉及将大于 $i$ 的索引向下移位一位。
- 抽象（关闭）：将 n-项中的一个自由名称替换为一个索引，以生成一个 (1+n)-项。这涉及将索引向上移位。
- 替换：结构定义。由于替换函数将名称映射到 0-项（Trm），“局部封闭”条件由类型系统自动强制。对 n-项进行替换会生成另一个 n-项。

主要贡献

WSLN 库：一个通用的 Agda 库，实现了作用域良好的局部命名项。它为定义任何由 Plotkin 绑定签名指定的语言的语法、操作（弱化、替换、抽象、具体化）和推理原则提供了基础设施。
形式化充分性证明：本文提供了严格的证明，建立了以下两者之间的双射：
1. 作用域良好的局部命名 0-项类型（Trm[0]）。
2. “有名称”项（即自由变量和绑定变量均具有显式名称的项）的 $\alpha$ -等价类。
  该双射证明了作用域良好的表示正确捕捉了避免捕获的替换和 $\alpha$ -等价的语义。
消除局部封闭证明：通过将作用域约束编码在类型索引中，消除了对显式“局部封闭”谓词及相关证明义务（例如证明替换保持局部封闭性）的需求。这些性质成为类型规则的推论。
新鲜性处理：该库与名义技术集成，使用“有限不可耗尽”的原子集（自然数）通过余有限量化生成新鲜名称，确保新鲜性条件得到系统处理。

结果
本文通过三个在 Agda 中实现的独立示例验证了该方法：

$\pi$ -演算：展示了该库在 $\lambda$ -演算之外的适用性，能够处理进程表达式和通道名称。它强调，虽然该库处理绑定结构，但针对良构性的类型检查（例如确保通道在预期位置使用）仍然是一个独立的、由用户定义的判断。
Martin-Löf 类型理论 (MLTT)：展示了该库如何促进类型规则的定义。它对比了“存在新鲜”规则（需要显式的新鲜性假设）与“余有限量化”规则（其中新鲜性是隐式的），证明了作用域良好的表示支持后者，从而带来更清晰、更透明的形式化。
Gödel 的 System T（通过求值进行归一化）：一项实质性的开发，证明了 $\beta\eta$ -转换的可判定性。该示例说明了作用域良好的表示如何简化抽象的语义以及复杂语义构造（集值预层）中新鲜性的处理，从而避免了对有限支持语义对象的需求。

意义与主张
本文主张，作用域良好的局部命名表示为解决传统局部命名方法中悬空索引的“陷阱”提供了一个“直接”而强大的方案。其主要意义在于将确保作用域正确性的负担从用户（通过手动证明）转移到了定理证明器的类型检查器（通过依赖类型）。

作者强调，这种方法保持了 PoplMark 标准所要求的透明度：形式化定义紧密反映非正式惯例，而“索引瑜伽”（de Bruijn 索引的操纵）被封装在库的操作中。虽然实现需要仔细处理有限序数（Fin n）和索引移位，但该库将这种复杂性参数化，允许用户定义语言并证明性质，而无需管理底层的机制。本文谦逊地指出，尽管当前的绑定签名是无序的且模拟简单的绑定作用域，但该方法足够稳健，能够处理复杂的类型系统和语义证明，System T 的开发即证明了这一点。