draft v0 — 各判定は要再audit STEP 未採番 2026-09-18

適用05 — アルゲブラ・コアルゲブラを超える

型の棲家。四欄が圏論的に二つに割れる。

藤本 伸樹 ／ Rei-AIOS ／ prior-art audit v0

draft v0 — 各判定は要再audit。STEP 未採番。素材のみ。shared tree 不触。 作成: 2026-09-18 / 前提: decision-device-type-prior-art-audit-v0.md の4欄 関連: [[d-fumt]]（★ §5 に直接影響）／ [[proof-pipeline-device-map]] PIN 5・PIN 6 ／ [[collatz-analysis]]

0. 位置づけ — これは5件目の「対象」ではない

前4件は「超える対象」があった。本件は違う。

アルゲブラ／コアルゲブラは、判定器の型そのものが棲んでいる数学である。

そして本 audit の結論は、型の4欄が二つに割れることである。

欄 圏論における地位
V（値域） 1973年から完全に吸収済み。 Lawvere の V-enrichment により、2値・多値・距離は「同じ定義の quantale 違い」にすぎない
t（全域性） 部分性は決定可能性の問題であって圏論の問題ではない（適用04）
e（誤り率） 圏論は扱わない
c（較正） 圏論は扱わない。 verdict が定義なので「誤りである」という概念が存在しない

この分割が本件の全部である。 V を新規と名乗ることは不可能で、e と c は圏論の外側にある。

1. 「超える」の分岐

分岐 内容 判定
A. より一般の枠組みを作る dialgebra など、代数と余代数を包摂する構造 KILL §3.1
B. コアルゲブラを置き換える 後継フレームワークを立てる KILL §3.2
C. 値域を多値化して超える 4値・8値の verdict 領域 KILL（最重要） §3.3
D. 分配則の壁を超える 効果の合成 CONFINE §3.4
E. 証明書として扱って超える 双模倣を出荷可能な証明書にする SURVIVE §4

2. コアルゲブラとオートマトンの正確な関係

2.1 「オートマトンはコアルゲブラである」の正確な形

函手 F = 2 × (−)^A に対し、Set^F は「初期状態を持たない決定性オートマトン」の圏と圏同型である。 同値ではなく同型 — データが文字どおり同じだから（状態集合、カリー化した遷移関数、受理述語）。

函手が与えないもの3つ：

  1. 初期状態は代数的である。 Rot（ENTCS 325, 2016）が明示する通り、初期状態は L-代数 [g, ι] : A×X + 1 → X の側に属する。古典的な5つ組 (Q, A, δ, q₀, F) は綺麗に割れる — (Q, δ, F) がコアルゲブラ（可観測性 → 言語意味論 → finality による最小化）、(Q, δ, q₀) がアルゲブラ（到達可能性 → initiality による最小化）。完全な DFA は pointed coalgebra であり、点は追加データ。

    ★ これが Brzozowski の二重反転最小化が initiality 構成と finality 構成の合成である理由。

  2. 有限性は不可視。 Set^F は終余代数 P(A*)（非可算）を含む。「有限状態」を表現する手立てが函手にない。正則性は終余代数における像の性質（導関数が有限個）として後から切り出される。決定可能性と計算量 — オートマトン理論の実務的な芯 — は枠組みの外側にある。

  3. 2 を超える受理条件は外付け。 Büchi・parity は F に符号化できない。Kupke & Venema（arXiv:0811.1976）は Acc ⊆ A^ω を函手とは別の成分として四つ組に置き、受理を無限二人ゲームで決める。ω-オートマトンの余代数的理論は「coalgebra + game」であって coalgebra 単独ではない。

2.2 ★ 適用04 §3.5 の非対称性に、正確な圏論的棲家がある

適用04 で「四欄は verdict の非対称性を表現できない」と書いた。その非対称は、ここでは構造として現れる。

圏論的側 原理 最小化
可観測性（外から見える） コアルゲブラ finality / coinduction 行動的同値による商
到達可能性（作られうる） アルゲブラ initiality / induction 到達可能部分の切り出し

「受理は結論だが却下は結論でない」という非対称は、「finality は到達可能性を見ない」という構造の影である。 適用04 で型の拡張候補として置いた欄は、実は新しい欄ではなく、代数側と余代数側のどちらを見ているかの区別だった。

→ 適用01 と適用04 に追記すること。

2.3 双対性は双対性ではない — Rutten 自身の警告

"Note that this table is not to suggest that the theory of systems is dual to that of algebras. (If so the paper would end here.)" — Rutten, Universal coalgebra, TCS 249, §1（verbatim）

