💻 computer science

Fully Evaluated Left-Sequential Logics

本文引入了一种从自由到静态 FEL 的完全求值左序逻辑层级，并以求值树为语义基础，为其二值和三值版本提供了完备的公理化体系。

原作者： Alban Ponse, Daan J. C. Staudt

发布于 2026-05-14

📖 1 分钟阅读☕ 轻松阅读

原作者： Alban Ponse, Daan J. C. Staudt

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

想象你是一位正在准备一道复杂菜肴的厨师。在计算机逻辑的世界里，“食材”是事实（真或假），而“食谱”则是关于如何组合它们的指令。本文介绍了一组被称为**完全求值左序逻辑（FELs）**的烹饪风格。

核心思想很简单：你必须从左到右依次品尝每一种食材，然后才能决定这道菜是否准备好。 你不能跳过任何一步，也不能仅仅因为第一口食材尝起来不好就中途停止。

以下是作者们探讨的不同“烹饪风格”（逻辑）的分解说明，并使用了日常类比。

1. 基本规则：“左序”

在这些逻辑中，顺序至关重要。如果你有一个食谱 A 然后 B，你必须先品尝 A。

那个点： 作者使用一个特殊的点（如 ∧•）来表示这一点。它意味着“先品尝左边。完成后，再品尝右边。”
区别： 在普通逻辑（如标准真值表）中，如果第一部分为“假”，你可能会就此停止，因为整个结果已经确定为假。但在这些逻辑中，你继续下去。无论如何，你都要品尝第二部分。这被称为“完全求值”。

2. 四种“烹饪风格”的层级

本文提出了一个包含四种逻辑的层级结构，从最混乱到最严格。可以将它们视为不同层级的厨房纪律。

层级 1：自由 FEL (FFEL) – “混乱的品尝者”

氛围： 这是最基础、最“自由”的风格。
规则： 你按顺序品尝一切。然而，如果你品尝了同一种食材两次（例如 A 然后又是 A），第二次尝起来可能会不同，因为第一次品尝改变了厨房环境！
类比： 想象品尝一颗柠檬。第一次，它是酸的。但如果你刚挤过汁后立即再尝一次，也许它现在只是一块湿漉漉的果皮。在 FFEL 中，A 和 A 不一定相同，因为第一个 A 可能产生了一个“副作用”（例如改变了环境）。
关键特征： 只有当你承诺食材不会改变时，它才能免疫副作用。由于它允许最大的不可预测性，因此它是“最弱”的逻辑。

层级 2：记忆 FEL (MFEL) – “做笔记的厨师”

氛围： 这位厨师很有条理。
规则： 如果你品尝了一种食材（比如 A），你会把它记在笔记本上。如果在食谱的后面再次遇到 A，你只需查看你的笔记本。你不再重新品尝它。
类比： 想象一名保安在检查身份证。如果他在门口检查了你的身份证，他就不需要在后门再次检查；他记得你。
关键特征： 这消除了“副作用”。一旦一个原子（食材）被求值，其值在整个过程中就被固定了。这使得逻辑更强且更可预测。

层级 3：条件 FEL (CℓFEL) – “灵活的团队”

氛围： 这个团队可以互换位置。
规则： 它像 MFEL 一样（你记得你尝过什么），但现在如果食材不同，你可以交换它们的顺序。A 然后 B 被视为与 B 然后 A 相同。
类比： 想象一群朋友决定去哪里吃饭。如果 Alice 和 Bob 在披萨和寿司之间做决定，谁先说话并不重要；最终的决定是一样的。
关键特征： 这种逻辑等价于一种著名的三值逻辑，称为Bochvar 逻辑。它通过立即将整个菜肴视为“损坏”（未定义）来处理“未定义”的食材（如坏掉的鸡蛋）。

层级 4：静态 FEL (SFEL) – “严格的会计”

氛围： 最严格、最传统的风格。
规则： 这就像标准命题逻辑（如高中数学），但规则是你仍然必须按顺序品尝所有食材。
类比： 这是“黄金标准”。如果你有一个食谱说“如果鸡蛋坏了，蛋糕就坏了”，这种逻辑会同意。它吸收了所有的混乱。
关键特征： 它非常严格，以至于无法处理“未定义”的食材。如果你试图将“未定义”与“假”混合，数学就会崩溃（因为 未定义 变成了 假，这是一个矛盾）。

3. “未定义”的食材 (U)

作者们还探讨了如果一种食材是未定义 (U) 会发生什么。

在“自由”和“记忆”风格中： 如果你品尝了一种未定义的食材，整个过程就会停止或变得未定义。这就像试图用“神秘粉末”烤蛋糕。结果是“神秘蛋糕”。
“吸收”规则： 在最强的三值版本（条件 FEL）中，未定义的食材是“吸收性”的。如果你将 未定义 与任何东西混合，结果就是 未定义。这就像你食谱中的一个黑洞。

4. 逻辑的“树”

为了证明他们的规则有效，作者使用了求值树。

想象一棵家谱树：
- 顶部是主要问题。
- 分支是“左”（真）和“右”（假）路径。
- 底部的叶子是最终答案（真或假）。
创新之处： 在这些逻辑中，树展示了你所走的确切路径。如果你先品尝了 A，然后是 B，树就显示了这段特定的旅程。在“记忆”逻辑中，树更干净，因为它不显示你重复品尝同一种食材。

本文成就总结

作者们不仅描述了这些烹饪风格，还为每一种风格编写了规则手册（公理）。

他们精确定义了如何组合食材（方程）。
他们证明了这些规则手册是完备的（涵盖所有可能的情况）且独立的（没有规则是多余的；你不能移除任何一条而不破坏系统）。
他们使用计算机工具（Prover9 和 Mace4）来双重检查他们的数学，确保没有人为错误混入。

