SAGA定理 — ソフトウェアアーキテクチャが本物の代数幾何になった日

本記事は、Hashnodeに公開したThe SAGA Theorem: The Day Software Architecture Became Genuine Algebraic Geometry の日本語訳です

TL;DR

• すべてのモジュールがレビューを通っているのに、システム全体は壊れている。 この「局所は正しいのに大域で破綻する」現象には、数学の名前があります。コホモロジー、特に H^1 です。
• AAT(Algebraic Architecture Theory)は、ソフトウェアアーキテクチャを「Atom という公理化された事実から生成され、law で切り出され、障害がコホモロジーとして現れる幾何対象」として扱う理論です。
• その AAT で、SAGA 定理(SAGA Grounding Theorem)と呼ぶ定理を Lean 4 で証明しました。アーキテクチャ意味論の側で育てた H^1 と、Atom から生成された site 上の本物の Čech H^1 が一致する、という比較定理です。
• 証明は 352 サイクル。うち 347 サイクルは AI エージェントの自動ループが「この語彙では証明できない」という不可能性定理を積み上げ、最後の 5 サイクルで「law は述語ではなく方程式である」という語彙の転換が岩盤を破りました。
• この記事は、代数幾何のミニ地図から始めて、SAGA 定理の中身と、コンピューターサイエンスにとっての意義までを解説します。

1. 局所は正しいのに、大域で壊れる

こんな経験はないでしょうか。

• 各チームのコードはそれぞれのレビュー基準を満たしている。しかし結合すると壊れる。
• 個々のマイクロサービスは契約どおりに動いている。しかしシステム全体の不変条件が守られていない。
• リファクタリングの各ステップは安全だった。しかし積み重なった結果、当初の設計思想が消えている。

lint や静的解析、依存グラフは「局所の違反」を見つけるのが得意です。しかし上の現象はどれも、局所には違反がないのに起きます。問題は個々の部品ではなく、部品の間の「貼り合わせ」にあるからです。

数学は、この「局所的には整合しているのに、大域的に貼り合わない」という現象を 1 世紀近く研究してきました。層(sheaf)とコホモロジーの理論です。局所データの族が大域データに貼り合うかどうかの障害は、H^1 というコホモロジー群の元として現れます。H^1 の類が零なら貼り合う。零でないなら、どの部品を見ても原因が見つからない種類の破綻が起きている。

AAT は、この数学をソフトウェアアーキテクチャに対して本気で実行する理論です。

2. エンジニアのための代数幾何ミニ地図

本題に入る前に、この記事で使う代数幾何の考え方を整理しておきます。代数幾何は高度な数学ですが、この記事を読むのに必要なのは厳密な定義ではなく、三つの「見方」と、用語の対応表だけです。

見方 1: 式と図形は、同じものの二つの顔

代数幾何は、一言でいえば「方程式の解がなす図形を、方程式の代数を通じて研究する数学」です。x² + y² = 1 という式と、平面上の円という図形は、同じ対象の二つの顔です。式の側の操作が図形の側の操作に対応する — この「代数 ⇄ 幾何」の辞書が理論の心臓部です。

見方 2: 「満たすか」より「どう課されているか」

x = 0 と x² = 0 は、解の集合としてはどちらも「原点だけ」で区別がつきません。しかし式としては別物で、x² = 0 は「二重に零」という情報を余分に持っています。現代の代数幾何は、解の集合という述語的な情報(満たす/満たさない)ではなく、方程式そのものという構造的な情報を対象に据えることで飛躍しました。エンジニアの感覚でいえば、「テストが通るか」だけを見るのをやめて、「どの余裕で、なぜ通るのか」を持ち回るようなものです。この違いが、記事の後半で決定的に効いてきます。

見方 3: 局所で調べて、貼り合わせる

地球全体は一枚の平面地図にできませんが、地図帳(局所的な地図の集まり)にはできます。代数幾何は図形を局所ビューの族で覆い、各ビューで調べ、結果を貼り合わせて大域を理解します。そして「局所ではうまくいくのに、貼り合わせで失敗する」ことがある。その失敗を測る道具がコホモロジーです。

用語ミニ辞書

