TL;DR
- ソフトウェアアーキテクチャの「局所は正しいのに大域で壊れる」現象を数学として定式化し、中心定理を証明し、実在の OSS で計測した論文を、Zenodo に公開しました(DOI: 10.5281/zenodo.21603761、CC BY 4.0)。
- 中心主張はひとつです。壊れ方の測り方を2つ、「どう直せるか」の言葉と「どの方程式が破れたか」の言葉で、互いを参照せずに独立に作ったら、同じ目盛りだった。 これを比較定理として証明しました。
- さらに、一定の貼り合わせ条件の下では、「障害の量がゼロ」と「システム全体を直す修理が実在する」が同値になります。「この修正がなければ全体は壊れていた」という、これまで経験則でしか言えなかった文が、定理の帰結になります。
- 論文は、数学の証明・Lean 4 での機械検証 status・実在マイクロサービスでの再現可能な計測、の三層を、同じひとつのスナップショットに固定して提示します。
0. これまでのあらすじ
このシリーズの目標は、ソフトウェアアーキテクチャを、図と経験則とレビュー上の好みで語る対象から、定義・定理・反例・証明で研究できる数学的対象へ移すことです。初見の方のために、登場するものをまとめておきます。
| 名前 | 何であるか |
|---|---|
| AAT (Algebraic Architecture Theory) | ソフトウェアアーキテクチャの代数幾何的理論。コードから読み取った型付きの最小の事実(Atom)の上に、守られるべき規約を方程式として立て、アーキテクチャを「方程式の解のなす幾何」として扱う |
| SAGA 比較定理 | 今回の論文の中心定理。「修理」の言葉で測った障害と「方程式」の言葉で測った障害が同じコホモロジー類として一致する比較定理。名前は代数幾何の GAGA 定理へのオマージュで、分散トランザクションの Saga パターンとは無関係 |
| ArchSig | AAT に基づく Rust 製の計測ツール。観測データと方程式から、貼り合わせの障害を決定論的に計算する |
| Lean | 定理証明支援系。AAT の定理はここで機械検証される |
前々回は定理の証明の物語を、前回は実在 OSS でのドッグフーディングを書きました。今回は、それらの成果を一本に束ねた初の論文が主役です。シリーズ未読でも前提は本文中で揃います。
1. どのファイルにもバグはないのに、全体は壊れている
実在のマイクロサービス(train-ticket、42 サービス)に、こういう場所があります。
-
order は注文の価格を文字列のまま保管する(
private String price) -
inside-payment はその文字列を
BigDecimalに直して正確に計算する -
cancel は同じ文字列を
doubleに直して 0.8 を掛け、小数第2位に丸める
3つのサービスは、それぞれ自分の規約には完全に従っています。ペアごとの受け渡しも、各々は成立しています。それでも、払い戻しの計算を一周すると帳尻が合いません。
元の価格: 12.33
cancel の規約: 0.8 × 12.33 = 9.864 → 丸めて "9.86"
inside-payment の規約: 正確算術で 9.864
残る差: 0.004(1セント未満)
この1セント未満のドリフトは、どのサービスの帳簿にも記帳されません。しかも 3 サービスの金額を同時に突き合わせるコードは、ソースのどこにもありませんでした。論文はこの実例を one-cent obstruction と呼びます。どのファイルにもバグはないのに、全体は壊れている。
この論文は、この現象を測る数学を作り、その数学の中心定理を証明し、Lean で機械検証し、上の実例で「障害の計測 → CI ゲート遮断 → 修理案の事前検証 → 通過」までを再現可能に一周した、という報告です。
2. 二つの測り方
論文の心臓部はここです。「壊れている度合い」の測り方を、2つ、まったく別の原理で作ります。
測り方A — 修理の言葉。 各サービス(以後チャートと呼びます)には、そこで許される「直し方の部品」があります。one-cent の例なら「金額の読みを scale-2 の BigDecimal に統一する」「丸め剰余を記帳する場所を作る」のような操作です。部品の組み合わせを修理の語と呼び、「結果が同じになる直し方は同じとみなす」という同一視でまとめます。すると各チャートに「意味のある修理の選択肢の空間」ができます。障害は、隣り合うチャートの修理案の食い違いが、ループを一周したときに打ち消せずに残る量として測ります。
測り方B — 方程式の言葉。 こちらは直し方を一切見ません。守られるべき規約を連立方程式として立てます。「両チャートの払い戻し金額は同一の通貨値として確定する」のような等式です。障害は、方程式の破れの残差がループ上に残る量として測ります。
大事なのは、この2つが互いを参照せずに独立に構成されることです。測り方Aの定義に方程式は出てこないし、測り方Bの定義に修理は出てきません。温度計にたとえるなら、水銀の膨張で作った温度計と、放射の色で作った温度計です。原理が違う2本が同じ目盛りを指す保証は、作っただけでは、どこにもありません。
SAGA 比較定理(論文の定理 5.1)は、選ばれた有限の範囲の上で、2つの測り方の局所データを対応させる有限個の条件(チェックリストとして論文に列挙されています)が満たされるとき、次を証明します。
- 2つの測り方が使う目盛り(係数)は、自然に同型である。
- その同型は、2つが測る障害の量(コホモロジー
H^1の類)を同一視する。測り方Aで測った障害類は、ちょうど測り方Bで測った障害類へ移る。 - さらに修理状態の族が貼り合わせの条件(sheaf 条件)を満たすなら、「障害類がゼロ」⟺「システム全体を貼り合わせる修理が実在する」。
ひとことで言えば: 意味論的な診断(どう直すか)と、幾何的な計算(どの方程式が破れたか)は、双方向に翻訳できる。
3. なぜそれが嬉しいのか
「2つの測り方が一致して、何がありがたいの?」— 論文の価値の中心は、この問いへの答えにあります。
その1: 診断と計算の往復切符。 修理の言葉は人間(と LLM)の言葉です。「この3サービスの金額の読みを統一すれば直る」は修理の言葉の文です。方程式の言葉は機械の言葉です。有限の線形代数に落ちて、決定論的に計算できます。比較定理は、この2つの世界の往復切符です。意味の側で立てた診断は幾何の側で計算でき、幾何の側で出た計算結果は修理の言葉で読める。実際、計測ツール ArchSig が計算するのは方程式側で、人間が受け取りたいのは修理側です。その橋が「たぶん対応しているはず」ではなく、証明された同型であることが、この定理の主張です。
その2: 「この修正がなければ壊れていた」が言える。 テストの語彙では、起きなかった障害は観測できません。「あの修正のおかげで障害を未然に防げた」は、いままで接地する場所のない反実仮想でした。定理の第3段(障害類ゼロ ⟺ 大域修理の実在)は、この文に数学的な身分を与えます。修理案を先に与えて障害類が消えることを計算すれば、それは「この直し方なら全体が貼り合う」の実装前の検証です。経験則ではなく、定理の帰結として。
その3: 障害の性質が分かる。 障害類が非零であるとは、「どのチャートが自分の基準をどう選び直しても消えない」という意味です。1つのサービスの規約を張り替えても、そのサービスに接する辺の食い違いが動くだけで、ループ一周分のズレは残る。つまり非零の障害はどのファイルにも帰属しない。直すには規約の張り替えではなく、構造の変更(剰余を記帳する場所を作る、など)が要ります。「犯人探しをしても見つからないタイプのバグ」であることが、計算で判定できるわけです。
4. 論文の作り — 三層をひとつのスナップショットに固定する
論文はこの数学を、性格の異なる三層で提示します。証明・機械検証・計測が、それぞれ別の種類の「本当に?」に答える分担です。
第一層: 数学(第3〜5章)。 上の比較定理の完全な証明。2つの測り方の独立な構成から、係数同型、H^1 同型、障害類の対応、大域修理の同値まで。
第二層: Lean(第6章)。 中心定理の結論束・各段の補題・非零と零の具体例(witness)が、Lean 4 で証明済みです。status 表の全行が proved、sorry はなく、依存公理は Lean/mathlib 標準の3つだけ。これは kernel レベルの公理監査を CI で回して確認しています。
第三層: 計測(第7章)。 §1 の one-cent obstruction で、診断の階段を一周します。
| 幕 | 結果 |
|---|---|
| 修理前の計測 |
MEASURED_NONGLUING_RESIDUAL — 各チャートは自分の規約を守っている(measured_zero)のに、ループ上の残差はチャートごとの基準の取り替えでは打ち消せない |
| ゲート判定 |
BLOCKED_BY_GATE_POLICY — CI ならここで PR が止まる |
| 修理案(BigDecimal scale-2 統一)を与えた計測 | REPAIR_GLUES_WITHIN_SELECTED_COMPLEX |
| 修理前後の比較 | MEASURED_OBSTRUCTION_NO_LONGER_RECORDED_AFTER_CHANGE |
| 修理後のゲート判定 | PASS_WITHIN_GATE_POLICY |
そして三層は、Lean source のタグ、ArchSig のバージョン、計測入力の digest という同定子の組(論文では release identity と呼びます)で、同じひとつのスナップショットに固定されます。論文中のどの主張からも、「それはどの種類の主張で(証明済み / 機械検証済み / 計測済み)、一次証拠はどこにあるか」へ辿れる作りです。数学の正しさは証明が、証明の正しさは Lean が、計測の再現性は固定された入力と手順が担保する。信じてもらう箇所を、できる限り小さくするのが設計方針です。
5. 言っていないこと
シリーズの慣例で、論文が主張していないことを明示します。ここは論文自身が §5.7 と §7.5 で固定している境界です。
- 定理は選ばれた有限の範囲(cover)の上の定理です。 範囲の選び方に依存しない一般のコホモロジーとの同一視は主張していません。
- 定理は無条件ではありません。 2つの測り方の対応には有限個の条件があり、論文はどの証明がどの条件を消費するかまで付録で固定しています。条件のどれか1つを外すと同型が壊れる有限反例も、Lean で証明済みです。
- 計測は「新しい障害を発見した」とは主張しません。 食い違い自体の検出は診断階段の下段の仕事で、SAGA 段の手柄は「局所は合法」「ズレは一周して残る」「この修理案なら貼り合う」を機械の判定として一続きにつないだことです。
- ドリフトの頻度と金額規模は測っていません。 動かして測る runtime 実測は今後の課題で、測っていない数字は語らないのがこのプロジェクトの流儀です。
6. ここからの展望 — SAGA は最初の定理
SAGA 比較定理は、AAT の「局所から大域へ」の能力について証明まで到達した、最初の定理です。塔にたとえるなら一階が建ったところで、論文の第9章は、この上に積む予定の階を研究展望として書いています(証明済みの成果と展望を混ぜないのが論文自身の規律で、以下の2つも展望の側です)。
Architecture scheme。 この論文が測ったのは、1つのアーキテクチャが「貼り合うか」でした。次は、規約の方程式系が定める零点の集まり(scheme)としてアーキテクチャそのものを幾何対象として扱い、アーキテクチャ間の写像・base change・ファイバーを定理化する方向です。うまく育てば、「このリファクタリングは構造を保っているか」「この PR の前後でアーキテクチャは同じ形か、形が変わったならどこか」といった日々の判断に、幾何的な意味 — アーキテクチャ間の検証可能な写像 — を与えられるかもしれません。
SFT (Software Field Theory)。 AAT はある時点のアーキテクチャの整合性を扱う、いわば静力学です。SFT はその幾何の上に、変更・分岐・マージという時間発展の力学を構成する研究です。バージョン管理のマージは局所変更の貼り合わせであり、SFT はこれを降下理論として読みます。目指す中心命題は「アーキテクチャがモジュラーであることと、その未来の進化が descent を満たすことは同値」という形で、SAGA が証明した静的な比較は、この力学が各時刻で使う地盤になります。
7. 読み方ガイドと入手先
論文は英語で書かれています。初見の方には、この順路をおすすめします。
- 要旨と第1〜2章: 問題設定と AAT アプローチ。
- 第7章: one-cent の実測。
- 第5.1節の冒頭: 中心定理の平文サマリ。数式を飛ばしても主張は追えます
- 第9章: 研究展望。「AI がコードを書く時代に、定理に接地した決定論的な計測が果たす役割」の構図はここにあります
- 論文: SAGA: A Comparison Theorem for Local-to-Global Software Architecture(Zenodo、CC BY 4.0、PDF + 再現用 bundle)
- ソース: AlgebraicArchitectureTheoryV2(MIT ライセンス。Lean 証明・ArchSig・計測入力すべてこの中にあります)
- 対象コードベース: FudanSELab/train-ticket
8. おわりに
「局所は正しいのに大域で壊れる」は、integration hell という名前で呼ばれ、経験則で対処されてきた現象でした。この論文が示したのは、そこに正確な数学の名前があること、その名前の下で障害が計算できること、そして「直し方の言葉」と「方程式の言葉」という2つの測り方が、証明された同型で結ばれていることです。
抽象的な比較定理から出発した航路が、機械検証を経て、実在コードの1セントに到達しました。この1セントは、局所的な正しさの総和が大域的な正しさに届かないことの、最小で具体的な証人です。
ご質問やご指摘があれば、気軽にコメントをお寄せください。「うちのコードベースにも、こういう三角形がありそうだ」といったお話も聞かせていただけたら嬉しいです。