"many notions that are defined in both worlds in the same way, have entirely different properties."

形式的双対 Coalg_C(F) = (Alg_{C^op}(F^op))^op は定義上の帳簿であって、Set^op は完全原子ブール代数の圏と同値な非具体的圏であり、誰もそこで普遍代数をやらない。非対称は4つ：

  1. 基底圏が自己双対でない
  2. 興味の所在が非対称 — 始代数は中心的だが始余代数は自明、終余代数は最重要だが終代数は自明
  3. 存在条件が双対でない — 冪集合函手 P は始代数（∅）を持つが終余代数を持たない（Lambek + Cantor）。終余代数には有界性／κ-accessibility が要る
  4. 側条件が余代数側にだけ乗る — Rutten の Convention 4.4 は全編で弱引き戻し保存を仮定する。これが無いと bisimilarity と behavioural equivalence が乖離する。代数側に対応する負担はない

3. 各分岐の判定

3.1 分岐 A（より一般の枠組み）→ KILL

dialgebra F(X) → G(X) は確かに両方を特殊ケースとして literally 含む（G = Id で代数、F = Id で余代数）。Poll & Zwanenburg（ENTCS 44(1), 2001）と Voutsadakis は準同型定理・合同／双模倣・部分／商構造が一般化することを示している。

だが両理論の生産的な中身 — Lambek の補題、始／終鎖、帰納法と余帰納法の原理、終余代数の存在定理 — はすべて不動点構造 F(X) ≅ X に依存し、F ≠ Id ≠ G になった瞬間に消える。 Poll & Zwanenburg の abstract 自身が「(余)代数と任意の dialgebra の本質的な違い」を貢献として掲げている。

レバレッジなき一般性。 対照的に bialgebra（Turi–Plotkin）は構造を足して（分配則）定理を得る。dialgebra は構造を引いて何も得ない。唯一生きている応用は inductive-inductive types の意味論。

3.2 分岐 B（置き換える）→ KILL

コアルゲブラを超えると位置づけた研究計画は存在しない。（限定的探索の negative）

証拠3点：

  1. 最も鋭い既知の限界は内側から修理されている。 Abstract GSOS は λ計算を扱えなかった — 応答は Higher-Order Abstract GSOS（Goncharov, Milius, Schröder, Tsampas, Urbat ら、2023–2026 に POPL/LICS/ICFP/FoSSaCS で約10本）。依然として bialgebraic、依然として coalgebraic。誰も枠組みを出ていない。
  2. 隣接分野の構造は吸収されている。 Clarke（arXiv:2108.00390, 2021）が delta lens は comonad の余代数であることを証明。fibration と enrichment は同じ ⟨X, X → FX⟩ の新しい基底設定にすぎない。
  3. ★ 対抗馬に見えるものは coalgebra を引用すらしていない。 Fong の学位論文（decorated cospans）、Baez らの cospan double categories（2025）、Cruttwell ら "Categorical Foundations of Gradient-Based Learning"（ESOP 2022）— いずれも coalgebra に一切言及していない。 引用していないものを超えることはできない。両者は祖先の違う並行伝統であり、指導層は相互作用を呼びかけている（Hansen & Zanasi, SIGLOG News 2022）。

3.3 ★★ 分岐 C（値域の多値化）→ KILL

これが本 audit で最も重要な判定である。

3.3.1 正確な一致 — Kurz, Poiger & Teheux

Kurz, Poiger, Teheux, "Many-valued coalgebraic logic over semi-primal varieties", LMCS 20(3:6), 2024（arXiv:2308.14581）。

結果：D が semi-primal なら、BA 上の任意の自己函手が D 値の多様体へ体系的に持ち上がり、one-step completeness と expressivity（Hennessy–Milner 性）が保存され、公理化も機械的に移送される。

つまり 4値・8値の鎖は解決済みである。 新しい値域を提案しても、一段完全性も表現力も公理化も有限モデル性も決定可能性も、既存の定理から無料で出る。

補助：Lin & Liau（arXiv:2012.05604, 2209.14688）が有限多値 Łukasiewicz 代数・FL_ew 代数に対する一段完全性と有限モデル性を、predicate lifting 経由で確立している。

3.3.2 より一般の一致 — Lawvere 1973

Lawvere, "Metric spaces, generalized logic, and closed categories"（Rend. Sem. Mat. Fis. Milano XLIII, 1973 / TAC Reprints No. 1, 2002）。

本人の 2002 年コメンタリから verbatim：