用語	大ざっぱな意味	エンジニア的なイメージ
ideal(イデアル)	方程式の集まりを「導出で閉じた」形で持つ入れ物	ルール集合と、そこから導出される全ルール
商 O/I	制約 I を課したあとの世界の見え方	制約で「同一視」した後のインターフェイス越しの視界
零点集合 V(I)	制約をすべて満たす点の集まり	全ルールを満たす構成の空間
被覆(cover)と site	全体を局所ビューの族で覆う分け方と、その分け方の正当性ルール	モジュール分割・スコープ分割
層(sheaf)	各局所ビューへのデータの割り当てで、ビューを狭めても整合するもの	スコープを絞っても矛盾なく引き継がれる設定値
コサイクル	局所ビューの境界ごとの「食い違い」の整合的な記録	ビュー境界ごとの差分ログ
コバウンダリ	各ビューの取り直しで解消できる食い違い	ローカルな再調整で消せる差分
H^1	コサイクル ÷ コバウンダリ = 消せない食い違いの類	どこを直しても消えない、系全体の食い違い
零点定理(Nullstellensatz)	述語(解集合)と方程式(ideal)の対応を精密化した定理	観測される挙動と課している制約の対応保証
GAGA	別々の作り方をした二つのコホモロジーが一致するという比較定理	二つの実装が同じ仕様を満たすことの証明

全部を覚える必要はありません。この地図を手元に置いて読み進めてもらえれば大丈夫です。それでは本題に入ります。

3. AAT とは何か — アーキテクチャを相対的な幾何として扱う

AAT(Algebraic Architecture Theory / 代数幾何的アーキテクチャ論)の出発点は、対象の取り方にあります。AAT が扱うのは裸のコードベースそのものではありません。

C : Codebase(コードベース)
V : AtomVocabulary(何を事実として観測するかの語彙)
U : LawUniverse(どんな法を課すかの選択)
J : CoverageTopology(どう局所に分けて見るかの被覆)
k : coefficient ring(障害を測る係数)

X_C^{V,U,J,k} : AAT geometry(これが理論の対象)

つまり「このコードベースは良いか」ではなく、「この語彙で観測し、この法を課し、この分け方で見たとき、どんな幾何が立ち上がるか」を問います。観測の語彙と法の選択を明示して、それに相対的な数学をやる。これが AAT の流儀です。「言えないことは言わない」という境界の規律(理論内部では「語れないことへの沈黙」と呼んでいます)も、この相対化から来ています。

4. Atom の公理 — アーキテクチャの最小事実

AAT の最小単位は Atom です。Atom は「それ以上分解せずに扱う、型付きのアーキテクチャ上の事実」で、5 つの成分を持ちます。

a = (kind, axis, subject, predicate, payload)

• kind: 事実の種別(component、relation、contract、semantic fact など)
• axis: どの構造軸に関する事実か
• subject: 何についての事実か
• predicate: 何が成立しているか
• payload: 値・名前・型・証拠などの内容

「サービス A はサービス B に依存する」「このモジュールは決済の補償処理を担う」「この API は認証を要求する」— こうしたものが全部 Atom です。構文的な事実も、意味論的な責務も、同じ土俵に乗ります。

Atom は公理系(A0〜A8)で縛られています。代表的なものだけ挙げると:

• A0 Primitive Existence: Atom の型が存在し、すべてはそこから生成される。
• A2 Single Fact: 一つの Atom は一つの事実だけを表す。複合的な主張は Atom の族(configuration)で表す。
• A3 Predicate Stability: Atom の同一性は 5 成分の一致で決まる。
• A4 Composition: Atom の有限族が configuration を生成し、そこから architecture object が立ち上がる。
• A5 Law Non-Generation: law は Atom を生成しない。 法は事実の上の制約であって、事実の供給源ではない。

この A5 が地味に重要です。「あるべき論」(law)と「観測された事実」(Atom)を公理レベルで分離しているので、願望が観測に混ざりません。

5. law を「方程式」にする — 代数幾何の辞書

Atom の族の上に、law(法)を課します。「循環依存があってはならない」「補償処理は必ず対になっていなければならない」といった制約です。

素朴には、law は述語です。「成り立つ/成り立たない」の二値。実際、AAT でも law は最初、述語として定義されていました。

しかし代数幾何は、150 年前にもっと良い見方を発見していました。制約を「述語」ではなく「方程式」として扱うのです。ここで第 2 節の辞書が仕事を始めます:

方程式の集合         →  ideal(方程式が生成する代数的対象)
方程式を満たす点     →  零点集合 V(I)(幾何的対象)
制約下で見える関数   →  商環 O/I

ポイントは、述語(満たす/満たさない)は方程式を復元できないことです。ヒルベルトの零点定理(Nullstellensatz)が精密化したように、方程式の側(ideal)には、解集合という述語的な情報よりも多くの構造 — 重複度、無限小、変形 — が宿っています。そしてコホモロジーを計算するために必要なのは、まさにこの余分な構造です。係数のない述語からは、コホモロジーは生えません。

