💻 computer science

Labelled Process Logic

本文引入了一个统一的循环标记证明论框架，由系统 G3PPL 和 G3FOPL 组成，该框架通过利用标签对公式进行富化，以在推导过程中显式地追踪轨迹和更新信息，从而实现了对命题过程逻辑和一阶过程逻辑的完整处理。

原作者： Yuanrui Zhang

发布于 2026-06-10

📖 1 分钟阅读☕ 轻松阅读

原作者： Yuanrui Zhang

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

想象一下，你正试图证明一个机器人在迷宫中导航时永远不会发生碰撞。

在旧的方法中（称为“动态逻辑”），你只会检查机器人的最终目的地。你会问：“如果机器人从这里开始并遵循这些指令，它是否会到达安全区域？”这就像只在终点线检查地图。它告诉你是否到达了目的地，但没告诉你途中是否开下了悬崖。

过程逻辑（Process Logic） 是一次升级。它关心的是整个旅程。它会问：“机器人在整个行程中的每一步是否都保持在道路上、避开了悬崖并遵守了规则？”这在证明上要困难得多，因为你必须追踪机器人的整个历史轨迹，而不仅仅是它的最后一个停点。

Yuanrui Zhang 的论文引入了一种名为**标记过程逻辑（Labelled Process Logic）**的新型强大工具来解决这个复杂的数学问题。以下是它的工作原理，使用简单的类比：

1. 问题所在：“拆分”噩梦

想象一下，你正试图证明一个机器人可以安全地通过一段由 A 段和 B 段组成的漫长隧道。

在传统的数学证明中，为了证明整个行程是安全的，你通常必须“拆分”问题。你尝试证明 A 段是安全的，然后证明 B 段是安全的，最后尝试将这两个证明“粘合”在一起。
问题在于，这种“胶水”非常混乱。如果机器人在 A 段的路径改变了 B 段的行为，数学就会变得极其复杂。现有的工具可以处理简单的隧道，但当隧道变得复杂、出现回路或拥有许多可能的路径时，它们就会崩溃。

2. 解决方案：“背包”（标签）

作者的大胆想法是停止在最后尝试将碎片粘合在一起。相反，给证明一个背包（称为“标签”）。

工作原理： 当证明在机器人的指令中移动时，它不仅仅记录“这是否安全？”，它还会记录“我们现在处于第 5 步，机器人向左转了，且电池电量为 80%”。
神奇之处： 这个“背包”（标签）将旅程的历史信息携带在证明过程内部。
- 与其将问题拆分为两个困难的部分，不如直接将新步骤添加到背包中。
- 如果机器人执行了 步骤 A 然后执行 步骤 B，证明只需更新背包，写明 历史记录：步骤 A + 步骤 B。
- 这使得数学变得更加简洁。你不需要复杂的规则来“粘合”事物；你只需要不断向清单中添加发生的事情。

3. 循环问题：“无限长廊”

计算机和机器人经常会有循环（例如，“持续行驶直到看到红灯”）。

如果你尝试用标准数学来证明一个循环，你可能会陷入无限长廊。你证明了第 1 步，然后是第 2 步，然后是第 3 步……由于循环在重复，你永远无法到达证明的终点。
循环修复方案： 作者允许证明“回环自身”。想象一个看起来像蛇吞掉自己尾巴的证明。
- 证明会说：“我正在第 10 步。我知道我曾经在第 1 步。既然规则是一样的，我可以跳回第 1 步并说：‘我已经检查过这部分了，所以没问题。’”
- 安全性检查： 为了确保这不是作弊，作者增加了一条规则：每次证明回环时，它必须证明“背包”（标签）正以一种特定的、缩减的方式发生变化。这就像一个游戏，你只有在饼干罐里的饼干变少时才能进行循环。最终，你会用完饼干，从而证明循环是安全且有限的。

4. 工具的两个版本

该论文构建了该系统的两个版本：

G3PPL（简单版本）： 用于抽象逻辑谜题，你只关心“真”或“假”的状态。它使用标签来追踪简单的路径。
G3FOPL（高级版本）： 用于涉及数字和变量（如 x = x + 1）的现实世界数学。在这里，“背包”不仅追踪路径，还追踪更新。如果机器人改变了一个数字，标签会明确记录该变化（例如，“x 现在是 5”）。这使得系统能够处理带有数学运算的真实计算机程序。

核心结论

该论文声称构建了第一个完整的、可靠的数学框架，能够证明复杂计算机程序整个执行路径的属性，包括包含数学运算的循环。

以前： 我们只能轻松证明程序的终点，或者处理非常简单的路径。
现在： 我们拥有一个统一的系统（利用“背包”和“安全循环”），可以证明简单逻辑和复杂数学程序中复杂的、逐步的行为。

作者证明了这个系统是可靠的（Sound）（它从不撒谎；如果它说程序是安全的，那它确实是安全的）且是完备的（Complete）（它可以证明任何实际上成立的事实）。这是在确保软件从第一秒到最后一秒都完全符合预期行为方面迈出的重要一步。

技术摘要：带标签的过程逻辑 (Labelled Process Logic)

1. 问题陈述

过程逻辑 (Process Logic, PL) 通过将关注点从推理最终程序状态转向推理整个执行轨迹，从而扩展了动态逻辑 (Dynamic Logic, DL)。虽然命题过程逻辑 (PPL) 的命题理论在可判定性和完备性方面已得到充分理解，但其一阶扩展 (FOPL) 面临着重大挑战。

