Completeness for Probabilistic Boolean Tapes

技术摘要：概率布尔带（Probabilistic Boolean Tapes）的完备性

问题陈述
本文解决了为概率布尔电路语义提供完备等式公理化（equational axiomatization）的挑战。虽然概率布尔电路已被提议作为有限概率编程的字符串图表（string-diagrammatic）基础，但之前的公理化尝试（特别是文献 [59]）是不完备的。此前工作中诱导的等价关系比语义相等要粗糙，它将图表 $c$ 和 $d$ 视为等价，仅当它们的语义成比例（$\langle\langle c \rangle\rangle \propto \langle\langle d \rangle\rangle$），而非严格相等。因此，先前工作中的某些公理相对于基于马尔可夫核（子分布）的标准语义是不适定的（unsound）。此外，本文指出，部分布尔电路（可能无法产生输出的电路）此前尚未被公理化。

方法论
作者采用了一种分阶段的方法，从更简单的结构转向完整的概率语言，利用了字符串图表理论和范畴论：

1. 布尔电路 ($Diag_B$)： 作者首先回顾了布尔电路的标准字符串图表表示，将其解释为集合与函数范畴中的态射。他们依赖于已知布尔代数公理在该片段中的完备性。
2. 部分布尔电路 ($Diag_{PB}$)： 作者通过引入一个“共复制”（cocopy）生成器（记作 $\cap$）来扩展签名，该生成器是“复制”（copy）生成器的对偶。该生成器比较两个输入，仅在两者一致时输出值；否则不产生输出（未定义）。这模拟了部分函数。作者定义了一个新的单子理论 $PB$，它通过控制此部分性的公理（结合律、交换律、幂等律和 Frobenius 定律）扩展了布尔代数。
3. 概率布尔带 ($T(Diag_{PB})$)： 作者并非直接对完整的概率布尔电路语言 ($Diag_{PrB}$) 进行公理化，而是引入了“概率布尔带”。该形式化是通过在部分布尔电路范畴中自由添加凸双积（convex biproducts）构建而成的。带支持两种单子结构：张量积 ($\otimes$) 和凸和 ($\oplus$)。后者允许模拟概率控制（例如，概率分支），而仅靠张量积无法实现这一点。
4. 范畴框架： 其语义被解释在 $KL(D_\le)$ 中，即子分布单子的 Kleisli 范畴。作者利用了 [6] 中关于带图表是 PCA 丰富范畴 $C^+$ 之上随机矩阵的特征化结果。具体而言，他们依赖于带范畴 $T(C)$ 与 $StMat(C^+)$ 同构这一事实。

核心贡献

1. 部分布尔电路的完备公理化：
   本文提出了部分布尔电路 ($Diag_{PB}$) 的一组完备公理。这些公理通过控制“共复制”生成器的定律扩展了标准布尔代数（图 3）。作者通过将任何部分电路分解为一个“定义域”电路（确定函数何时有定义）和一个“全函数”电路（确定输出值）来证明其完备性（定理 9），从而将问题简化为已知布尔电路的完备性。

2. 概率布尔带的完备公理化：
   作者为概率布尔带提供了完备公理化（图 4 和图 5）。该系统包括：

   • 关于带构造的公理（自然且相干的单子、共指向凸代数）。
   • 关于部分性的特定公理（例如，将失败的计算等同于空分布）。
   • 一个关键的蕴含公理 (T3)，表达了消去律（cancellativity），这是代数结构中的一种标准推理原则。
     完备性证明（推论 29）依赖于带与随机矩阵之间的同构，表明 $KL(D_\le)$ 中的语义相等恰好对应于在定义的公理下带演算中的相等。

3. 将电路相等性归约为带相等性：
   通过利用从概率布尔电路到概率布尔带的编码 $E(-)$（如 [8] 中确立），作者证明了检查电路的语义相等性可以归约为检查其带编码的相等性（推论 30）。

结果

• 适定性与完备性： 本文证明了所提出的公理系统对于 $KL(D_\le)$ 中的语义既是适定的也是完备的。
• 对前人工作的修正： 作者表明，其系统诱导的等价关系比 [59] 中的关系更精细。具体而言，他们证明了先前系统的公理 F2 和 F7 是不适定的，而他们的公理 F8（源自 [59]）在他们的系统中是可导出的。
• 带的表达能力： 本文说明了带比仅依赖 $\otimes$ 的电路能更自然地模拟概率控制。例如，带可以模拟在有效计算与失败（空行为）之间的概率选择，而不会导致整个组合变为空，这是仅使用单子积的方法所固有的局限性。

意义
本文声称其意义在于提供了第一个针对部分布尔电路的完备公理化，以及针对概率布尔带的完备公理化。通过建立这些结果，作者使得直接在图表层面进行概率编程的等式推理成为可能。向“带”的转变允许了一种结构透明的公理化方式，能够统一处理概率控制和部分性。作者指出，虽然目前的工作侧重于有限概率编程，但该框架（特别是使用 $\oplus$ 的迹/trace）可以为概率程序逻辑和概率正则表达式的表示提供潜在的代数基础，尽管这些被识别为未来的研究方向而非当前结果。这项工作依赖于“字符串图表”视角，即数据被视为物理资源，防止了自由复制或丢弃，这在概率和量子计算语境中是核心所在。