代数化时间回溯

# 逆向而行，代数之道
来源：https://arxiv.org/html/2608.17087 © 无  
###### 摘要。线性时序逻辑是命题逻辑的一种模态扩展，用于描述系统在时间上的预期行为。其标准定义域是布尔值，但离散的判断对于引导连续值系统（如神经网络策略、自适应控制器、序列模型等）而言作用甚微。在此类场景中，目标公式的满足程度成为训练信号，可微性成为首要考量。候选的可微语义丰富多样，但驾驭它们却颇具挑战。现有的实现多为浅层嵌入，要求预先选定单一的语义代数及其（通常隐含的）运算规则。本文将读者设想为一名面对此困境却决意突破的函数式程序员。由此突破，诞生了一个代数通用且支持微分的求值引擎，以及一份可接受代数的可执行规范。文中实现了多种代数，并对其正向与反向行为进行了审计。每种代数实质上都是对"失望方向"与"失望方式"的一种选择。所有描述（及更多内容）均已整合至 PyTorch 库 telos 中，可访问 https://github.com/konstantinosKokos/telos。

## 1. 语法
你偶然发现一个逻辑公式，而且它看起来相当温和；其中只包含熟悉的命题联结词，外加几个奇特的符号。某位模糊但无可置疑的权威要求你评估该公式在时间流逝中的有效性。你毫不退缩。当问题进入你的记忆时，这些奇特符号获得了它们的指称。这问题由来已久，且几乎已被解决。你拂去古老权威文献（22 (https://arxiv.org/html/2608.17087#bib.bib1)）的灰尘，回想线性时序逻辑的语法：

φ, ψ ::= ⊤ | ⊥ | α | ¬φ | φ ∧ ψ | φ ∨ ψ | φ → ψ | Xφ | φUψ

\\phi,\\psi ::= \\top | \\bot | \\alpha | \\neg\\phi | \\phi\\wedge\\psi | \\phi\\vee\\psi | \\phi\\to\\psi | \\mathcal{X}\\phi | \\phi\\mathcal{U}\\psi

两个非经典算子中，一个直观明了：\\(\\mathcal{X}\\phi\\)（读作“下一个 \\(\\phi\\)”）就是比当前时刻晚一个时间单位的 \\(\\phi\\)。另一个则需要稍加思考：\\(\\phi\\mathcal{U}\\psi\\)（读作“\\(\\phi\\) 直到 \\(\\psi\\)”）实际上是两个同时许下的承诺：存在一个有利于 \\(\\psi\\) 的时刻，并且在通往该时刻的每一时间单位（包括到达时） \\(\\phi\\) 都承担着为真的重任。一个是逐步推进；另一个是在一次搜索中嵌套了另一次搜索。还有两个符号常被提及：\\(\\mathcal{F}\\phi\\)（读作“最终 \\(\\phi\\)”）和 \\(\\mathcal{G}\\phi\\)（读作“全局 \\(\\phi\\)”）。两者其实都是 \\(\\mathcal{U}\\) 的变体。前者是去掉了附加条件的搜索：\\(\\mathcal{F}\\phi := \\top\\mathcal{U}\\phi\\)；后者则否认存在一个 \\(\\phi\\) 失效的未来：\\(\\mathcal{G}\\phi := \\neg\\mathcal{F}\\neg\\phi\\)。这两者常用于规定时间上的行为：安全性（safety），要求坏事绝不发生；活性（liveness），要求好事终将发生（12 (https://arxiv.org/html/2608.17087#bib.bib2)）。

公式本身只是一半指令。另一半是一个轨迹 \\(\\tau\\)，即公式所描述的世界。轨迹是一个二维赋值：它指明每个原子命题 \\(\\alpha\\) 在有限时间窗口的每个时间单位 \\(t\\) 上的取值。将两者结合，你得到完整的指令：一个判断 \\(\\tau \\models \\phi\\)。你卷起袖子准备动手，说实话，这看起来并非难事；对 \\(\\phi\\) 进行模式匹配，对 \\(\\mathcal{X}\\cdot\\) 将轨迹向右移动一步，对 \\(\\cdot\\mathcal{U}\\cdot\\) 从远端开始扫描，等等。正当你宣布准备就绪时，数据来了。它并非你所预期的。首先，轨迹矩阵不是布尔值。它包含某个 \\(dtype=float32\\) 的数字，并带有一个标记为 \\(requires\\_grad=True\\) 的标志；这是一个 PyTorch（21 (https://arxiv.org/html/2608.17087#bib.bib3)）张量。你畏缩了。这些数字，你得知，是刚从神经网络中挤压出来的，那个标志是连接它们与其生成机制的脐带。数据的发送者并不太关心公式目前的结论如何；他们打算通过持续地微调轨迹的生产者，直到该结论变得有利为止，无论需要多久。你让步了；你对自己的工具极为挑剔和珍视，但妥协有时是必要的。语法转换花了约一小时，包括处理语法糖，你的 ADT 现在通过抽象类继承来模拟。你的第一个语义直觉是进行四舍五入：将任何大于 0.5 的值判定为 True，那么古老文献又重新生效了。取整恢复了你的真值，但代价是一切。步进函数的导数在零和无穷大之间闪烁；无论你结论下游构建了何种损失函数，都无法穿透取整返回到网络中。你的错误在于：当你被要求提供反馈（公式的满足程度）时，你却给出了一个结论（公式是否被满足）；而且这个反馈必须对于轨迹中每个数值都是可微的。那个声音没有谈论布尔值；它谈论的是大写的“值”。你尽职尽责地浏览模糊逻辑的市集（10 (https://arxiv.org/html/2608.17087#bib.bib4)）。你感到头晕；选项太多了，而你又不够投入来亲自做出选择。你耸耸肩：“我想，我就让这个代数通用化，让用户自己选择吧”。

## 2. 抽象语义
你收集并叠加主流代数，将它们不同的地方留白。由此产生的底图是它们共享的抽象蓝图：一个带有两个特殊元素的载体，分别代表 \\(\\top\\) 和 \\(\\bot\\)，以及载体上针对每个逻辑联结词的逐点运算。你没有因为反向传播的义务而放弃纯粹性和内心的平静；PyTorch 可以自行处理这些副作用账簿。你开始书写（111 将 \\(\\text{Fn}\\) 作为难以发音的 Callable 注解的简写。将 \\(\\text{T}\\) 作为 \\(\\text{torch.Tensor}\\) 的简写。将语法错误视为有意的精简（大多数确实是））：

```python
class Algebra(abc.ABC, torch.nn.Module):
    top: T; bot: T
    def meet(self, x: T, y: T) -> T: ...
    def join(self, x: T, y: T) -> T: ...
    def impl(self, x: T, y: T) -> T: ...
    def neg(self, x: T) -> T: ...
```

这些名字是信用借贷自格理论；一个代数是否配得上这些名字，是一个稍后讨论的问题。但是时间呢？那些奇特符号在语义上仍然漂浮不定。锚定它们几乎不费吹灰之力；你很清楚“时序”部分只是披着伪装的一阶量化（即迭代）。时间作为最后一个张量轴进入游戏，所有关于时间的需求都归结为沿着该轴进行某种操作的扫描：

```python
def scan(fn: Fn[[T, T], T]) -> Fn[[T], T]:
    def f(x: T) -> T:
        return torch.stack(
            list(accumulate(x.unbind(-1), func=fn)),
            dim=-1
        )
    return f

def fold(fn: Fn[[T, T], T], initial: T) -> Fn[[T], T]:
    def f(x: T) -> T:
        return reduce(fn, x.unbind(-1), initial)
    return f

def span(fn: Fn[[T], T], neutral: T, bot: T) -> Fn[[T], T]:
    def f(x: T) -> T:
        n = x.size(-1)
        mask = torch.triu(torch.ones(n, n, device=x.device)).bool()
        rows = torch.where(mask, x.unsqueeze(-2), neutral)
        return torch.where(mask, fn(rows), bot)
    return f
```

有了这些，你调配代数的配方终于完成了：

```python
class Algebra(abc.ABC, torch.nn.Module):
    ...
    def running_meet(self, x: T) -> T:
        return scan(self.meet)(x)
    def running_join(self, x: T) -> T:
        return scan(self.join)(x)
    def forall(self, x: T) -> T:
        return fold(self.meet, self.top)(x)
    def exists(self, x: T) -> T:
        return fold(self.join, self.bot)(x)
    def span_meet(self, x: T) -> T:
        return span(self.running_meet, self.top, self.bot)(x)
```

注意悄然发生的事情：派生操作只用那四个抽象原语及其他极少内容就定义了一次。你对此的依赖程度将超出目前的想象；上面的定义与其说是默认实现，不如说是一份碰巧可运行的规范。

## 3. 接口
卷起已久的袖子，终于遇到了它们的模式匹配。求值是对公式结构的递归，每种情况都委托给代数：

```python
class Model(torch.nn.Module):
    def forward(self, A: Algebra, judgement: Judgement) -> T:
        (trace, phi) = judgement
        def go(phi: Formula) -> T:
            match phi:
                case Variable(x):
                    return trace[x]
                case Negation(Until(AbstractTop(), Negation(x))):
                    return A.running_meet(go(x).flip(-1)).flip(-1)
                case Negation(x):
                    return A.neg(go(x))
                case Conjunction(l, r):
                    return A.meet(go(l), go(r))
                ...
                case Next(x):
                    return torch.nn.functional.pad(
                        go(x)[..., 1:], (0, 1), value=A.bot
                    )
                case Until(AbstractTop(), r):
                    return A.running_join(go(r).flip(-1)).flip(-1)
                case Until(l, r):
                    return A.exists(
                        A.meet(A.span_meet(go(l)), go(r).unsqueeze(-2))
                    )
        return go(phi)[..., 0]
```

用 \\(\\llbracket\\cdot\\rrbracket\\) 表示在某个代数和轨迹下的求值器 \\(g\\)。\\(\\mathcal{X}\\cdot\\) 用 \\(\\llbracket\\bot\\rrbracket\\) 填充其未占用的最终时间单位；这是关于时间终结的一种你选择持有的特定悲观主义。\\(\\mathcal{U}\\) 的两个别名适用于对后缀的计算友好搜索，即对反转时间的运行归约；因此“最终”和“全局”只差一个原语。更通用的 \\(\\cdot\\mathcal{U}\\cdot\\) 按照承诺精确读取：\\(\\phi\\) 的每个窗口都与其见证者 \\(\\psi\\) 进行较量，并保留最佳结果。求值器由此完成，完全不受代数特性和 \\(dtyp\\)e 承诺的影响；它能解释在每个已编写（包括尚未编写的）代数下的每个公式。

## 4. 具体语义
在庆祝通用性之前，你通过一次快速回归测试与古老文献达成和解。毫不意外，布尔语义极易恢复：

```python
class Boolean(Algebra):
    top, bot = torch.tensor(True), torch.tensor(False)
    def meet(self, x, y): return x & y
    def join(self, x, y): return x | y
    def impl(self, x, y): return ~x | y
    def neg(self, x): return ~x
```

实例化、求值，答案如期而至。无论抽象最终代价如何，都不会是正确性；古老文献已被降级为蓝图的一个特例。你自信地回到模糊逻辑的市集，刚刚卸下了选择的负担。你开始转录；先是一个辅助类：

```python
class FuzzyBase(Algebra, abc.ABC):
    top, bot = torch.tensor(1.), torch.tensor(0.)
    def neg(self, x): return self.top - x
```

然后是概率论者的默认选择：

```python
class Product(FuzzyBase):
    def meet(self, x, y): return x * y
    def join(self, x, y): return x + y - x * y
    def impl(self, x, y): return torch.where(
        x == self.bot, self.top, (y / x).clamp(max=1)
    )
```

求值器应允了；现在每个判断都返回一个像概率的值。回到之前推迟的信用检查；名字 \\(meet\\) 和 \\(join\\) 带有格理论的义务。结合律、交换律和单调性你一笔带过，对合律和德摩根对偶性也一并处理；所有这些在这个世界的这个角落普遍成立，这一事实经过审计并得以确认。其他值得关注的性质列举如下：

*   **幂等性**：\\(\\llbracket\\phi\\wedge\\phi\\rrbracket = \\llbracket\\phi\\rrbracket\\)
*   **吸收律**：\\(\\llbracket\\phi\\wedge(\\phi\\vee\\psi)\\rrbracket = \\llbracket\\phi\\rrbracket\\)
*   **分配律**：\\(\\llbracket\\phi\\wedge(\\psi\\vee\\xi)\\rrbracket = \\llbracket(\\phi\\wedge\\psi)\\vee(\\phi\\wedge\\xi)\\rrbracket\\)
*   **补余律**：\\(\\llbracket\\phi\\wedge\\neg\\phi\\rrbracket = \\llbracket\\bot\\rrbracket\\)

Product 代数的审计简短且不友好。幂等性立即反弹：\\(x*x\\) 只在定义域边界处与 \\(x\\) 一致。一个固定为 \\(x\\) 的公式 \\(\\phi\\) 会使 \\(\\llbracket\\mathcal{G}\\phi\\rrbracket = x^T\\)；“始终”的值现在与其持续时间挂钩。吸收律和分配律基于相同理由失效，带来更多官僚作风却无新见解。补余律也好不到哪里去：\\(x*(1-x)\\) 持续高于 \\(\\llbracket\\bot\\rrbracket\\)，而中间值本应被排除，实际上却被完美包含。简而言之，Product 代数几乎没有赢得它借用的任何一个名字。没关系；在假设没有定律的情况下，求值器不可能违反任何定律。你仍然记录了审计结果，并屈服于你对自动化的倾向。每个定律都是对其约束的函数的函数：

```python
def idempotent(op: Fn[[T, T], T]) -> Fn[[T], bool]:
    def f(x: T) -> bool: return torch.allclose(op(x, x), x)
    return f

def absorption(meet: Fn[[T, T], T], join: Fn[[T, T], T]) -> Fn[[T, T], bool]:
    def f(x: T, y: T) -> bool:
        return torch.allclose(meet(x, join(x, y)), x) & \
               torch.allclose(join(x, meet(x, y)), x)
    return f
```

严格相等让位于宽松协商，这是有限精度计算的产物。审计变成了引导式的反例搜索：对每个定律与每个代数，在一批（初始）随机张量上循环（3 (https://arxiv.org/html/2608.17087#bib.bib5); 15 (https://arxiv.org/html/2608.17087#bib.bib6)）。测试就位后，其余商品转录同样迅速，审计同样不均（表 1 (https://arxiv.org/html/2608.17087#S4.T1)）。

**表 1. 常见代数，经审计。**  
**Diff.** 标记输入可微的代数；**Train.** 标记参数族，其参数本身是可学习的张量。带字母的条目仅在相应注释指明时成立。定律条目为机械检查。  
a `impl` 对其第一个参数不可微。  
b 当 \\(p \to 0\\)。  
c 当 \\(p \to \infty\\)。  
d 当 \\(p = 1\\)。  
e 对于 \\(p \geq 1\\)。

**Booleans** 居于顶层；唯一的真格。其下方的后代为了可微性的利益而放弃了合规律性。在 \\(\{0, 1\\}\\) 值轨迹上，边界条件毫无余地：单位区间上的每个代数都与 **Boolean** 完全一致（模必要的类型转换）。变化存在于内部。**Robustness** 和 **LSE** 与众不同，它们已完全偏离单位区间。这些是从信号时序逻辑（16 (https://arxiv.org/html/2608.17087#bib.bib7); 6 (https://arxiv.org/html/2608.17087#bib.bib8); 13 (https://arxiv.org/html/2608.17087#bib.bib22)）引入的；它们的载体是扩展实数线，其否定是纯算术：\\(\\llbracket\\neg\\phi\\rrbracket = -\\llbracket\\phi\\rrbracket\\)。表格下半部分是广义的参数族（10 (https://arxiv.org/html/2608.17087#bib.bib4)）：每个都带有一个声明为可学习张量的参数 \\(p\\)，因此代数本身（而不仅仅是它们判断的轨迹）可以接受数值优化。平滑地变化 \\(p\\) 会变形一个代数，直到它遇到一个遵守定律的邻居：Frank、Aczél-Alsina、Dombi 和 Yager 都硬化为 Gödel，LSE 硬化为 Robustness。回顾过去，你欣喜地注意到抽象机制如何一直在充当参考手册，其实例化现在又充当了文献综述。

## 5. 更快的语义
唉，实用性与通用性是对立的。当轨迹超出礼貌性示例的规模时，求值器在未……（此处截断）