核心难点在于对正则程序进行一阶过程逻辑推理时所需的组合推理 (compositional reasoning)。在标准动态逻辑中，公式 $[\alpha]\phi$ 断言 $\alpha$ 的每一个终止执行都结束于满足 $\phi$ 的状态。而在过程逻辑中， $[\alpha]\pi$ 断言 $\alpha$ 的每一个执行轨迹都满足一个时间性质 $\pi$ （通过线性时序逻辑算子如 next、always、eventually 和 until 来表达）。

现有的针对该逻辑片段的组合演算（例如 Beckert 对确定性 while 程序的序列演算，或 DLT、DTL 等扩展）无法为正则程序（可能是非确定性的）上的全一阶过程逻辑提供完整的处理。具体而言：

对于顺序程序（将轨迹性质 $\pi$ 分割为 $\alpha; \beta$ ）的组合规则，往往过度依赖于特定时序公式的形式（例如针对 “always” 与 “eventually” 的特定规则）。
一些提议的规则对于一般的正则程序是不充分的，因为顺序组合中的测试 (tests) 会阻塞轨迹，从而使简单的组合分割失效。
目前尚无现有系统能提供一个统一的框架，使得轨迹性质和一阶计算能在同一个证明结构中被处理。

2. 方法论：循环带标签证明系统

本文提出了一种全新的证明论框架，通过引入标签 (labels) 来丰富过程逻辑公式，从而显式地记录执行信息，而不是依赖于日益复杂的组合规则。

2.1 带标签公式

作者引入了形式为 $\sigma : \phi$ 的带标签公式，其中：

$\phi$ 是一个过程逻辑公式。
$\sigma$ $σ$ 是一个标签，代表目前为止累积的执行轨迹或程序配置。
- 在命题过程逻辑 (PPL) 中，标签是世界轨迹 ( $\sigma \in L$ )，由世界变量、轨迹变量和连接运算构造而成。
- 在一阶过程逻辑 (FOPL) 中，标签通过程序更新 ( $U$ ) 进行了增强，以记录对算术结构的累积效应（例如 $\{u := e\}$ ）。

这种方法使得中间执行信息在证明系统中变得可用。因此，证明系统不再需要在顺序组合处使用专门用于分割顺序轨迹的规则；相反，它通过在标签中累积信息来展开程序结构。

2.2 循环证明结构

由于正则程序包含迭代 ( $\alpha^*$ )，证明搜索可能会产生无限推导。为了处理这一问题，作者采用了循环证明理论 (cyclic proof theory)。

前证明 (Preproofs)：有限树，其叶节点（芽，buds）可以“回连”到具有相同句法形式（忽略变量重命名）的祖先节点。
循环条件 (Cyclic Condition)：为确保可靠性，并非所有循环都是有效的。论文定义了一个渐进式推导轨迹 (progressive derivation trace)。如果每条无限路径都包含一个“渐进步骤”（例如，应用一个能够降低轨迹或公式复杂度的规则），则该推导是一个有效的循环证明。
可靠性机制：作者通过证明任何满足循环条件的无限推导路径都会导致良基多元集排序 (well-founded multiset ordering) 中的无限下降，从而证明了其可靠性。这一矛盾确保了不会证明无效的公式。

2.3 证明系统

定义了两个特定的系统：

G3PPL：一种用于命题过程逻辑的循环带标签证明系统。它扩展了用于模态逻辑的带标签序列技术，并将其适配于轨迹语义。
G3FOPL：一种用于一阶过程逻辑的循环带标签证明系统。它通过使用赋值规则（更新标签）替换原子程序规则，并添加标准的一阶量词规则，对 G3PPL 进行了扩展。

3. 核心贡献

本文做出了以下具体贡献：

带标签公式：引入了用于 PPL 的轨迹标签和用于 FOPL 的基于更新的标签，从而允许在证明结构内追踪执行历史。
循环带标签系统：定义了 G3PPL 和 G3FOPL，它们共享一个共同的带标签框架，但分别使用针对命题过程逻辑和一阶过程逻辑的特定规则。
可靠性证明：证明了两个系统的可靠性。其论证依赖于将每个渐进的无限推导路径归约为最小反例轨迹的良基多元集排序中的无限下降。
完备性证明：
- 对于 G3PPL，通过证明该带标签系统可以导出已建立的 PPL 希尔伯特风格证明系统的每一个公理和规则，从而确立了其完备性。
- 对于 G3FOPL，通过将经典的针对一阶动态逻辑 (FODL) 的完备性论证适配到基于轨迹的设置中（利用算术编码），确立了其完备性。

4. 结果

统一框架：本文成功构建了一个统一的框架，使得基于轨迹的程序性质和一阶计算可以在同一个证明结构中被处理。
正则程序的完备性：这些系统提供了第一个针对全一阶过程逻辑在正则程序（包括非确定性选择和迭代）上的完整逻辑框架。
可靠性与完备性：G3PPL 和 G3FOPL 均被证明相对于其各自的语义是可靠且完备的。

5. 意义

本文声称这项工作解决了文献中长期存在的空白。以往的系统要么：

仅限于确定性程序（如 DLT, DTL）；
在处理一般正则程序时缺乏完备性；
无法在存在非确定性的情况下统一处理所有 LTL 算子（如 until）。

通过使用标签来外部化执行信息，并使用循环证明来处理迭代，作者提供了一种原则性且统一的机制来对轨迹性质进行推理。这使得验证涉及中间行为的关键规范成为可能，而无需为每个时序算子编写特设的组合规则。该框架统一了命题级和一阶级的处理，为涉及复杂时序性质的程序验证提供了稳健的基础。