"The closed interval [0, ∞] of real numbers as objects, ≥ as maps, + as 'tensor' and truncated subtraction as adjoint 'hom', constitute a bona fide example of a complete, symmetric, monoidal closed category V."

"The inclusion of V₀ into V interprets 'true' as zero distance or 'already achieved', but interprets 'false' as infinite distance or 'unattainably expensive'."

V-豊穣圏は集合 X と X(x,y) ∈ V で、単位律（d(x,x) ≤ 0）と合成律（d(x,z) ≤ d(x,y) + d(y,z)）を満たすもの。V = 2 で前順序／関係、V = [0,∞] で距離空間。同じ2公理、quantale が違うだけ。

「2値 vs 多値 vs 距離」は設計空間ではない。1973年から一つの定義のパラメータである。

現代の余代数側での貫徹：Goncharov, Hofmann, Nora, Schröder, Wild（arXiv:2202.07069）の abstract verbatim — "the notion of quantale abstracts over the actual values distances take, thus covering, e.g., two-valued equivalences, (pseudo-)metrics, and probabilistic (pseudo-)metrics."

3.3.3 最も一般の一致 — codensity games

Komorida, Katsumata, Hu, Klin, Hasuo, "Codensity Games for Bisimilarity"（LICS 2019, arXiv:1907.09634）。CLat_⊓-fibration + codensity lifting により、fibration を変えれば verdict 領域が変わり（関係 → 擬距離 → 位相 → 束値）、最大不動点の特徴づけも codensity bisimulation も対応する安全ゲームも一般に導出される。

3.3.4 判定

KILL。 「値域を多値にする」は新規性を主張できない。行動距離（Baldan, Bonchi, Kerstan, König, LMCS 14(3:20), 2018）、量的代数（Mardare, Panangaden, Plotkin, LICS 2016/2017）、graded monads による linear-time/branching-time スペクトル（Dorsch, Milius, Schröder, CONCUR 2019）が、それぞれ別方向から同じ空間を埋めている。

3.4 分岐 D（分配則の壁）→ CONFINE

Zwart & Marsden, "No-Go Theorems for Distributive Laws", LICS 2019 / LMCS 18(1:13), 2022（arXiv:1811.06460）。

方程式理論に対する構文的条件から分配則の不存在を導く3系統の定理。確定した結果：

Turi–Plotkin の Theorem 7.1 により分配則は bialgebraic 枠組みの中身そのものなので、これは枠組みの外縁を定める。「まだ見つかっていない」ではなく「存在しえない」。

判定 CONFINE：ここは「超える」対象ではなく境界である。確率＋非決定性の合成を「超える」と称する提案は、不可能性定理に抵触していないかを先に検査すること。Varacca–Winskel の対処法（確率側の理論を弱め、非アフィン方程式を落として indexed valuation にする）が示す通り、通る道は「超える」ではなく「何を捨てるかを申告する」である。

4. 分岐 E（証明書）→ SURVIVE

4.1 双模倣は証明書である

関係 R が R ⊆ b(R) を満たせば Knaster–Tarski により R ⊆ ν b = ~。関係そのものが証明書で、検査は対ごとの局所的な遷移条件 — 探索不要、O(|R|·|Act|)。適用04 の「閉集合を出して閉性を局所検査する」形と同一。

不同値の証明書は Hennessy–Milner 論理式（JACM 32(1):137–161, 1985）。像有限性の下で s ≁ t なら s ⊨ φ, t ⊭ φ なる単一の φ が存在する。Geuvers（Vaandrager Festschrift, LNCS 13560, 2022）の apartness が構成的な形を与える — 双模倣が余帰納的なのに対し apartness は帰納的なので、証拠は有限の導出木になり、φ はそこから機械的に抽出される。

4.2 ★ 証明書サイズが測られている唯一の場所 — HKC

Bonchi & Pous, "Checking NFA equivalence with bisimulations up to congruence", POPL 2013。

指数的分離（Fig. 5 の族、x+y ~ z の検査）：

対象 サイズ
最小の素の双模倣（HK が計算） 2^(n+1) − 1 対
AC の反鎖 2^(n+1) − 1 要素
HKC の合同を法とする双模倣 2n + 1 対

実測（Table 1、ランダム NFA 1000本／行、2文字）：

n HK 中央値 AC 中央値 HKC 中央値
50 2,511 112 21
70 10,479 150 27
100 58,454 204 36
1000 (OOM) 1,808 228

n=100 で 58,454 対 vs 36 対、約1,600倍。HKC は決定化された到達可能状態の千分の一未満しか探索しない。

4.3 差分候補

