💻 computer science

Work-in-Progress: A Tactic for Pattern Matching in Autosubst

这篇在研论文介绍了一种用于 Autosubst 的自动模式匹配策略，该策略解决了其在处理类型规则、归约关系和非唯一解方面的现有局限性，并通过在 POPLMark 和 POPLMark Reloaded 挑战集上的评估进行了验证。

原作者： Mathews George (Heriot-Watt University Edinburgh), Kathrin Stark (Heriot-Watt University Edinburgh)

发布于 2026-07-15

📖 1 分钟阅读☕ 轻松阅读

原作者： Mathews George (Heriot-Watt University Edinburgh), Kathrin Stark (Heriot-Watt University Edinburgh)

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

想象一下，你正在试图解决一个巨大的、神奇的拼图，每一个碎片都带着一个隐藏的标签。在计算机科学的世界里，这些标签被称为“De Bruijn 指数”。它们是追踪代码中变量的一种巧妙方式，但也极其棘手。你可以把它们想象成一场音乐椅游戏，每当有人坐下时，椅子（变量）的名字就会不断变换。如果你试图将一个拼图碎片（规则）匹配到一个孔洞（目标）上，即使它们实际上是同一个东西，看起来也可能因为戴着不同的帽子而显得截然不同。

长期以来，一个名为 Autosubst 的工具一直是这个故事中的英雄。它就像一个超级聪明的机器人，即使标签被重新洗牌了，也能瞬间分辨出两个拼图碎片是否相同。它通过使用一套神奇的规则（称为 $\sigma$ -演算）将碎片归一化，直到它们看起来完全一致。如果你只是想检查两件事是否相等，这个机器人是完美的。

问题所在：“应用”（Apply）陷阱
然而，这里有一个陷阱：当你试图通过应用一条规则（比如在视频游戏中点击“应用”按钮）来使用这些拼图碎片去解决一个问题时，机器人会陷入困境。它非常擅长说“是的，它们相等”，但它却很不擅长说“如何将这条规则放入这个特定的孔洞中”。

为什么呢？因为有时，一条规则可以有多种方式契合一个孔洞，而机器人如果不借助帮助，并不知道哪一种才是“正确”的那一个。在过去，人类程序员必须承担繁重的体力活。他们不得不以一种奇怪且间接的方式重写规则，或者手动猜测缺失的标签，才能让机器人正常工作。这就像是在尝试把一个方榫头塞进圆孔里，你不是在寻找合适的工具，而是在亲自动手把榫头磨掉一部分。

新思路：一种聪明的猜测策略
本文介绍了一个名为 as_apply 的新工具。你可以把它想象成一个全新的、稍微更具冒险精神的机械臂，旨在抓取那些拼图碎片，并将它们塞进孔洞中，即使这些碎片的标签在初看之下并不完全匹配。

这个新策略并没有在遇到不匹配时放弃或要求人类重写一切，而是使用了一套启发式算法（heuristics，即基于以往观察到的模式所做的有根据的猜测）。它观察孔洞，观察规则，然后说：“我敢打赌，如果我稍微移动一下这些标签，它们就能契合了！”

它是如何运作的（魔术技巧）
整个过程分为两个步骤：

准备阶段： 机器人首先使用可靠的旧版 Autosubst 规则对拼图碎片进行清理，使它们尽可能整洁。
猜测游戏： 接着，它尝试匹配这些碎片。如果碎片不完全匹配，它不会惊慌。相反，它会尝试几种特定的技巧：
- 它会检查这种不匹配是否仅仅是一个简单的“偏移”（比如将变量向上移动一个位置）。
- 它会检查缺失的部分是否仅仅是一个“恒等式”（即什么都不做）。
- 它会寻找在这些拼图中经常出现的常见模式。

如果其中一个猜测奏效了，它就会填补缺失的标签并继续下一步。如果失败了，它会回溯并尝试另一种猜测。

论文说了什么（以及没说什么）
作者们非常谨慎，没有过度吹捧。他们承认这并不是一个能解决所有可能问题的神奇魔杖。

它并不完美： 论文明确指出，有时一个拼图可能有多个解决方案，而这个机器人可能会选错一个。即使存在正确答案，也完全可以构造出一个极其刁钻的例子，让机器人猜错。
这是一个“进行中的工作”： 作者将此描述为一种“进行中的工作（work-in-progress）”方法。他们并不声称已经永远解决了匹配理论中的所有问题。
结果： 他们在两个著名的、极具挑战性的任务——POPLMark 和 POPLMark Reloaded 上测试了这个新策略。这些任务就像是证明编程语言属性的“奥林匹克”。
- 在 POPLMark 挑战赛（642 行代码）中，他们使用了该新策略 15 次。
- 在 POPLMark Reloaded 挑战赛（683 行代码）中，他们使用了 10 次。
- 在所有这些案例中，该策略都成功解决了目标。

结论
论文表明，虽然这种新策略在理论上存在局限性（可能会被非常古怪的、对抗性的拼图搞糊涂），但在现实世界中表现得惊人地好。它允许程序员停止以那种奇怪且间接的方式重写规则，而是直接自然地编写规则。

作者们持乐观但谨慎的态度。他们认为这种方法可以在许多实际案例中取代旧有的、笨拙的方法，但他们也知道要确保机器人永远不会选错方案，仍有大量工作要做。他们目前正在努力确定究竟哪些类型的拼图可以由这个机器人以 100% 的确定性来解决，而哪些可能仍然需要人类进行复核。

