前回はこちら
はじめに
こんにちは！
結合テストが全部通ったのにリリースしたら壊れた——そんな経験はありませんか？
第5部の出発点はこの一つの定理です。
/-- qComp を保存する写像はあるが、ReflectionHom は存在しない反例。 -/
theorem qComp_preserving_without_reflectionHom :
Nonempty (QCompMap Xnot Xid) ∧
¬ Nonempty (SystemOps.ReflectionHom Xnot Xid)
ワークフロー全体の結果が一致していても、個々のAPIの振る舞いが保存されているとは限らない。 結合テストが通ったのに壊れる——その現象の代数的な正体がここにあります。
第1部の発見は「ACIDは四つの独立軸で選択できる」、第2部は「ES ≤ Saga ≤ CRUDという格子がある」、第3部は「CRUDのカスケード故障とSagaの補償故障は同構造」、第4部は「SOLIDだけでは分解可能性が保証されない」でした。第5部の発見は——「結合テストが通ってもバグは残る」。
1. 結合テストが通ってもバグは残る
このセクションのポイント： not/id反例により、「ワークフロー全体の結果が偶然一致する」と「各APIの振る舞いが保存されている」は異なる条件であることを示す。結合テストが通っても安全とは言えない——その代数的な根拠。
最小の反例
Bool上で P = (p = isTrue) とする観測族を考えます。Bool の true/false を完全に区別する観測なので、全ての操作が自動的にP-両立になります。型1バグ（不変量を壊す操作の混入）は存在しません。
この設定で、以下の二つのシステムを比べます。
Xnot = [notOp] -- 「フラグ反転」だけを持つシステム
Xid = [idOp] -- 「何もしない」だけを持つシステム
not ↦ id という写像を作ります。ワークフロー合成の結果を確認しましょう。
comp(not, not) = 二重否定 = 恒等
comp(id, id) = 恒等
合成の結果は一致しています。 結合テスト——「操作を組み合わせたワークフロー全体の結果が同じか」——は通ります。
しかし notOp と idOp は個々のAPIとしては明らかに異なる振る舞いです。not(true) = false だが id(true) = true。
theorem not_eqv_not_id : ¬ MP.Eqv notOp idOp
ワークフロー全体が偶然動いても、個々のAPIの意味論が変わっているならそれはバグです。
qComp保存とReflectionHom
この「偶然の一致」と「本物の対応」の差を精密に捉えるために、二つの概念があります。
qComp保存（QCompMap）： 基底系の操作ペアについて、写像先の合成結果が元の合成結果と商上で一致する。ワークフロー全体の結果が一致するかを問う——「結合テスト」に相当します。
反射準同型（ReflectionHom）： 基底系の各操作に対して拡張系の中に ≈_P で同値な対応物を具体的に指定するデータ。各APIの振る舞いが個別に保存されているかを問う——「API互換性」に相当します。
structure ReflectionHom (X X' : SystemOps S Err P) where
lift : ∀ {f : MP S Err P}, f ∈ X.ops → MP S Err P
mem_lift : ∀ {f} (hf : f ∈ X.ops), lift hf ∈ X'.ops
eqv_lift : ∀ {f} (hf : f ∈ X.ops), MP.Eqv f (lift hf)
ReflectionHom が存在すれば、qComp は自動的に保存されます。
theorem qComp_preserved_by_reflectionHom
{X X' : SystemOps S Err P}
(h : ReflectionHom X X')
{f g : MP S Err P}
(hf : f ∈ X.ops) (hg : g ∈ X.ops) :
qComp (Quotient.mk _ (h.lift hf)) (Quotient.mk _ (h.lift hg)) =
Quotient.mk _ (MP.comp f g)
しかし逆は成り立ちません。 not/id反例がそれを示しています。
theorem qComp_preserving_without_reflectionHom :
Nonempty (QCompMap Xnot Xid) ∧
¬ Nonempty (SystemOps.ReflectionHom Xnot Xid)
なぜこうなるのか？
実務で考えてみましょう。ECサイトのクーポンシステムです。
v1には toggleCoupon APIがある。呼ぶたびにクーポンの有効/無効が切り替わる。管理画面のトグルボタンに紐づいていて、担当者が「有効にする」「やっぱり無効にする」を繰り返し操作できる。
v2へのアップグレードで、「トグルはUXが悪い」という判断から、toggleCoupon を getCoupon（現在の状態をそのまま返す）に差し替えた。管理画面は「クーポン確認」ボタンに変わった。
結合テストのシナリオ：「クーポンを2回操作して、元の状態に戻ることを確認する。」
- v1:
toggleCoupon → toggleCoupon= 有効→無効→有効。元に戻る。 - v2:
getCoupon → getCoupon= 有効→有効→有効。元のまま。
結合テスト → 通る。 どちらも「2回操作後に元の状態」という結果は同じ。
しかしv1の toggleCoupon を1回だけ呼ぶフロントエンドのコードがある。v1では「クーポン無効化」として動いていたそのコードが、v2では「クーポン確認」になり、無効化が効かなくなる。 個々のAPIの意味論が変わっているのに、結合テストのシナリオでは帳尻が合ってしまった。
これがnot/id反例の実務的な意味です。結合テストは合成の結果しか見ない。個々のステップの意味論が変わっていても、全体の帳尻が合えば気づかない。
では、「各APIの振る舞いが保存されている」とはどういう条件なのか？ なぜこの条件が型チェックだけでは保証されないのか？——次のセクションで、機能追加の代数を構築します。
2. 機能追加の代数——SystemOpsと構造保存拡張
このセクションのポイント： 「機能追加」を操作集合の包含として定式化し、「安全な追加」を構造保存拡張として定義する。ReflectionHom はこの枠組みの中で「セクション1の問いへの答え」として自然に位置づけられる。
ECサイトを代数で書く
ECサイトの注文システムを考えます。状態は自然数（注文数）、操作は以下の通り。
| 操作 | 意味 | Leanでの定義 |
|---|---|---|
add2Raw |
注文を2件まとめて集計 | fun n => .ok (n + 2) |
add4Raw |
4件バッチ加算 | fun n => .ok (n + 4) |
set0Raw |
注文数リセット | fun _ => .ok 0 |
add1Raw |
1件ずつ加算（バグの例に使う） | fun n => .ok (n + 1) |
観測族 P を「注文数が小さいか」（isSmall n = n ≤ 1）で定義します。P は「外部から観測できる契約」——ビジネスロジックが区別すべき性質だけを入れます。P が決まれば「同じ」の意味が決まり、「壊れた」の意味が決まります。
add2Raw（2件加算）はP-両立です。0と1はどちらも isSmall で同値ですが、add2(0) = 2 と add2(1) = 3 もどちらも isSmall が不成立なので同値です。一方、add1Raw（1件加算）はP-両立ではありません。add1(0) = 1（isSmall 成立）と add1(1) = 2（isSmall 不成立）は同値でない。1件加算は「小さいかどうか」の区別を壊す操作なのです。
SystemOps——型で不変量を守る
P-両立な操作だけを集めたのが第3部の MP。操作とP-両立性の証拠をセットで持つ構造体です。SystemOps は、この MP のリストです。
structure SystemOps (S : Type u) (Err : Type v) (P : ObsFamily S) where
ops : List (MP S Err P)
ECサイトの初期システムと拡張後システムは：
def X : SystemOps Nat String P where ops := [add2, add4] -- 初期
def X' : SystemOps Nat String P where ops := [add2, add4, set0] -- 拡張後
SystemOps に含まれる全操作はP-両立であることが型レベルで保証されています。不変量を壊す add1Raw はそもそもリストに入れられません。
拡張と構造保存
拡張は操作の包含として定義します。
def Extension (X X' : SystemOps S Err P) : Prop :=
∀ f, f ∈ X.ops → f ∈ X'.ops
しかし、操作が「含まれている」だけでは不十分です。既存操作の振る舞いが変わっていないことも要求したい。ここで ≈_P（P-観測同値）と、セクション1で導入した ReflectionHom が活きます。
/-- 構造保存拡張 = 包含 + 観測同値の保存。 -/
def StructPreservingExtension (X X' : SystemOps S Err P) : Prop :=
Extension X X' ∧ PreservesReflection X X'
Extension は API surface（エンドポイントの存在）の保存、PreservesReflection は API semantics（振る舞いの意味）の保存。 v2でエンドポイントが残っていても、レスポンスの意味が変わっていれば壊れる。両方必要です。
theorem structPreserving_X_X' : SystemOps.StructPreservingExtension X X'
セクション1の問いへの答えがここで得られます。結合テストが通るだけでは構造保存拡張とは言えない——各APIの振る舞いが ≈_P で保存されている（ReflectionHom が存在する）必要がある。 not/id反例は、この二つの条件の間のギャップを具体的に示したものでした。
3. バグの二つの型——そして型1は消える
このセクションのポイント： バグは正確に二種類。型1（不変量を壊す操作の混入）は型システムで排除できる。残るのは型2（既存APIの振る舞いが変わる）だけ——そしてそれがセクション1で見た現象の正体。
型1バグ——不変量の破壊
型1バグ（Invariant-breaking injection）： P-両立でない操作の混入。
def RawSystemOps.BugType1 (X : RawSystemOps S Err) : Prop :=
∃ f, f ∈ X.ops ∧ ¬ Respecting P f
実務では：
- 「残高は0以上」という不変量があるのに、残高チェックなしの引き出し関数を追加した
- 「ユーザーIDは一意」という制約のあるDBに、一意性チェックなしのINSERTを追加した
- 偶数単位でしか処理しないシステムに、奇数単位の加算関数を追加した（ECサイト例の
add1Raw）
共通する構造は「新しい操作が、既存のシステムが前提としている対称性（不変量）を破壊する」ことです。
型2バグ——後方互換の破壊
型2バグ（Backward-compatibility break）： 全操作はP-両立だが、既存操作の観測同値が崩壊。
def SystemOps.BugType2 (X X' : SystemOps S Err P) : Prop :=
¬ PreservesReflection X X'
セクション1のnot/id反例はまさにこれです。notOp も idOp もP-両立だが、idOp の振る舞いの同値類が拡張後に消失した。型1より見つけにくく、実務で最もストレスフルなバグです。
型2バグは ReflectionHom の不在として精密に特徴づけられます。
/-- 型2バグ ↔ 反射準同型の不在。 -/
theorem bugType2_iff_homBreak (X X' : SystemOps S Err P) :
BugType2 X X' ↔ BugType2HomBreak X X'
型1バグが消える
SystemOps は MP のリストです。MP の要素は定義上 Respecting P の証拠を保持しています。ということは、SystemOps に含まれる操作は全て自動的にP-両立です。
theorem respecting_of_mem_forget
(X : SystemOps S Err P)
(hf : f ∈ (RawSystemOps.forget X).ops) :
Respecting P f
型1バグは SystemOps の世界では型エラーとして排除されます。コンパイルが通った時点で、型1バグは存在しません。
反射操作（P-両立な操作だけを取り出す操作）を定義すると、MP の世界ではそれは恒等写像になります。
def reflectivePart (X : SystemOps S Err P) : SystemOps S Err P := X
theorem reflectivePart_idempotent (X : SystemOps S Err P) :
reflectivePart (reflectivePart X) = reflectivePart X := rfl
rfl で証明が閉じる。型が全ての仕事を終えているからです。
ただし現実のシステムは MP の世界に閉じていません。 外部API、生SQL、動的コードなど、型の保証が効かない操作が混入しうる。RawSystemOps はその世界を表現しており、そこでは型1バグが構成可能です。
整理すると：
安全な拡張 = StructPreservingExtension（操作が消えない ∧ 振る舞いが変わらない）
壊れる拡張 = 型1バグ ∨ 型2バグ
型1（不変量破壊）: 不変量を壊す操作の混入 → 型システムで排除可能
型2（後方互換破壊）: 既存APIの振る舞いの変化 → ReflectionHom の不在として検出
型1は型システムが消す。残るのは型2だけ。 そしてセクション1で見た通り、型2は結合テストをすり抜ける。
4. 構造保存拡張は合成で閉じる——バージョン履歴は圏をなす
このセクションのポイント： 各スプリントの機能追加がそれぞれ安全なら、半年分の全体変更も安全。ReflectionHom は合成可能で、バージョン履歴が圏をなす。リファクタリングは双方向のReflectionHomとして自然に定式化できる。
合成閉性
v1 → v2 が構造保存拡張で、v2 → v3 も構造保存拡張なら、v1 → v3 も構造保存拡張。
theorem structPreserving_compose
(hXY : StructPreservingExtension X Y)
(hYZ : StructPreservingExtension Y Z) :
StructPreservingExtension X Z
証明の核は MP.eqv_trans。≈_P の推移性がそのまま拡張の合成閉性を与えます。半年分のスプリントを経たシステムの後方互換性を、各スプリントの差分レビューの積み重ねで保証できるということです。
バージョン履歴は圏をなす
ReflectionHom もデータとして合成が可能です。
def ReflectionHom.comp
(hXY : ReflectionHom X Y) (hYZ : ReflectionHom Y Z) :
ReflectionHom X Z
恒等射（ReflectionHom.id）、左単位律、右単位律、結合律が全て証明され、ReflectionHom は圏の射として機能します。
これは「システムのバージョン履歴」が圏をなすことを意味します。対象がバージョン（操作集合）、射が「各APIの対応表」（ReflectionHom）です。Gitのコミット履歴を思い浮かべてください。各コミットが構造保存拡張なら、任意の二つのコミット間に ReflectionHom が構成でき、その合成は結合的です。
逆に、ある一つのコミットが構造保存でなかった場合（型2バグの導入）、そのコミットを含む全ての合成パスが汚染されます。「どのコミットでバグが入ったか」は、ReflectionHom の構成が失敗する最初のコミットとして特定できます——git bisect の代数的な解釈です。
リファクタリング = 双方向のReflectionHom
Martin Fowlerの定義を借りれば、リファクタリングとは「外部から見た振る舞いを変えずに内部構造を変えること」。これはそのまま本稿の枠組みに翻訳できます。
リファクタリング = ReflectionHom が X → X' と X' → X の両方向に存在する拡張。
新しい定義は不要——ReflectionHom の対が、リファクタリングの形式的な定義をそのまま与えます。いくつかの帰結が直ちに得られます。
-
リファクタリングの安全性は合成で閉じる。
ReflectionHom.compがそのまま使えます。 - リファクタリングは可逆、機能追加は不可逆。 この非対称性が「リファクタリングは安全だが機能追加には注意が必要」という直感の正体です。
- 型2バグはリファクタリングの失敗。 X → X' 方向の ReflectionHom は構成できるが X' → X 方向が構成できない——外から見た振る舞いが変わった、ということです。
5. 操作の正しさとアーキテクチャの正しさは独立である
このセクションのポイント： 「APIの振る舞いが変わる」と「依存構造に循環が入る」は独立に起きる。単体テストが通っても結合テストで壊れうるし、依存構造が健全でもAPIの意味論が変わりうる。
ECサイトの3シナリオ
ECサイトの例で、操作の正しさとアーキテクチャの正しさの独立性を見ましょう。コンポーネントは order（注文）、inventory（在庫）、shipping（配送）の3つです。
sysX = { ops: [add2, add4], graph: Ggood }
操作正常 ✓ 非巡回 ✓（order → inventory → shipping）
sysX' = { ops: [add2, add4, set0], graph: Ggood }
構造保存拡張 ✓ 非巡回 ✓
sysX''= { ops: [add2, add4, set0], graph: Gbad }
操作は同じ ✓ 循環あり ✗（shipping → order の辺が追加）
操作は同じなのに、依存グラフの選び方次第でアーキテクチャが壊れる。 sysX' と sysX'' の操作集合は同一ですが、依存グラフが異なります。
theorem Ggood_decomposable : Decomposable Ggood
theorem Gbad_not_decomposable : ¬ Decomposable Gbad
同時崩壊の例
同一の拡張で、操作レベルの型2バグとアーキテクチャレベルの崩壊が同時に起きる例も構成できます。
theorem simultaneous_op_and_arch_bug :
SystemOps.BugType2 base.ops bad.ops ∧
¬ Decomposable bad.graph
しかし因果関係はない
直感的には「APIの意味論が変われば、依存構造も壊れそう」あるいは「依存構造が壊れれば、APIの振る舞いも変わりそう」と思えます。どちらも偽です。
- 操作側崩壊のみ（構造側は健全）： APIのレスポンスが変わったが、マイクロサービスの依存関係図は変わっていない。各APIの単体テストは通るのに、振る舞いの意味論が変化している。
- 構造側崩壊のみ（操作側は健全）： 各APIの単体テストは全て通るが、サービス間の依存が循環してしまい結合テストが壊れた。
二つの障害モードは完全に独立しています。この独立性はモデルの欠陥ではなく、ソフトウェアの現実を反映しています。「このAPIはどのコンポーネントに属するか」「この操作の追加がどのコンポーネント間に依存を生むか」は、コードの意味論からは導出できない情報であり、人間が設計判断として与える必要があるからです。
第4部で「SOLIDだけでは分解可能性が保証されない」ことを証明しましたが、それは静的な結果でした。第5部のこの独立性は、その動的な対応物です。操作レベルの正しさからアーキテクチャレベルの正しさは導出できない——第4部はこれを静的に、第5部は動的に示しました。
6. ソフトウェアの正しさは三層構造を持つ
このセクションのポイント： ソフトウェアの正しさは「操作の正しさ」「合成の正しさ」「アーキテクチャの正しさ」の三層からなり、各層は独立。単体テスト＋結合テストでも層2はカバーできない——層2に届くのはAPI互換テスト（contract testing）だけであり、層3にはテスト自体が届かない。
三層モデル
以上を統合すると、ソフトウェアの正しさに関する三層モデルが浮かび上がります。
層3：アーキテクチャの正しさ（Decomposable）
↑ GraphAssignment（人間が与える設計判断）
層2：合成の正しさ（≈_P の保存、ReflectionHom）
↑ MP.comp の閉性（自動的に保証）
層1：操作の正しさ（Respecting）
↑ 型システム（コンパイル時に検査）
入力：生の操作（TxnK）
各層は独立した保証メカニズムを持ちます。
-
層1→層2の伝播は部分的に自動。 コンパイルが通れば、個々の関数の合成の型整合性（
MP.compの閉性）は保証される。ただし層2の本体——既存APIの振る舞いが拡張後も保存されているか（ReflectionHom）——は型だけでは保証されず、別途検証が必要。 - 層2→層3の伝播は手動。 人間が設計判断として構成する必要がある。
日常のテスト手法を各層に対応させると、驚くべき隙間が見えます。
単体テスト → 層1の有界近似（個々の操作がRespectingか）
結合テスト → qComp保存 ← 層2より厳密に弱い（not/id反例）
API互換テスト → 層2の有界近似（ReflectionHom）
設計レビュー → 層3の非形式的検査
単体テストと結合テストを組み合わせても層2はカバーできません。 単体テストは個々の操作の不変量保存（層1）を検査し、結合テストはワークフロー全体の合成結果の一致（qComp保存）を検査する。しかしセクション1のnot/id反例が示した通り、qComp保存はReflectionHomより厳密に弱い条件です。合成結果が偶然一致しても、個々のAPIの意味論が変わっていれば型2バグは残る。
層2に届くのはAPI互換テスト（contract testing）——v1の各APIに対してv2の対応APIを特定し、同じ入力に対して観測的に同等な出力を返すかを個別に検証するテストです。これはReflectionHomの有界近似に相当します。
テストは有界近似である
この「有界近似」は定理として形式化されています。
theorem finite_not_imply_global :
InvariantPreservingOn sampleStates invLe10 weird ∧
¬ InvariantPreserving invLe10 weird
weird（3以上なら100を返す）は [0, 1, 2] 上では invLe10（10以下）を保存するが、3を入れると100を返して壊れます。テストが通ったのに本番で壊れる——まさにこの構造です。
ただし、サンプルが十分に被覆していれば、その範囲では形式検証と同等です。
theorem finite_with_coverage_implies_bounded
(hOn : InvariantPreservingOn states I f)
(hCover : ∀ s, s < n → s ∈ states) :
∀ s, s < n → I s → I (f s)
テストと形式検証は二項対立ではなく、被覆範囲をパラメータとする連続的なスペクトル上にあります。
第4部の3層分類との接続
第4部では設計パターンを射影整合（DIP/ISP/SRP）、置換整合（LSP）、分解可能性（レイヤードアーキテクチャ）の3層に分類しました。第5部の3層はこれに対応しています。
| 第4部の分類 | 第5部の対応 | 性質 |
|---|---|---|
| 射影整合 | 層1（操作の正しさ） | 型システムで自動検査 |
| 置換整合 | 層2（合成の正しさ） | 代数的構造で保証 |
| 分解可能性 | 層3（アーキテクチャの正しさ） | 設計判断として人間が構成 |
第4部は静的な性質を分類しました。第5部は動的な側面——「拡張がこれらの性質をどう保存するか、どう破壊するか」——を形式化しました。
機能追加のとき何をすべきか
三層モデルから、機能追加時のチェックリストが導かれます。
層1：新しい操作はP-両立か？ 型安全な言語ならコンパイラが教えてくれる。そうでなければ不変量テストを書く。
層2：既存APIの対応表（ReflectionHom）は構成できるか？ v1の各APIについて個別に、v2の対応APIと同じ入力に対して観測的に同等な出力を返すかを検証するAPI互換テスト（contract testing）がこれに相当する。単体テスト（層1）と結合テスト（qComp保存）を組み合わせても層2には届かない——セクション1のnot/id反例がその根拠。
層3：依存グラフに循環が入っていないか？ これは自動化できない。設計レビューやアーキテクチャ分析ツールで確認する。
三つの層は独立なので、どれか一つを省略すると、他の二つが健全でも壊れうる。
7. コード全体
本稿のLean 4コードは以下のファイルで構成されています。
| ファイル | 内容 |
|---|---|
Core.lean |
Endo上の基盤定義（RespectingP, Idempotent, CommutativePair, InvariantPreserving） |
OpsExtension.lean |
SystemOps, RawSystemOps, Extension, StructPreservingExtension, BugType1/2 |
QuotientOps.lean |
MPIdempotent, MPCommutativePair, qComp, 商への持ち上げ定理 |
Homomorphism.lean |
ReflectionHom, ReflectionHom.comp/id, ReflectionCategory, BugType2HomBreak |
Bridge.lean |
OpsCategory, GraphCategory, GraphAssignment, graphFunctor, ReflectionGraphAssignment, reflectionGraphFunctor |
Samples/BugFix.lean |
バグ修正の具体例（buggy→fixed） |
Samples/Idempotence.lean |
setTrue（冪等）vs toggle（非冪等） |
Samples/Commutativity.lean |
add1+add2（可換）vs add1+double（非可換） |
Samples/Testing.lean |
有限検査と全検査のギャップ、被覆条件 |
Samples/ECommerce.lean |
EC統合例（3シナリオ）、Ggood/Gbad |
Samples/Type2Bug.lean |
型2バグ具体例、qComp反例、同時崩壊例 |
Comparisons.lean |
全対比定理の束ね（6行） |
機械検証された主要な定理をまとめます。
| 定理 | 内容 |
|---|---|
qComp_preserving_without_reflectionHom |
qComp保存 ⇏ ReflectionHom（結合テストの限界） |
bugType2_iff_homBreak |
型2バグ ↔ 反射準同型の不在 |
qComp_preserved_by_reflectionHom |
反射準同型は商上の合成を保存 |
structPreserving_compose |
構造保存拡張の合成は構造保存 |
not_structPreserving_iff_bug |
構造保存の否定 ↔ 型1 ∨ 型2（Raw版） |
respecting_of_mem_forget |
SystemOpsの忘却像は全てRespecting |
reflectivePart_idempotent |
反射操作の冪等性（rflで閉じる） |
simultaneous_op_and_arch_bug |
操作側とアーキテクチャ側の型2バグが同時発生 |
bugType2_X_X' |
型2バグの具体構成（Bool上） |
qIdempotent_of_idempotent |
冪等性の商への持ち上げ |
qCommutative_of_commutative |
可換性の商への持ち上げ |
retrySafe_of_idempotent |
冪等ならリトライ安全 |
finite_not_imply_global |
有限検査は全検査を含意しない |
finite_with_coverage_implies_bounded |
被覆条件つき有限検査 = 有界形式検証 |
decomposable_preserved_by_graph_structure |
グラフ像不変 → Decomposable保存 |
structPreserving_X_X' |
EC例の構造保存拡張 |
bugType1_XbadRaw |
EC例の型1バグ |
Ggood_decomposable / Gbad_not_decomposable
|
非巡回→分解可能、循環→分解不能 |
GitHubリポジトリ公開準備中！
8. おわりに
第5部では、「機能追加」を操作集合の拡張として定式化し、バグを構造からの逸脱として代数的に分類しました。
最大の発見は「結合テストが通ってもバグは残る」です。
not/id反例は、「ワークフロー全体の結果が偶然一致する」（qComp保存）と「各APIの振る舞いが保存されている」（ReflectionHom）が異なる条件であることを示しました。前者は結合テスト、後者はAPI互換性テストに対応します。バグの正しい定義は後者であり、前者では検出できないバグが存在します。
この発見を軸に、三つの帰結が得られました。
第一に、型1バグは型システムで消える。 MP で操作を型付けすると、P-両立でない操作はコンパイル時に排除されます。残るのは型2バグだけ。
第二に、構造保存拡張は合成で閉じ、バージョン履歴は圏をなす。 各スプリントの差分が安全なら全体が安全。リファクタリングは双方向のReflectionHomとして自然に定式化されます。
第三に、操作の正しさとアーキテクチャの正しさは独立である。 単体テストが全部通っても循環依存は検出できず、依存構造が健全でもAPIの意味論の変化は防げない。
第4部の結論は「SOLIDだけでは分解可能性が保証されない」でした。第5部の結論はその動的版です。「テストだけでは、次のリリースが安全とは言えない。」
しかも「テスト」の内訳が重要です。単体テスト＋結合テストでは層2に届きません。結合テストはワークフロー全体の合成結果（qComp保存）しか検査せず、個々のAPIの意味論の変化（ReflectionHomの不在）を見逃します。層2に届くのはAPI互換テスト（contract testing）——各APIを個別に検証するテストだけです。そして層3（アーキテクチャ）にはテスト自体が届かない。ソフトウェアの正しさは三層構造を持ち、各層は独立で補完的です。
全ての主張は「たぶんそうだよね」ではなく「型が通りました」として提示されています。
次回予告
第6部以降では、第1部〜第5部の統合と、より大きな問いへ向かいます。
第1部のACID性質、第2部の格子構造、第3部の移送定理、第4部の3層分類、第5部の拡張理論——これらは同じ代数的世界の異なる断面です。統合すれば「ソフトウェアアーキテクチャの代数的理論」の輪郭が見えてくるはずです。
お楽しみに！