AAT はこの辞書をアーキテクチャに移植します:

law                  →  violation 座標が生成する witness ideal I_L
すべての law の破れ  →  obstruction ideal I_Ob = Σ I_L
law の下での読み     →  商 O/I_Ob(= obstruction sheaf の係数)
law が成り立つ       ⟺  読みを引き戻すと ideal が消える(s*I_Ob = 0)

最後の行が、ヒルベルトの零点定理とまったく同じ形をしていることに注目してください。「law の成立」という意味論的な事実が、「ideal の消滅」という代数的な事実と同値になる。ここが AAT が「代数幾何的」ではなく「代数幾何」である理由です。

さらに、被覆(coverage)を入れます。アーキテクチャをコンテキスト(文脈)の族で覆い、各コンテキストで局所的に観測する。コンテキストの圏の上に Grothendieck topology が Atom から生成され、site ができる。その上の層(sheaf)、そして Čech コホモロジー。局所ごとの読みが大域に貼り合うかどうかの障害が、H^1 の類として現れます。

6. SAGA 定理の前まで — 塔の下層

私はこの構想を、Lean 4 の上で一段ずつ定理にしてきました。

• 有限降下定理: 局所修復の族が大域修復に貼り合うのは、有限 obstruction class が消えるとき、かつそのとき。「local-pass / global-fail」に最初の定理が与えられた段階です。
• 真の H¹ 定理: その obstruction class が、名前だけの H^1 ではなく、本物の商 H^1 = Z^1/B^1(コサイクルをコバウンダリで割ったもの)であること。

ここまでで、AAT は「アーキテクチャの貼り合わせ障害を H^1 で測る」理論になりました。しかし一つ、根本的な弱点が残っていました。

この H^1 は、専用に作られた有限の構成物だったのです。site や sheaf の一般理論は同じリポジトリの中に形式化されていたのに、semantic repair の H^1 はその隣に接ぎ木された別の塔でした。「AAT は代数幾何をやっている」という主張の根拠が、「代数幾何と同じ形の構成を自前で持っている」止まりだった。これでは、任意の ad hoc な有限商を H^1 と呼ぶのと、原理的には区別がつきません。

7. SAGA 定理 — 二つの世界が一致する

この隙間を閉じるために立てたのが、後に SAGA 定理 と名付けることになる目標でした。主張を一言でいうと:

アーキテクチャ意味論の側で育てた semantic repair H^1 は、Atom から生成された site 上の、law から生成された係数による、一般理論の Čech H^1(選んだ被覆に相対的な計算版)の instance として読める。二つの零判定は同値である。

名前の由来は Serre の GAGA(Géométrie Algébrique et Géométrie Analytique)です。GAGA は「代数幾何と解析幾何という二つの世界のコホモロジーが一致する」ことを示した比較定理の金字塔で、SAGA(Sémantique Architecturale, Géométrie Algébrique)は「アーキテクチャ意味論と代数幾何の一致」を示す、その伝統へのオマージュです。そしてこの名前にはもう一つの意味が掛かっています。証明が、文字通りの saga(叙事詩)だったのです。

これが証明されたことで、次の連鎖が全部つながりました。

Atom(公理化された事実)
  → law = 方程式(witness ideal)
  → obstruction 係数 = 商 O/I_Ob
  → Atom が生成する site と被覆
  → 一般理論の Čech H^1
  = semantic repair の H^1(前節の「真の H¹ 定理」のもの)

AAT のコホモロジーは、AAT 自身の公理から生えている。 接ぎ木ではなく。

8. 証明の物語 — 347 の不可能性定理と、一つの決断

SAGA 定理の証明過程は、それ自体がおもしろい研究記録です。

証明は 352 サイクルの反復で行われました。いわゆるループエンジニアリングです — AI エージェントの自動ループが、小さな証明義務を一つずつ Lean で潰していく。各サイクルは敵対的な監査を通り、「結論と等価な前提をこっそり仮定に押し込む」たぐいの弱化は都度弾かれます。ループを速く回すことよりも、ループが何を証明したことになるかを監査で守ることに、設計の重心を置いた形です。

圧縮と封鎖

最初の約 100 サイクルで比較の骨格ができ、その後の約 250 サイクルで奇妙なことが起きます。ループは前進する代わりに、あらゆる迂回路を反例つきで封鎖しはじめたのです。「この入力面からは証明できない」「この補助データを足しても駄目」— 36 系統の不可能性境界が定理として積み上がり、目標全体が最終的にたった一つの命題に圧縮されました。そしてサイクル 320〜347 で、その一点が現行の語彙からは原理的に導出できないことまで証明されてしまいます。

