A Logical 3-valued Semantics for Nondeterministic Choice

想象你正站在一个繁忙的控制室里，注视着一个巨大的屏幕，上面监控着一支无人机配送机队。在计算机科学的世界里，这个屏幕代表了一个“逻辑系统”——一套帮助机器决定什么是真、什么是假，以及出错时该怎么办的规则。通常情况下，计算机是非常非黑即白的：灯要么是开着的（真），要么是关着的（假）。但现实生活是复杂的。有时传感器坏了，信号丢失了，或者无人机根本不知道自己在哪里。为了处理这种情况，科学家们发明了“三值逻辑”，它增加了第三个选项：“可能”或“未知”。

然而，当这些“可能”状态遇到“选择”时，会出现一个棘手的问题。想象两架无人机正在尝试选择路径。如果其中一架无人机的地图损坏了（发生错误），整个任务会失败吗？还是另一架无人机会继续前进？旧有的计算机规则就像一个严厉的交通警察：如果一条车道有坑洼，整条路就会关闭。另一些规则则像是一个只看左侧车道的懒惰司机；如果左侧车道被堵住了，他们会立即停止，而不去检查右侧。但在无人机飞行和并行计算的世界里，许多事情是同时发生的。我们需要一种规则来表达：“如果一条路径坏了，也许另一条路径仍然可行，而在我们尝试之前，我们无法确定会选哪一个。”这就是在存在错误的情况下进行“非确定性选择”的难题。

由 Alessandro Aldini 及其团队撰写的这篇论文，正是针对这一难题展开研究的。他们认为，旧有的处理错误的方式在计算机逻辑中过于僵化或过于片面。他们提出了一种全新的思考“或”（OR）选择的方式，尤其是在涉及错误时。他们引入了一种“对称”的规则，不再强求单一答案，而是让计算机能够在一个真实的“抛硬币”过程中，在成功与失败之间做出抉择。他们通过一种被称为“非确定性矩阵”的特殊数学方法证明了其有效性，并展示了如何将其转化为用于检查计算机程序的严格规则集。

问题所在：“懒惰型”与“传染型”

为了理解作者的解决方案，让我们来看看计算机处理信号故障（我们称之为“错误”）的三种旧方式。

1. “懒惰型”方式 (McCarthy)： 想象你在看菜单。如果第一个项目是“毒药”，你会立即停止阅读，甚至不去看第二个项目。许多编程语言就是这样工作的。如果决策的第一部分失败了，整个过程就会停止。问题在于？这不公平。它将选择的左侧视为比右侧更重要。在两个计算机平等协作的世界里，这种“左侧优先”的偏见是不合理的。
2. “传染型”方式 (Bochvar)： 想象一个“传声筒”游戏，如果一个人说错了词，整个信息就会变成乱码。如果计算中的任何部分出现了错误，整个结果都会被宣布为错误。这非常安全，但也过于悲观了。如果一架无人机坠毁了，为什么另一架飞行完美的无人机也要被迫停飞呢？
3. “不确定型”方式 (Kleene)： 这是中间地带。如果一部分损坏了，结果就是“未知”。它不会导致整个系统崩溃，但也不会保证成功。

作者指出，虽然这些规则对于简单的、逐步执行的任务很有效，但在处理并发系统（即许多事情同时发生的系统，如无人机群或服务器网络）时，它们会失效。在这些系统中，如果决策的一个分支失败了，另一个分支可能仍然可以正常工作。旧规则要么让整个系统瘫痪，要么强制执行一种在现实中并不存在的检查顺序。

解决方案：公平的抛硬币

团队引入了一种新的逻辑工具，一种特殊的“或”（他们称之为 $\tilde{\lor}$）。你可以把它想象成计算机的魔法硬币投掷器。

在他们的新系统中，如果你要在“成功”和“错误”之间做选择，计算机并不仅仅是二选一。相反，它承认两种结果都是可能的。

• 如果你问：“我们可以走左边（成功）或者右边（错误）吗？”，答案不仅仅是“是”或“否”。
• 答案是：“可能是‘是’，也可能是‘错误’。我们现在还不知道，而这两种情况都是有效的可能性。”

这被称为对称非确定性。它平等对待选择的两侧。它不在乎你先检查哪一边（不像“懒惰型”方式），也不会让一个错误毁掉整个聚会（不像“传染型”方式）。它只是简单地表示：“如果一条路径坏了，系统可能会成功，也可能会失败，而这本身就是一个真实且有效的世界状态。”

他们是如何证明的

作者并不仅仅是凭直觉认为这行得通，他们建立了一个严密的数学框架来证明这一点。

1. 神奇的表格（非确定性矩阵）： 他们创建了一个特殊的表格（“矩阵”），列出了所有可能的结果。在这个表格中，“成功 或 错误”这一单元格并不只有一个答案，它拥有一组答案：{成功, 错误}。这使得逻辑可以同时持有多种可能性。
2. 规则手册（相继演算）： 他们编写了一套新的规则（“演算”），计算机可以用它来检查程序是否安全。他们证明了这些规则是可靠的（它们从不给出错误答案）且是完备的（它们能找到任何有效问题的答案）。
3. 两个版本： 他们展示了这两种应用方式：
   • 动态式： 每次计算机做出选择时，都会重新投掷一次硬币。这非常适合事物不断变化的系统。
   • 静态式： 计算机选择一条规则后就一直沿用。这更适合需要可预测性的系统。

“深度探索”：五值而非三值

为了让他们的想法更加清晰，作者更进一步。他们意识到，他们三值系统中的“错误”其实是一个谜团。这究竟是一个小故障？一次大崩溃？还是方向性的错误？

于是，他们构建了一个五值系统。他们将那个单一的“错误”框拆分成了三种截然不同的类型：

• 软错误 (Kleene)： 一个系统可以从中恢复的小瑕疵。
• 顺序敏感错误 (McCarthy)： 一种只有在你检查顺序错误时才会发生的错误。
• 致命错误 (Bochvar)： 一个导致一切停止的总崩溃。

他们证明了他们的新型“对称”三值逻辑实际上是这个更详细的五值世界的简化版本。这就像看一张模糊的照片（三值）与看一张高清晰度照片（五值）的区别。模糊的照片在缺乏细节时很有用，但高清晰度照片能解释模糊产生的原因。

这为什么重要

这项工作是连接“我们如何思考逻辑”与“计算机在现实世界中如何表现”之间的桥梁。通过创造一种尊重对称性并允许真实不确定性的逻辑，作者为设计稳健的系统提供了更好的工具。如果你正在构建一个自动驾驶汽车网络或云计算系统，你不希望你的逻辑仅仅因为一个传感器失效就崩溃。你希望系统能说：“那个传感器失效了，但让我们看看另一个是否能接管。”

论文证明了这种“公平”逻辑在数学上是可行的，并提供了构建它所需的精确规则。它表明，通过使用这些新工具，我们可以创造出能更优雅地处理错误的软件。这为验证复杂且易错的系统是否能安全运行开辟了道路，确保当事情出错时，计算机不会直接放弃——它会保持尝试，以公平且符合逻辑的方式继续运行。