Completeness for Probabilistic Boolean Tapes

技術要約：確率的ブール・テープの完全性

問題提起
本論文は、確率的ブール回路のセマンティクスに対する完全な等式公理化の課題に取り組んでいる。確率的ブール回路は、有限確率プログラミングのための弦図（string-diagrammatic）的な基礎として提案されてきたが、先行研究（具体的には[59]）における公理化の試みは不完全であった。先行研究で誘導された同値関係は、意味論的な等価性よりも厳密に粗いものであり、図式 $c$ と $d$ の意味論が比例している（$\langle\langle c \rangle\rangle \propto \langle\langle d \rangle\rangle$）場合にこれらを同一視していた（厳密な等価性ではなく）。その結果、先行研究における特定の公理は、マルコフ核（劣分布）に基づく標準的な意味論に対して不健全であった。さらに、本論文は、部分的なブール回路（出力を生成しない可能性がある回路）がこれまで公理化されていなかったことを指摘している。

手法
著者らは、弦図の理論と圏論を活用し、より単純な構造から完全な確率的言語へと段階的に進むアプローチを採用している。

1. ブール回路 ($Diag_B$): 著者らはまず、集合と関数の圏における射として解釈される、標準的なブール回路の弦図表現を想起する。彼らは、このフラグメントに関するブール代数の公理の既知の完全性に依拠している。
2. 部分ブール回路 ($Diag_{PB}$): 著者らは、シグネチャを「コピ（cocopy）」生成子（$\cap$ で表される）を含むように拡張する。これは「コピー」生成子の双対として機能し、2つの入力を比較し、それらが一致する場合にのみ値を出力する。一致しない場合は出力を生成しない（未定義となる）。これは部分関数をモデル化するものである。著者らは、部分性を制御する公理（結合律、交換律、冪等律、およびフロベニウス則）を備えた、ブール代数を拡張した新しいモノイダル理論 $PB$ を定義する。
3. 確率的ブール・テープ ($T(Diag_{PB})$): 確率的ブール回路の言語 ($Diag_{ }PrB$) を直接公理化するのではなく、著者らは「確率的ブール・テープ」を導入する。この形式体系は、部分ブール回路の圏に凸二重積（convex biproducts）を自由に追加することによって構築される。テープは、テンソル積 ($\otimes$) と凸和 ($\oplus$) という2つのモノイダル構造をサポートする。後者は、テンソル積だけでは不可能な、確率的制御（例：確率的分岐）をモデル化することを可能にする。
4. 圏論的枠組み: セマンティクスは、$KL(D_\le)$（劣分布モノイドのクレイズリー圏）において解釈される。著者らは、テープ図式が PCA 拡張圏 $C^+$ 上の確率行列 ($StMat(C^+)$) の弦図として特徴付けられるという [6] の結果を利用している。具体的には、テープの圏 $T(C)$ が $StMat(C^+)$ と同型であるという事実に依拠している。

主要な貢献

1. 部分ブール回路の完全な公理化:
   本論文は、部分ブール回路 ($Diag_{PB}$) に対する完全な公理系を提示している。これらの公理は、コピ生成子を制御する法則（図3）によって標準的なブール代数を拡張するものである。著者らは、任意の部分回路を「ドメイン（定義域）」回路（関数が定義される場所を決定するもの）と「全域」回路（出力値を決定するもの）に分解することで、完全性（定理9）を証明し、問題を既知のブール回路の完全性に帰着させている。

2. 確率的ブール・テープの完全な公理化:
   著者らは、確率的ブール・テープのための完全な公理化（図4および図5）を提供している。この体系には以下が含まれる：

   • テープ構成のための公理（自然かつ余単位的なモノイド、余点付き凸代数）。
   • 部分性に関する特定の公理（例：失敗した計算を空の分布と等置する）。
   • 代数的構造における標準的な推論原理である、キャンセル可能性を表現する決定的な含意公理（T3）。
     完全性の証明（系29）は、テープと確率行列の間の同型関係に基づき、定義された公理のモジュロとして、 $KL(D_\le)$ における意味論的等価性がテープ計算における等価性と正確に一致することを示している。

3. 回路の等価性のテープの等価性への還元:
   確率的ブール回路から確率的ブール・テープへのエンコーディング $E(-)$ （[8] で確立）を利用することで、著者らは、回路の意味論的等価性のチェックが、それらのテープ・エンコーディングの等価性のチェックに還元されることを示している（系30）。

結果

• 健全性と完全性: 本論文は、提案された公理系が $KL(D_\le)$ における意味論に対して、健全かつ完全であることを証明している。
• 先行研究の修正: 著者らは、彼らのシステムによって誘導される同値関係が、[59] のものよりも厳密に細かいことを示している。具体的には、先行システムの公理 F2 および F7 は不健全であるが、彼らのシステムの公理 F8（[59] より）は彼らのシステム内で導出可能であることを示している。
• テープの表現力: 論文では、テープが $\otimes$ のみに依存する回路よりも、確率的制御をより自然にモデル化できることが示されている。例えば、テープは、全体の合成が null になることなく、有効な計算と失敗（null 行動）の間の確率的選択をモデル化できる。これは、モノイダル積のみを用いるアプローチに固有の制限である。

意義
本論文は、部分ブール回路に対する初の完全な公理化、および確率的ブール・テープに対する完全な公理化を提供することで、その意義を主張している。これらの結果を確立することにより、著者らは、確率プログラミングの図式のレベルで直接的な等式推論を可能にしている。テープへの移行により、確率的制御と部分性を一様に扱う、構造的に透明な公理化が可能となる。著者らは、現在の研究は有限確率プログラミングに焦点を当てているものの、$\oplus$ を伴うトレース（trace）の使用を含む枠組み（具体的には、確率的正規表現の表現の基礎となる可能性のある、確率的プログラム論の代数的基礎）は、将来の研究方向として特定されている。本研究は、データが物理的なリソースとして扱われ、自由なコピーや破棄が妨げられるという「弦図的」な視点に依拠しており、これは確率的および量子コンピューティングの文脈において中心的である。