原因は根本的でした。law が holds : Prop、つまり不透明な述語として形式化されていたことです。述語は方程式を決めない。係数のない所にコホモロジーは生えない。第 2 節の「見方 2」と第 5 節の教訓が、Lean の不可能性定理として跳ね返ってきたわけです。

347 サイクルは無駄だったのでしょうか。逆です。理論が、自分の語彙の限界を、拡張する前に定理として確定させた。 どこを直せばよいかが「どこか」ではなく「ここしかない」まで絞られた。数学の形式化でこれをやった例は、そう多くないはずです。

語彙の決断

ここで私は決断しました。「law は方程式である。だからこそ AAT は代数幾何になれる。」

興味深いのは、この拡張に必要な数学が、すでにリポジトリの中にあったことです。AAT の数学本文には、law を方程式として扱うための道具立て — violation 座標、witness ideal、lawful locus — が最初から書かれていました。形式化がそれをまだ使っていなかっただけ。つまりこの決断は新しい数学の発明ではなく、形式化を本文の編集意図に追いつかせることでした。

語彙を換えた後は速かった。obstruction 係数を ideal の商として生成し、局所の読みを defect(ずれ)の商クラスとして生成すると、347 サイクル塞がっていた岩盤の命題 — 「law が局所で成り立てば、共通細分上で読みの制限が一致する」— が定理として落ちました。5 サイクルで、比較定理・零判定の同値・非零クラスが実際に生きている具体例まで、すべてが揃いました。

査読が定理を生む

最後の見どころは査読です。完成直前、4 レーンの敵対的査読のうち数学レーンの一つが veto を出しました。「この合成定理の H^1 零の部分は、構成から自明に真であり、law の意味論はコホモロジーの次数 0 にしか作用していない。誤読を招く」— 正しい指摘でした。

これへの応答は、主張の切り下げではなく新しい定理でした。「law の意味論の寄与は次数 0 の消滅である」という正の境界定理と、「上位の結論群は law と独立に成り立つ」という負の境界定理。理論は、査読を通じて自分自身についての知識を一段深めた。再査読は veto を解除し、定理は受理されました。

9. コンピューターサイエンスにとっての意義

数学の話に見えて、SAGA には CS 的な含意がいくつもあります。

(1) lint の先にある解析のクラス。 局所違反の検出(lint、静的解析、契約検査)と、大域的な貼り合わせ障害の検出は、数学的に別のクラスの問題です。ここで、冒頭の三つの例に戻りましょう。

• 「各チームのコードはレビューを通るのに、結合すると壊れる」 — チームの担当範囲が、被覆の局所ビューに対応します。チーム境界ごとの認識の食い違い(コサイクル)のうち、どのチームが自分のコードをどう直しても消えないもの — それが非零の H^1 類として読めるものです。原因がどのチームの中にも見つからなかったのには、構造的な理由があったわけです。
• 「各マイクロサービスは契約どおりなのに、システムの不変条件が破れる」 — 契約は局所の law、システム全体の不変条件は大域の切断(global section)に対応します。全サービスが局所的に契約を守っていても、それらを貼り合わせた大域切断が存在しないことがある。H^1 が判定するのは、まさにこの存在です。
• 「リファクタリングの各ステップは安全なのに、設計思想が消えた」 — 各ステップは局所の取り直し(コバウンダリ)に対応します。ところが、取り直しを一周分積み重ねると、消えない差分が残ることがある。実は SAGA の証明で非零クラスの実例に使ったのは、文字通り**「円を一周すると 1 だけずれる」**という構成でした。一歩一歩は安全なのに、一周して戻ってきたら別物になっている — あの既視感の、数学的な正体です。

SAGA 以後の AAT は、この障害クラスに対して「検出器の健全性が証明された」装置を持ちます。非零の H^1 類は、どの law がどの観測事実の上で破れているかまで遡れる(traceability)。「どのファイルにもバグはないのに壊れている」という現象に、原理的な検出装置を与える道筋です。

