この記事はHashnodeに公開したSemantic Geometry of Architectureの日本語版です
TL;DR
- アーキテクチャに表示的意味論はあるか。ある。 ただし古典とは三つの点で違う。構文は観測から生成される。システム全体の意味は自動的には存在せず、存在自体が定理の対象になる。そして意味の破れはエラーではなく、測定対象である
- その存在定理群(大域貼り合わせ、descent、torsor 構造、解像度不変性)は、AAT(代数的アーキテクチャ論)の中で Lean 4 により機械検証済みだ
- 存在定理の先に、もう一つ問いがある。意味たちのなす空間は、どんな形をしているか。 この問いを研究する幾何を Semantic Geometry of Architecture と名付け、研究プログラムとして表明する
- 山頂は Scheme 表現可能性。アーキテクチャが自分自身の意味の空間を持つという予想だ。記事の最後にロードマップを置く。
会議室の可換図式
ある設計議論が、図式一枚で収束したことがある。
紛糾していたのは、二つの処理経路のどちらが正しいかだった。データはこの順で流れるべきか、あの順か。主張は平行線を辿った。そこでホワイトボードに図式を書いた。角が四つ。矢印が四本。この四角形は可換であるべきか。つまり、どちらの経路を通っても同じ結果に着くべきか。
書いた瞬間、議論の性質が変わった。可換であるべき箇所は、合意すべき等式になった。可換でなくてよい箇所は、引き受けるべき判断になった。前者は数分で合意され、後者は判断として決着した。どちらの経路が正しいかという水掛け論は、そこで終わった。
帰り道に考えた。いま起きたことは何だったのか。
プログラミング言語には表示的意味論(denotational semantics)がある。プログラムという構文的な対象に、数学的な意味を割り当てる理論だ。ではアーキテクチャにはあるのか。あの会議室で手で実行されたものの正体は、それではないのか。
この記事は、その問いへの答えとして、一つの研究プログラムの地図を描く。名前は Semantic Geometry of Architecture。アーキテクチャの意味の幾何学。
意味論の歴史の階段
表示的意味論の歴史は、意味が構造を獲得していく歴史として読める。
最初、意味は集合と関数だった。プログラムは入力から出力への関数である。言えることは少なかった。
Dana Scott が意味に順序と位相を与えた。近似の列が極限を持つようになり、再帰が語れるようになった。「このループの意味は、近似の極限である」という文が、初めて数学の文になった。
圏論が合成の構造を与えた。Lawvere の関手的意味論では、理論は圏であり、モデルはそこからの関手であり、意味の等式は図式の可換性である。会議室のホワイトボードに書いたあの四角形は、この伝統の末端にいる。
仕様の抽象模型論(Goguen–Burstall の Institutions)は標語を掲げた。Truth is invariant under change of notation。 真理は記法の変更で不変であるべきだ、と。
一段上がるたびに、言えることが増えた。では、次の段は何か。
この階段に、アーキテクチャは一度も乗れなかった。
乗り場がなかった
表示的意味論は構文から始まる。プログラムでこの構図が成立したのは、構文が言語定義によって最初から与えられていたからだ。パーサが受理するものがプログラムであり、意味論はその解釈として後から定義できた。
アーキテクチャには所与の構文がない。
構文を先に発明する道はあった。アーキテクチャ記述言語(ADL)であり、形式仕様であり、設計文書だ。しかしこの道は宿命を抱え込む。記述と実装の二重管理だ。仕様を書き、コードを書き、両者の乖離を人力で追いかける。乖離はいつか必ず起き、そして記述のほうが負ける。現場のエンジニアなら誰でも知っている結末だ。
乗り場を建てる
構文は書くものではない。観測するものだ。
この方針で乗り場を建ててきた理論がある。AAT(代数的アーキテクチャ論)。ソースコードを Source of truth とし、アーキテクチャを代数幾何の武器で診断する理論で、数学的核は Lean 4 で形式検証されている。
観測によってコードから抽出される型付きの事実を Atom と呼ぶ。「このモジュールはこの状態を書く」「この操作はこのイベントを発行する」「この値はこの意味を指す」。そういう小さな事実の粒だ。Atom が構文の生成元になり、Atom の組み合わせからアーキテクチャの構文(部品の圏、被覆の構造)が生成される。
生成は構文で止まらない。
仕様は law、すなわち方程式として書かれる。「リプレイは状態を再現する」「二つの操作は適用順序に依らない」。そして意味の住む場所(数学で言う係数)も、law を経由して同じ Atom から生成される。表示関数は、独立に与えられた二つの世界を結ぶ橋ではなく、Atom からの単一の生成過程の因子化である。
意味論の全体が、Atom と選ばれた law のほかに外部入力を要さないことは、係数の生成契約から解像度の不変性まで、段階的に Lean 4 で定理化されている。
転回1: 構文は書かれるのではなく、観測される
古典的表示的意味論では、人間が項を書き、意味論がそれを解釈する。ここでは順序が逆転する。実装の観測から構文が立ち上がり、意味論はその上に立つ。
帰結として、意味論は設計時の文書ではなく、測定装置になる。 仕様を先に書いて実装を従わせるのではない。実装を観測し、その観測に対して方程式を立て、成立を測る。二重管理は原理的に発生しない。管理すべき記述が、観測から生成されるからだ。
転回2: 大域的な意味の存在は、定理の対象である
古典版では、表示関数は全域的に定義される。プログラム全体の意味は、定義により常に存在する。アーキテクチャではこの前提が崩れる。
意味はまず局所的に与えられる。個々のコンテキスト(サービス、モジュール、集約)の上でだけ意味が定まっている状態。数学ではこれを切断(section)と呼ぶ。システム全体を覆う部品の族(被覆、cover)を選び、局所的な意味を重なりの上で貼り合わせて、全体で一貫した一つの意味に届いたとき、それを大域切断と呼ぶ。局所を貼り合わせて大域を再構成するこの原理は、数学で descent(降下)と呼ばれる。
「システム全体の意味」は、定義によって自動的に存在するものではない。存在するかどうか、それ自体が定理の対象である。
そしてこの存在定理は、AAT の中ですでに証明されている。重なりの上での食い違いを集計した代数的な指紋を障害類(obstruction class)と呼ぶと、semantic 係数の上で次が成り立つ。
大域的な意味が存在する ⟺ 障害類がゼロ
Nonempty P_sem(W) ⟺ [r_sem] = 0
ここで P_sem(W) は選ばれた被覆 W の上の大域 semantic state の空間、[r_sem] はその被覆から計算される障害類だ。もう一本、同じ形の定理が修理の側にも立つ。law の破れを部品ごとに直せている状態を持ち上げ(lift)と呼ぶ。各部品では直せている。では、全体で同時に直せるか。局所的な持ち上げの族 s が定める類
∂_U(s) ∈ ČechH¹(U, ConDef)
(ConDef は修理方向を集めた係数)について、∂_U(s) = 0 と大域的な持ち上げの存在が同値になる。局所で直せることと全体で直せることの距離が、この類一つに集約される。記号 ČechH¹ の中身は、後の節で 1 セント硬貨を数えながら手で計算する。
存在すれば、一意か。これも定理になっている。大域的な意味は一つに決まらない。解の集合は、被覆全体で整合する自由度を集めた群 H⁰ の作用で、ただ一つの軌道の上を自由に移り合う(torsor 構造)。一意性の代わりに、意味の選択の自由度が群として正確に測れる。
古典的表示的意味論はどこに行ったのか。消えていない。被覆が自明で、障害類が常にゼロになる退化ケースとして、この構図の中に沈んでいる。 アーキテクチャは、その退化の外にいる。
転回3: 破れはエラーではなく、測定対象である
古典版では、可換であるべき図式が可換でないなら、それは意味論の定義の失敗だ。定義を直して可換にする以外の選択肢がない。
アーキテクチャでは事情が違う。結果整合性。並行操作の適用順序。チーム間で読みが食い違うデータ。可換性の破れは、排除すべき欠陥である場合と、設計上引き受けた判断である場合の両方がある。
だから AAT は破れを一級のデータとして扱う。方程式の残差(residual)が消えないとき、それは障害として定義され、有限のデータとして提示され、コホモロジー類として測定される。破れが「ある」だけではない。どの被覆の、どの重なりで、どの類として破れているかが局在化される。
あの会議室の議論が紛糾したのは、参加者が暗黙に異なる可換性の仮定を置いていたからだ。図式を外に出すと、合意すべき等式と引き受けるべき破れが分離する。「どちらの経路が正しいか」は収束しない問いだが、「この破れを引き受けるか」は判断として決着する問いだ。
AAT の棚には、まだ定理がある。測る軸を増やすと、それまで一致していた二つの設計が分離する(Period Separation)。プログラム意味論で full abstraction と呼ばれてきた現象の、アーキテクチャ版だ。この語には歴史の重みがある。Plotkin が言語 PCF についてこの問題を立てたのが 1977 年。意味論は観測的同値を過不足なく捉えるかという問いは、プログラム意味論最大の難問として20年近く立ち続け、1990年代のゲーム意味論でようやく落ちた。Period Separation は、同じ問いがアーキテクチャの水準で再来することの予告である。
一方、同じ軸の中で測定の粒度(読みの解像度)を変えても、較正条件の下で診断は正確に一致する(Atlas 定理)。粗くしても欠陥は消えず、細かくしても捏造されない。条件を破れば両方の事故が起きることまで、有限反例つきで同じ定理パッケージに収められている。矛盾ではない。軸の追加は診断を真に増やし、同一軸内の解像度変更は診断を変えない。二つの定理は、この二方向を分担している。Atlas 定理は意味論の well-definedness 定理であり、Institutions の標語「Truth is invariant under change of notation」の、成立条件と崩壊反例つきの定理化だ。古典的表示的意味論に対応物はない。
存在定理。一意性の自由度。well-definedness。full abstraction。教科書の章立てが、そのまま揃っている。しかもこれらの定理は、意味論のために証明されたのではない。大域貼り合わせは修理理論の途中で。conormal descent は修理方向の探索で。torsor 構造は一意性の失敗の定量化のために。解像度不変性は診断の信頼性のために。別々の動機で積まれてきた定理たちが、一斉に読み替わった。
我々が積み上げてきたものは、自然と一つの意味論につながっていた。
意味の幾何
意味論の階段に戻る。順序と位相の次、圏の次。次の段は何か。
幾何である。
存在定理は「意味があるか」に答えた。しかしその先に、伝統が一度も立てたことのない問いがある。
意味たちのなす空間は、どんな形をしているか。
AAT の代数幾何は、この問いを診断の実質として構成する。
失敗は空間を切り出す。 方程式の失敗は障害イデアルを生成し、合法な設計の範囲(lawful locus)を切り出す。「どこまでが合法か」は判定値ではなく、空間の部分として存在する。
破れは解剖できる。 障害は類として測られるだけでなく、特異点・モノドロミーの語彙で解剖される。同じ「非可換」でも、孤立した貼り間違いと、設計全体を巻き込む捻れは、別の病理だ。要する手術が違う。
修理は変形理論である。 障害イデアル I に対する I/I² という係数(先の ConDef の正体)の双対は、設計をどの方向に一次変形すれば合法へ届くかの接空間を与える。修理候補は場当たりのパッチの列挙ではない。修理候補の空間そのものが、幾何的対象になる。
進化は時間方向の幾何である。 設計変更の履歴は、意味の空間の族として読まれる。
そして、射程の最遠点。
意味がモジュライ空間(意味たちを点として集めた空間)を持つなら、開発とは、その空間の中の軌道である。 リファクタリングは空間内の運動であり、修理は接方向への一歩であり、アーキテクチャが安定して見えるのは軌道が吸引域に入っているからだ。特異点は、流れが滑らかに延長されない点として、文字通りの意味を得る。
静力学と動力学。意味の空間の形が静力学で、その上の開発の運動が動力学だ。可換図式は破れの位置を教える。幾何は、破れの型と手術を教える。
崖の記録
Atlas 定理は、すんなり立った定理ではない。AAT では、定理の証明探索を AI エージェントのループが担い、人間は裁定する。そのループが、自分の証明対象を4回反証した。主張を立て、反例に落とされ、条件を精密化し、また落とされる。その過程で「形だけの条件の継ぎ足しでは原理的に届かない」という no-go が示され、係数の定義そのものが作り直された。4回の反証の各々が、有限反例として Lean のコードベースに残っている。
その定理が最終的にどう立ったかは、Lean のコードで直接見られる。
theorem generatedComparisonH1Map_bijective [Fintype Source]
(M : TargetSupportedNerveMorphism coarseReading fineReading hcoarser
coarse fine)
(laws : FiniteLawFamily Source)
(hcoarse : laws.Adequate coarseReading)
(hfine : laws.Adequate fineReading)
(hC : M.ConditionC laws hcoarse hfine) :
Function.Bijective
(M.generatedComparisonH1Map laws hcoarse hfine)
読み下す。M は粗い読みと細かい読みを結ぶ比較の射。laws は有限の law の族。hcoarse と hfine は、どちらの読みでもその law 族が語れる(adequate)という仮定。結論は、二つの読みの診断 H¹ を結ぶ比較写像が全単射であること。「粗くしても消えず、細かくしても捏造されない」の正確な形だ。そして仮定 hC、較正条件 C の中身こそ、4回の反証が削り出したものだ。反証のたびに条件が一本ずつ足され、no-go が係数の定義を作り直させ、最後にこの形で閉じた。傷跡は、定理の仮定として残っている。
定理本体とは別に、第二のハントも走った。不変性が成立する範囲の境界を、有限の構文的条件で切り出す試みだ。こちらは今も開いている。三世代の候補定義が立て続けに反例に倒れ、最後に残ったのは否定的結果だった。その境界は、隣接する部品までしか見ない登録済みの観測語彙では、原理的に区別できない。 分離の証明は Lean の反例で錨止めされ、定理水準への固定が、いまの登攀目標として立っている。
なぜ崖の話をするのか。崖が描いてある地図だけが、本物の地形の地図だからだ。
反証の記録は失敗の記録ではない。この理論が触っている地形が、比喩ではなく実在することの証明だ。願望で描いた地図に崖は現れない。数学が押し返してくるたびに、地図は正確になった。
岩に触る
崖を見たら、次は岩肌だ。障害類が比喩でないことを、一度だけ計算で確かめる。
AAT のリポジトリには「1セントのドリフト」という実行可能な例がある。Rust で書かれた 3,000 行級のコマースサービスに、一本のプルリクエストが届く。ユニットテストは全構成で green。diff のどの断片も、レビューでは正当化できる。そしてこの PR は、チェックアウト画面の表示より 1 セント多くカードに課金する。
金額は三つのモジュールを流れる。PR の後、三者は別々の丸め規約を話している。デモの買い物かごでは小計 33,990 セント、ロイヤルティ割引 2.5% で、割引の厳密値は 849.75 セントだ。
| モジュール | 規約 | 割引額 |
|---|---|---|
| 表示(checkout) | 総額で四捨五入 | 850 |
| 決済(payment) | 行ごとに銀行丸め | 849 |
| 台帳(ledger) | 丸めない | 849.75 |
実デモの測定はもう少し大きい complex の上で走るが、骨格だけを取り出す。部品と、その部品が担当する範囲の宣言をチャートと呼ぶ。いまの三つのモジュールが、三つのチャートだ。重なり(モジュール間のインターフェース)も三つで、輪をなす。各重なりの上で食い違いを測ると、
r(表示→決済) = 849 − 850 = −1
r(決済→台帳) = 849.75 − 849 = +0.75
r(台帳→表示) = 850 − 849.75 = +0.25
これが障害の生データだ。
修理できるか。修理とは、各チャートの値を、そのチャートの law が許す範囲で動かすことだ。表示と決済は整数セントしか動かせない。画面とカードは整数セントの世界だからだ。台帳は動かせない。厳密であることが台帳の law だからだ。チャート X を c(X) だけ動かすと、各食い違いは
r'(X→Y) = r(X→Y) + c(Y) − c(X)
に変わる。ここで算術が決着をつける。c(表示) と c(決済) は整数で、c(台帳) は 0。だから、どの修理も食い違いの小数部分を変えられない。+0.75 と +0.25 は、あらゆる局所修理を生き延びる。
H¹ とは、測られた食い違いの空間を、局所修理で作れる食い違いの空間で割った商だ。いま生き延びた小数部分が、その商の中の非零の類である。剰余を生んでいるのは、輪の形そのものではない。law が修理に許す動きの乏しさだ。整数でしか動けない者が二人、動けない者が一人。この制約系で商を取った瞬間、どの局所修理でも消せない剰余が、大域の不変量として立つ。 実際に最小化してみるとよい。c(決済) = 1 と動かせば、残差は (0, −0.25, +0.25) まで縮む。だが +0.75 の小数部分が消えない以上、どれかの重なりには必ず 4 分の 1 セントが残る。これがこの設計の障害類の大きさだ。デモでは CI の gate がこの類を検出して PR を止め、規約を統一する修理の後に通す。全工程がリポジトリの example として実行できる。
ついでに、古典の埋め込みも命題になる。被覆が一枚なら、重なりが存在しない。食い違いの置き場が零なので、障害は定義から消えている。これは被覆の選択の退化であって、Atlas 定理が不変性を守る読みの解像度とは別の軸である。プログラム全体の意味が常に存在した古典的表示的意味論は、この算術の退化した特別な場合である。転回2の主張は、修辞ではなくこの計算の一般化だ。
この H¹ は、遠い異国の代物ではない。lint も契約テストも整合性チェッカーも、測っているのは局所条件だ。個々のファイルの中、個々のインターフェースの上。そして「局所修正では消せない食い違い」を測ろうとした瞬間、それは定義により、この商の計算になる。あなたの整合性ツールは、名前を知らずに H¹ を近似している。
この形には、出自がある。量子力学のベルの定理は、層の言葉ではこう述べられる。局所的な観測はすべて整合しているのに、それらを同時に説明する大域切断が存在しない(Abramsky–Brandenburger の層論的 contextuality)。骨格は、前層と、大域切断の不在。いまの計算と同じだ。三つの丸め規約の輪は、局所的にはどれも正しく、大域的な帳簿だけが存在しない。量子力学に古典的な大域説明がないことを示した数学が、マイクロサービスが 1 セントを照合できない理由を測っている。 規模は違っても、形は同じである。
山頂: Semantic Scheme Representability
この地図には山頂がある。まだ誰も登っていない。
代数幾何には Spec という操作がある。可換環(足し算と掛け算のできる代数系)R から、その方程式的な内容を幾何化した空間 Spec R を作る。方程式系を空間として見る、代数幾何の根本操作だ。
予想はこうだ。Atom と law から生成される「係数 R の上での一貫した意味の実現」の集まり Sem_{A,r}(R)(A はアーキテクチャ、r は読みの選択)に対して、ある幾何的対象 M_{A,r} が存在して、自然な全単射
Sem_{A,r}(R) ≃ Hom(Spec R, M_{A,r})
が成り立つ。アーキテクチャ A は、自分自身の意味の空間 M_{A,r} を持つ。 意味の実現を一つ選ぶことは、この空間への写像を一つ選ぶことに等しい。成立すれば、意味の空間は読みの選択や観測の都合から独立した、内在的な幾何的対象として立つ。ここまでの存在定理、自由度、修理の接空間はすべて、この一つの空間の性質として一列に並び直す。
この形は思いつきではない。代数幾何には点の関手という視点の転回がある(Grothendieck の相対的視点)。空間とは、点の集まりとして直接与えられるものではなく、あらゆる係数からの写像の全体で知られるものだ。空間を知ることと、そこへの写像の全体を知ることは同じである(米田の補題)。だから「意味の実現の集まりが、ある空間への写像の全体と一致する」という予想の形は、意味の空間を定義する正統な道をなぞっている。そしてモジュライ問題の歴史は、この道の険しさも教えている。楕円曲線のモジュライは、対象が自己同型を持つせいで fine moduli scheme を持てず、stack という概念の発明を強制した。アーキテクチャの実現が自己同型を持つなら、この山頂も scheme から stack へ上がる。分岐まで含めて、地形は古典に写っている。
この予想の最大の敵は、外の反例ではなく循環定義だ。意味の実現を最初から M への写像として定義してしまえば、表現可能性は空虚に成立する。実現の集まりを Atom と law からの方程式の解として独立に定義し、それが空間への写像と一致することを示して、初めて定理の名に値する。局所的な部分は方程式の解空間の話としてほぼ定義から従う見込みがあり、主張の実質は貼り合わせに集中する。つまりこの予想の核心もまた、descent だ。
死に方も設計してある。表現可能性が scheme の水準で閉じない場合、その障害(実現の自己同型、貼り合わせの高次障害)は失敗ではなく、stack への昇格が必要であることの証拠として換金する。affine の水準で主張が恒真に堕ちた場合は、functor の独立定義を作り直す。反証されたとき何が起きるかまで、先に決めてある。崖の規律は、未来に対しても同じに適用される。
これは予想だ。しかし山頂の位置が見えている地図と、見えていない地図は、別の地図だ。
名前について
この研究プログラムを Semantic Geometry of Architecture と呼ぶ。
語順が内容である。これは幾何を道具にして意味を説明する geometric semantics ではない。意味そのものが空間を持ち、その空間を研究する幾何である。
全体の座はこうなる。
- AAT
純粋数学的土台。意味の空間の静力学 - Semantic Geometry of Architecture
AAT の上に開く研究プログラム。本記事 - SAGA 定理
その中の証明済み定理系列の一つ(貼り合わせ・修理・descent) - Atlas 定理
その中の証明済みの単独峰(解像度不変性、意味論の well-definedness) - SFT (Software Field Theory)
意味の空間の上の動力学。開発という軌道の理論
現在地とロードマップ
いま、どこに立っているか。
振り返ると、歩いてきた道はすべて舗装されている。大域貼り合わせ、conormal descent、torsor 構造、Atlas、Period Separation、一元生成の完全性系列。ここまでの定理は、一つ残らず Lean 4 の機械検証を通っている。道の下には、理論の正本で固定された土台がある。Atom を生成元とする構文、law = 方程式系、係数の生成契約、表示関手。
顔を上げると、まだ誰の足跡もない斜面が広がっている。意味のモジュライ化。山頂の Semantic Scheme Representability。破れの二次元化。解像度階層の正規形。full abstraction 問題の再来。証明は、まだ一行もない。
登路は引いてある。最初の技術的関門は係数の base change(係数の生成を固定した数体から一般の係数代数へ広げること)。そこから意味のモジュライ化を経て、表現可能性へ登る。稜線の予想たちは、その途中で拾われる。
足場は、すべて公開されている。
- 理論と Lean 形式化のリポジトリ: https://github.com/iroha1203/AlgebraicArchitectureTheoryV2
- SAGA 論文(Zenodo): https://doi.org/10.5281/zenodo.21603761
- Atlas 定理の解説記事(反証4回の記録): https://zenn.dev/iroha1203/articles/496cff14471f5a
まとめ
下山する。理論が会議室に持ち帰るものは、二相構造だ。設計時に、方程式系を選ぶ。観測時に、残差を測る。 可換図式に合意することは、方程式系の選択である。実装後は、選んだ方程式系に対する残差を観測から計算し、合意が実装で成立しているかを測る。この測定は機械化されている(AAT のツール群が実装している)。設計時の合意が、そのまま観測時の測定基準になる。
冒頭の会議室で起きたことは、この意味論の第一相の手動実行だった。図式を書いた瞬間に議論が収束したのは、偶然でも修辞の勝利でもない。あの図式は、意味論の部品だった。 理論はそれを、手動でなく、測定装置として実行する。
方法論には先例がある。Grothendieck は難問を正面から割らなかった。一般性の海の水位を上げ、問題が自然に沈んで解けるのを待った。上昇する海と呼ばれる流儀だ。このプログラムも同じことをしている。個々のバグを叩くのではなく、意味の数学の水位を上げる。水位が十分に上がれば、1 セントのドリフトも、会議室の紛糾も、同じ一つの幾何の水面下に沈む。
意味は空間を持つ。その空間の測量が、始まったところだ。