候補 内容 判定
A-1 双模倣を format + checker + 実測サイズの揃った出荷可能な証明書にする SURVIVE
A-2 up-to 証明書は naive checker で検査できない、という trade-off の明示 SURVIVE
A-3 値域の多値化 KILL（§3.3）

A-1 の空白の形

format 独立チェッカ 実測サイズ
Heath & Miller FPC（PxTP'15 / JAR'19） ✅ 関係を担ぐ co-inv(Ŝ,·) ✅ Bedwyr 参照実装 ❌
Bonchi & Pous HKC ❌ 実行の内側 ❌（Coq はアルゴリズムを証明） ✅ 本分野最良
mCRL2 / CADP ❌ 肯定側の証明書がそもそも無い ❌ ❌
Coq/Isabelle（paco, coinduction, AmiCo） カーネル項、外部化不可 証明器カーネルのみ ❌
ハードウェアMC（Certifaiger/HWMCC） ✅ AIGER witness circuit ✅ 義務化済み ✅ 幾何平均 1.74×

★ 唯一成熟したシミュレーション関係の証明書生態系はハードウェアにあり、そこでは誰もそれを bisimulation と呼んでいない。

必要な部品はすべて別々に存在する — 正準的形式（対の集合）、自明に検査できる条件（局所遷移条件）、形式の健全性証明（Bonchi–Pous が Coq、Blanchette らが Isabelle で形式化済み）。空白は「どの検証ツールもそれを出力せず、したがって誰も測っていない」ことだけ。 HKC が唯一の例外だが、対の数を効率の統計として測っており、出荷して再検査する成果物としては測っていない。

A-2 — 誰も書いていないトレードオフ

合同を法とする双模倣の証明書は、素の遷移条件では検査できない。 チェッカは合同閉包の所属も検証せねばならず、その健全性は up-to 関数の compatibility に依存する。HKC が達成する指数的圧縮（2n+1 対 2^(n+1)−1）は、より複雑なチェッカという代価を伴う。

これは DRAT 対 RUP のトレードオフそのものであり、この分野で書き下されていない。 適用04 §5.2 の「証明書サイズは不在の構造の量」という観察の、双模倣版。

5. ★★ D-FUMT₈ への直接の影響

[[d-fumt]] に反映が要る。 STEP 2078 で Kato prior art に対し3系統の novelty 主張を恒久禁止したが、本 audit はそれより広い範囲を閉じる。

5.1 閉じる主張

主張 状態
「8値の verdict 値域を持つ判定系」の新規性 主張不可。 Łukasiewicz 鎖 L₇ は semi-primal（Kurz–Poiger–Teheux Example 1.15）。一段完全性・表現力・公理化が既存定理から出る
「2値より豊かな値域を持つこと」自体の新規性 主張不可。 Lawvere 1973 以来、2値・多値・距離は quantale 違いの同一定義
「多値の様相論理を余代数的に扱う」新規性 主張不可。 Lin & Liau（2020, 2022）、Kurz–Poiger（CALCO 2023）、Kurz–Poiger–Teheux（LMCS 2024）
「行動的同値を量的にする」新規性 主張不可。 Baldan ら LMCS 2018、Mardare ら LICS 2016/2017、Dorsch ら CONCUR 2019

5.2 残る主張可能な位置

  1. 各値に操作的意味を与えた特定の8値意味論で、鎖でも bilattice の twist-product でもないもの。ただし「D-FUMT₈ は Belnap ではない（core-4 のみ）」という STEP 2081/2083 の但し書きと整合させること
  2. semi-primal でも quantale でもない値代数。持ち上げ定理が本当に適用されない場合に限る
  3. ★ 較正 — §6 の通り、これは圏論の外側にある。ただし数学的新規性ではなく metrology の主張として位置づけること

5.3 Belnap FOUR についての注意

△ 本 audit の推論であって、論文の記述ではない。 Belnap の FOUR は素の De Morgan 代数としては semi-primal でないと推論される — t と f を固定して2つの中間元（both / neither）を入れ替える非自明な自己同型があり、項演算は自己同型で保たれるので T_⊤ が項定義不可能、よって Theorem 1.14(4) により semi-primal でない。

ただし 同じ定理により、signature に T_d 演算を足せば semi-primal になり、枠組みの内側に入る。

したがって「Belnap 値の余代数的様相論理は存在しない」は探索範囲内の negative であり、かつ枠組みが明示的に許可する signature 拡張の後には成立しない。