简而言之： 本文描绘了一系列逻辑系统的谱系，在这些系统中，你被迫按顺序品尝每一种食材。它始于一个混乱的系统，其中食材可能会改变；过渡到一个你记得尝过什么的系统；然后到一个顺序无关紧要的系统；最后到一个表现得像标准数学的严格系统。他们为每种风格提供了精确的数学定律。

技术摘要：完全评估左序逻辑

问题陈述
本文旨在形式化并公理化“完全评估左序逻辑”（FELs）。与短路逻辑（SCLs）不同（后者在复合表达式的结果确定后停止评估），FELs 规定了一种“完全”或“严格”评估的策略：无论原子命题的值是否为得出最终结果所严格必需，表达式中的每一个原子命题都必须被评估。这一策略的动机源于编程环境，其中必须确保表达式中所有原子产生的副作用（例如状态变更）均会发生。作者旨在定义此类逻辑的层级结构，从最弱的（自由 FEL，Free FEL，对原子副作用免疫）到最强的（静态 FEL，Static FEL，表现为经典命题逻辑的序列版本）。此外，本文还将这些逻辑扩展至三值设定，以处理“未定义”（ $U$ ），这是编程和逻辑中的常见特征（例如除以零）。

方法论
作者采用基于评估树的语义框架，该概念源自其先前的工作 [19]。

语义：评估树是二叉树，其中内部节点代表原子，叶子节点代表真值（ $T$ $T$ 、 $F$ $F$ 或 $U$ $U$ ）。从根到叶的路径模拟评估序列。
- 在**自由 FEL（FFEL）**中，树结构严格保留评估顺序，并允许同一原子重复出现，以此模拟潜在的副作用。
- 在**记忆 FEL（MFEL）**中，语义得到细化，使得树中没有任何路径包含同一原子的多次出现；若再次遇到某原子，其评估结果将被“记忆”。
- 在**条件 FEL（CℓFEL）**中，逻辑引入了原子的交换律，实质上视独立原子的顺序为无关紧要。
- 在**静态 FEL（SFEL）**中，逻辑坍缩为命题逻辑的序列版本，其中吸收律成立。
三值扩展：除 SFEL 外，作者为所有逻辑引入了常量 $U$ （未定义）。语义扩展至叶子节点属于 $\{T, F, U\}$ 的树，其中 $U$ 充当吸收元素（例如 $U \land_r x = U$ ）。
公理化：主要的方法论贡献是为每种逻辑推导出了完备的等式公理化系统。作者定义了范式（例如 FEL 范式、 $\sigma$ -范式）以证明完备性。他们利用定理证明器 Prover9 验证可推导性，并利用 Mace4 生成有限反模型以证明公理的独立性。

主要贡献与结果

二值 FEL 的层级结构：
- 自由 FEL（FFEL）：最弱的逻辑，由集合 $EqFFEL $公理化。它否定幂等性（$ x \land_r x \neq x$），但满足结合律。它是无副作用约束的完全评估逻辑。
- 记忆 FEL（MFEL）：通过在 FFEL 基础上增加一个公理（具体为 $(x \lor_r y) \land_r z = (\neg x \land_r (y \land_r z)) \lor_r (x \land_r z)$ ）进行公理化。它强制重复出现的原子被视为同一，从而消除副作用。
- 条件 FEL（CℓFEL $_2$ ）：通过在 MFEL 基础上增加交换律（ $x \land_r y = y \land_r x$ ）进行公理化。该逻辑等价于条件逻辑（Guzmán 和 Squier [12]）的二值子逻辑。
- 静态 FEL（SFEL）：最强的逻辑，通过在 CℓFEL $_2$ 基础上增加 $x \land_r F = F$ 获得。它等价于静态短路逻辑（SSCL）以及在序列评估下的标准命题逻辑。
三值扩展（FELU）：
- 作者通过增加公理 $\neg U = U$ 和 $U \land_r x = U$ 定义了三种三值版本（FFELU、MFELU、CℓFEL）。
- CℓFEL（三值条件 FEL）被证明等价于Bochvar 的严格逻辑 [8]。
- SFEL 无法扩展加入 $U$ ，因为吸收律 $F = U \land_r F = U$ 会导致真值的坍缩。
完备性与独立性：
- 为所有定义的逻辑提供了完备的等式公理化系统。
- 作者为每种逻辑提出了替代的、更简洁的独立公理集（例如用于 MFEL 的集合 $MF$），并利用自动化工具进行了验证。
- 构建了范式，以证明范式的语法相等性对应于评估树的语义相等性。

意义与主张
本文声称提供了一个理解完全左序评估的统一框架，弥合了短路逻辑与经典命题逻辑之间的鸿沟。

可预测性：作者认为，与 SCLs 相比，FELs 在评估后对环境状态（副作用）的可预测性更高，因为所有原子都保证会被评估。
表达能力：本文表明，虽然 FFEL 无法表达某些统一的评估树（例如原子在不同分支中以不同结果出现的树），但 MFEL 及更强的逻辑可以表达这些情况，从而提高了逻辑的表达能力。
与现有工作的关系：该工作将 CℓFEL 置于逻辑层级中，表明其等价于 Bochvar 逻辑，且是条件逻辑的子逻辑。它还阐明了 FELs 与短路逻辑（SCLs）之间的关系，指出 FEL 连接词可以在 SCL 框架内定义（反之亦然，在特定条件下），尽管 FELs 执行更严格的评估纪律。

本文结论认为，这些逻辑为推理需要完全评估的表达式提供了坚实的理论基础，提供了完备且独立的公理化系统，有助于自动化推理和验证。