(2) AI が爆速でコードを書く時代にこそ、効く。 AAT の研究目標には、最初から「rival(競合)」という欄がありました。静的解析、依存グラフ、ADL(アーキテクチャ記述言語)、そして膨大なコンテキストでコード全体を読める AI コードレビュー — それらにできないことを AAT は出せているか、と毎サイクル問い続ける規律です。その答えがこの H^1 です。AI エージェントが PR を量産する時代、CI は局所の検査(テスト、lint、契約検査)を高速に回せます。しかし H^1 型の障害は、どの diff にも、どのファイルにも現れません。各 PR は緑、各モジュールは lawful、それでも大域切断が存在しない — この障害は、diff 単位・ファイル単位の検査を原理的にすり抜けます。ADL は構造と適合性を高度に記述できますが、意味論的な責務の貼り合わせ障害を cohomology class として証明する装置は持ちません。コード全体を読める AI レビューでさえ、「全部読んで違和感を語る」ことはできても、障害の存在を定理として固定し、検出器の健全性と反例で支えることはできません。コードが書かれる速度が上がるほど、貼り合わせの障害は速く静かに蓄積します。この種の障害に定理レベルの検出装置を与えられるのは、貼り合わせそのものを数学として扱う理論です。

(3) 形式化における語彙進化の方法論。 大きな形式化プロジェクトは必ず「最初の定義が間違っていた」問題に直面します。SAGA の証明過程は一つの型を示しました: 語彙の限界をまず不可能性定理群として確定させ、拡張を「強制された最小の一手」にする。拡張後も、旧語彙で証明した不可能性境界がそのまま監査装置として生き続ける。定義の変更が「やり直し」ではなく「積み上げ」になる設計です。

(4) 人間と AI の分業の実例。 AI の自動ループによる 347 サイクルの探索と封鎖、人間である私が下した語彙の決断、そして敵対的なマルチエージェント査読(veto と再審)。どれか一つでも欠けたら、この定理はこの形では存在しません。AI が数学をやる時代の協働の型として、証明そのものと同じくらい価値のある記録だと思っています。

(5) 全部が機械検証済み。 上の物語のすべての定理 — 比較も、不可能性境界も、非零クラスの実例も — は Lean 4 でコンパイルが通り、依存公理は Lean 標準のもの(propext、Classical.choice、Quot.sound)だけです。sorry はありません。

10. 正直な境界 — なんでも語れるわけではない。でも、足場としては十分

最後に、AAT の規律に従って、SAGA 定理が主張しないことも書いておきます。箇条書きはどうしても専門的になるので、それぞれに平易な言い換えを添えます。

• 定理は有限または小さい site、選ばれた被覆、law の方程式的実現を備えた語彙に相対化されています。任意の Grothendieck site への無条件の一般化は主張しません。
  • かみ砕くと: 「有限個の部品、明示した分け方、方程式の形に書けた law」の範囲で成り立つ定理です。数学的に考えうるあらゆる無限に複雑な状況までカバーするとは言っていません。
• cover-relative な Čech H^1 と full sheaf cohomology の無条件の同一視は主張しません(むしろ「無条件には言えない」ことが反例つきの境界定理になっています)。
  • かみ砕くと: コホモロジーには「選んだ分け方に相対的な計算版」と「分け方に依らない理論版」があり、SAGA が扱うのは前者です。両者を無条件に同じとは言えないこと自体も、反例つきの定理として固定してあります。
• コードベースから Atom を観測する過程の完全性や、「実コード全体の品質判定」は理論の外側です。AAT は観測された Atom と選ばれた law に相対的な数学をやります。
  • かみ砕くと: 「コードから事実を漏れなく拾えたか」は観測ツールの仕事で、数学は保証しません。AAT が保証するのは、拾った事実と課した law から先の推論の正しさです。

では、この境界は理論の弱さでしょうか。私はそうは思いません。ソフトウェアアーキテクチャの解析は、そもそも有限の営みだからです。モジュールは有限個、観測できる事実も有限、レビューで課すルールも有限。SAGA 定理が成り立つ「有限で、語彙が明示された」世界は、アーキテクチャ解析が実際に住んでいる世界そのものです。なんでも語れる理論ではありません。しかし、ソフトウェアアーキテクチャを解析するための足場としては、十分に広い。

言えないことを言わない。この境界の明示まで含めて、理論の一部です。

11. おわりに

「ソフトウェアアーキテクチャに代数幾何を使う」という言葉は、比喩としてなら誰でも言えます。SAGA 定理がやったのは、それを比喩でなくすことでした。Atom という公理から、方程式としての law、商としての障害係数、site、層、そして H^1 まで — 全部が一本の機械検証された定理の連鎖でつながっている。

局所は正しいのに大域で壊れる、というあの現象には、いまや公理から生えた数学があります。

参考

• リポジトリ: AlgebraicArchitectureTheoryV2(MIT ライセンス)