简而言之，这是一个聪明且有帮助的新工具，它让匹配拼图碎片这项杂乱的工作变得容易得多，尽管它还没有准备好成为工具箱里唯一的工具。

技术摘要：Autosubst 中的模式匹配策略

问题陈述
本文针对 Autosubst 框架中的一个特定局限性进行了研究。Autosubst 是一个用于 Rocq（原 Coque）证明助手的代码生成器，旨在通过 $\sigma$ -演算自动化处理关于 de Bruijn 项和替换的推理。虽然 Autosubst 通过 asimpl 策略成功实现了无假设目标的等价性检查自动化，但在用户尝试通过标准策略（如 apply 或 eapply）将假设（例如类型规则或引理）应用于目标时，该框架会失效。

在这些场景中，用户必须在 $\sigma$ -等价模下将目标与假设进行统一。然而，Autosubst 的自动化设计并非针对假设进行匹配。因此，用户被迫采用繁琐的变通方法，例如：

使用间接形式（使用新鲜的元变量而非直接的替换项）来构建规则。
引入辅助引理以弥合目标与假设之间的差距。
在证明过程中手动转换目标或显式实例化存在变量。

核心困难在于 $\sigma$ -匹配（在 $\sigma$ -等价模下的匹配）并不具有唯一性；单个匹配问题可能会产生多个解，而并非所有解都满足上下文的前提。此外，针对完整 $\lambda\sigma$ -演算的二阶匹配是不可判定的，即使在不考虑 $\beta$ -归约的情况下，解也不一定是唯一的。

方法论
作者提出了一种名为 as_apply 的工作进展阶段启发式策略，该策略在 Rocq 的 Ltac 语言中实现，用于实现模 $\sigma$ -等价的自动化模式匹配。该策略分为两个主要阶段运行：

预处理阶段：
- 使用现有的 asimpl 策略，对目标和目标假设的结论进行相对于 $\sigma$ -演算的归一化。
- 将假设中的量化变量替换为存在变量（evars）。
- 将假设的前提转换为在匹配阶段之后需要解决的子目标。
- 该策略处理显式重命名操作（例如 $s\langle\xi\rangle$ ）与实例化操作（ $s[\xi]$ ）之间的转换，利用 substify 和 renamify。
匹配阶段：
- 策略构建一组匹配方程 $M = \{s_i =_\sigma t_i\}$ ，连接目标项与实例化的假设项。
- 使用部分程序 $\sigma_{min}$ 从左到右处理方程，该程序尝试在 $\sigma_{min}$ 片段（描述实例化和组合性的 $\sigma$ -规则的一个子集）模下进行匹配。
- 启发式算法： 如果 $\sigma_{min}$ $σ_{min}$ 未能找到匹配，策略将应用一组捕捉形式化开发中常见模式的启发式规则。这些规则包括：
  - 处理形如 $s[t \cdot \sigma] =_\sigma ?s[t \cdot id]$ 的方程，通过将未知项实例化为提升后的替换项（ $?s \mapsto s[\Uparrow\sigma]$ ）。
  - 处理涉及恒等替换或特定变量结构的案例。
- 应用替换后，策略对假设进行重新归一化。如果目标与假设在语法上相等，则判定为成功。

该策略已进行泛化，以支持 Autosubst 编译器的完整输入语言，包括多个相互归纳的类型（sorts）、向量替换以及一等公民级别的重命名操作。

核心贡献

引入 as_apply： 一种旨在取代基于 Autosubst 开发中的 apply/eapply 的启发式策略，能够在存在假设的情况下实现模 $\sigma$ -等价的匹配。
泛化： 将匹配逻辑扩展到涵盖 Autosubst 支持的完整语法，包括复杂的绑定器和重命名操作。
实证评估： 将该策略应用于标准的基准测试，特别是 POPLMark 和 POPLMark Reloaded 挑战。

结果
作者在 POPLMark (642 行) 和 POPLMark Reloaded (683 行) 挑战解决方案上评估了 as_apply。

使用频率： 在 POPLMark B 解决方案中使用了 15 次 as_apply，在 POPLMark Reloaded 解决方案中使用了 10 次。
有效性： 在所有测试案例中，as_apply 都成功解决了预定目标。
简化： 该策略的使用消除了以往解决方案中特征性的间接规则构建、辅助引理以及手动目标转换的需求。
局限性： 作者承认 as_apply 并非 $\sigma$ -完备的，也不是一个判定器。由于 $\sigma$ -匹配可能存在多个解，由于其启发式性质，它在理论上可能会在存在正确解时选择一个错误的解，尽管在案例研究中并未观察到此类失败。

意义与主张
论文声称，尽管 $\sigma$ -匹配的理论问题本质上是困难的（非唯一解、完整 $\lambda\sigma$ 中的不可判定性），但一种务实的启发式方法在实践中可以恢复高水平的自动化。其意义在于减轻了处理 de Bruijn 语法的用户的负担，允许他们以直接、自然的形式陈述类型规则和引理，而不是为了适应证明助手统一引擎限制而采用的间接形式。

作者对当前工作的状态保持谦逊，将其标记为“工作进展（Work-in-Progress）”。他们指出，由于存在无限解或多解的可能性，目前的策略依赖于启发式方法。未来的工作旨在确定满足唯一性标准的最大的片段 $\sigma'$ ，从而有望实现一个具有证明保证的匹配策略。

技术摘要：Autosubst 中的模式匹配策略

类似论文