隣接する既存物：Rivieccio, Jung, Jansana「Four-valued modal logic: Kripke semantics and duality」（J. Logic Comput. 2015、代数的・双対性的、余代数への言及なし）／Cruz, Madeira, Barbosa「A Logic for Paraconsistent Transition Systems」（EPTCS 358, 2022 — 4値真理束の上に距離を載せた遷移系、まさに本件の設計空間の中）。

6. ★ そして c は圏論の外にある — これが SURVIVE の芯

量的コアルゲブラは verdict に測定された誤り率も較正も一度も付けていない。

量的コアルゲブラがやること やらないこと
値域（quantale・距離空間・有限剰余束）を定義する 偽陽性／偽陰性率
持ち上げ（Kantorovich / Wasserstein / codensity / fuzzy lax）を定義する 較正曲線
誘導される距離が擬距離であることを証明する verdict への信頼区間
核が bisimilarity であること（d = 0 ⟺ 双模倣）を証明する 「値 v を出したとき正しい確率は p」
論理的特徴づけ（量的 Hennessy–Milner）を証明する
数値的近似保証を与える（van Breugel & Worrell 2006 は強多項式時間で精度 ε）

最後の行が要点である。 その ε は厳密に定義された数学的対象に対する数値近似誤差であって、ground truth に対する verdict の経験的誤り率ではない。

この文献において verdict が「誤りである」という概念は存在しない。verdict が定義そのものだからである。

境界事例は強化学習側にある（Calo ら arXiv:2505.18005, 2025 の標本複雑度、Castro ら MICo NeurIPS 2021、Ferns ら SIAM J. Comput. 2011）が、これも標本から数学的に定義された距離を推定する統計的誤差限界であって、外部の真理に対する較正ではない。

帰結：判定器の型の 4欄のうち、V は既存数学に完全に吸収され、e と c は圏論が扱わない領域にある。 前4件の audit が全部 c の話だったのは偶然ではない。

7. 前件への訂正・補強

7.1 適用01 — 分岐にコアルゲブラが無かった（取りこぼし）

適用01 §1 の分岐 A（表現力で超える）に register/nominal automata・VASS・WSTS 等を挙げたが、コアルゲブラを名指ししていなかった。これは取りこぼしである。コアルゲブラはオートマトンの標準的な圏論的抽象であり、分岐 A の最上位に来るべきだった。

判定は変わらない（対象外）。理由は「60年分の prior art」から「コアルゲブラがオートマトンを含む形で既に一般化を完了しており、その外に出る提案は存在しない（§3.2）」に更新する。

7.2 適用04 §3.5 — verdict の非対称性に圏論的棲家がある

「受理は結論だが却下は結論でない」という非対称は、新しい欄ではなく代数側（到達可能性・initiality）と余代数側（可観測性・finality）のどちらを見ているかの区別である（§2.2）。CONFINE の判定は維持し、根拠をこの構造に差し替える。

7.3 適用04 §5.2 — 「同じ手」の観察に既出の一部がある

適用04 で「FAR・Certifaiger・CeTA・IC3 は全部同じ手（閉集合の局所検査）」と観察し、既出かの確認を反証条件 (c) に置いた。双模倣も同じ手であることが本件で確定した。ただし「不在の証明書」を横断的に扱う枠組みは依然として見当たらない（McConnell ら Certifying algorithms, CSR 2011 が最も一般だが、SAT／停止性／探索に踏み込んでいない）。反証条件 (c)(d) は維持。

8. 反証条件（事前登録）

# 条件 発火時の処置
(a) D-FUMT₈ の8値が semi-primal または quantale の構造を持つ §5.2 の主張可能位置 1・2 を撤回。値域の新規性主張を全面禁止
(b) §5.3 の Belnap FOUR 非 semi-primal の推論が誤り §5.3 を撤回。論文引用に使う前に必ず direct verify すること
(c) 双模倣を format + checker + 実測サイズで扱った既存研究が1件でも出る A-1 を KILL
(d) up-to 証明書のチェッカ複雑性トレードオフを書いた既存文献が出る A-2 を KILL
(e) 量的コアルゲブラが verdict を外部 ground truth に対して較正した例が出る §6 を撤回。本 arc 全体の SURVIVE が消える
(f) コアルゲブラを超えると位置づけた研究計画が出る §3.2 を撤回
(g) 「超える」の語が、§0 の欄の分割以外の根拠で使われている 語を撤回。「型の棲家の同定」に降格

恒久禁止事項（Pattern L 予防）：

9. 引用一覧

✓ = 本 audit で直接確認 / △ = 二次情報・要確認

直接確認 ✓

二次情報・要確認 △

10. この audit の限界