前回はこちら

はじめに

こんにちは！

ソフトウェア設計には無数のパターンがあります。SOLID原則、レイヤードアーキテクチャ、契約継承、インターフェース分離……。それぞれ「良い設計」のための指針として広く受け入れられています。

でも、こう思ったことはないですか？

これらのパターンは、結局のところ何を保証しているのだろう？

「疎結合にしましょう」「依存を逆転させましょう」「単一責任にしましょう」——どれも正しそうに聞こえる。でも、あるパターンを適用したとき、システムのどの性質が保証され、どの性質はまだ保証されていないのか。そこが曖昧なまま「良い作法」として一括りにされています。

第4部では、設計パターンを圏論で定式化し、各パターンが何を保証するかで3層に分類します。結果として、SOLID原則とレイヤードアーキテクチャの関係が数学的に明確になります。全てLean 4で機械検証済みです。

第1〜3部では、ACID・CRUD・Saga・Event Sourcingという具体的なパターンを代数で分析しました。第4部からは問いの抽象度が上がります。「設計パターンとは何か」「各パターンは何を保証するのか」——これらは特定のパターンについての問いではなく、パターン一般についての問いです。

個別のモノイドや依存グラフでは表現しきれません。対象と射の関係、関手による構造の保存、商による同一視——圏論の語彙が必要になります。

この記事で扱うこと

依存グラフから圏を構成し、分解可能性を圏論的に定義する
射影関手と商のwell-defined性でDIPを圏論的に定式化する
実装継承が商を壊すことを証明し、LSP違反との接続を示す
SOLID 5原則に圏論的定式化を与え、成立例と違反例を全て機械検証する
SOLID 5原則が分解可能性を含意しないことを反例で証明する

1. なぜ分解したいのか——そしてなぜ自明でないか

ある日の出来事

認証モジュールのトークン検証ロジックを修正したら、決済処理のテストが落ちた。決済コードは一切触っていないのに。調べてみると、決済モジュールが認証モジュールの内部ヘルパーを直接importしており、そのヘルパーがトークン検証と共有している内部状態に依存していた。

こういう経験、ありませんか？

これが「分解不能なシステム」の日常です。あるコンポーネントの変更が、一見無関係なコンポーネントを壊す。影響範囲が予測できない。レビューで「この変更、他に影響ないですか？」と聞かれても、自信を持って「ない」と言えない。

一方、分解可能なシステムでは変更の影響が層内に閉じます。認証層を変更しても、決済層のテストは落ちない。なぜなら、決済層は認証層の抽象（インターフェース）にだけ依存しており、内部実装への依存が存在しないからです。

分解可能性が保証する三つのこと

この「体験の違い」は、分解可能性という代数的性質で精密に特徴づけられます。

故障の局在化。 分解可能なシステムでは、故障が発生した層を特定し、その層だけを調査すれば原因に到達できます。本稿のFreeBase（分解可能）では故障局在性 localizable が証明され、StrongBase（分解不能）では not_localizable が証明されます。第2部で証明した「関係式が増えるほど故障モードが増える」格子構造の直接的な帰結です。

修復範囲の限定。 分解可能なら壊れた層だけを直せます。分解不能なら、循環依存に巻き込まれた全コンポーネントに手を入れる必要がある。本稿の repair_operation_effect は、循環辺1本の切断で分解不能→分解可能に回復し、同時に依存の総本数が4→3に減少することを示します。

第1部の反単調性定理の実現。 第1部で「公理が少ないほど壊れにくい」（robust_of_weaker）を証明しました。分解可能なアーキテクチャは不要な依存を持たないため関係式数が小さく、この定理の恩恵を最大限に受けます。分解可能性とは、反単調性定理を具体的なアーキテクチャ設計に降ろしたものなのです。

しかし分解は保証されない

有限群の理論には、Jordan-Hölderの定理という美しい結果があります。どんな有限群でも、それ以上分解できない単純群の列（組成列）に分解でき、その分解は順序の違いを除いて一意です。

ソフトウェアにはこの保証がありません。

コンポーネントA → B → C → Aという巡回依存があると、どの切り口で分けても切り残しが出る。レイヤーに分けようにも、全員が同じ層にいるしかない。これは「分解不能」であり、スパゲッティコードの代数的な診断です。

第4部の出発点はここです。分解可能性は公理ではなく、証明すべき性質である。 ではその証明には何が必要なのか——圏論の道具を使って調べていきます。

2. 圏論基盤——最小限の道具立て

なぜ圏論か

第3部までの道具（状態空間上のモノイド、Kleisli射、依存グラフ）で十分だったのは、具体的なパターンを分析していたからです。しかし「設計パターン一般」について語るには、対象と射の関係を抽象的に扱う言語が必要です。

圏論は以下を統一的に表現します。

コンポーネント間の依存関係 → 圏の射
実装から抽象への写像 → 関手
同じ抽象に対応する実装の同一視 → 商圏
分解の可能性 → 層化（フィルトレーション）の存在

Mathlibに依存すると学習・ビルドコストが高いので、必要最小限の定義を自前で構成しました。

SmallCategory

structure SmallCategory where
  Obj : Type u
  Hom : Obj → Obj → Sort v
  id : {X : Obj} → Hom X X
  comp : {X Y Z : Obj} → Hom X Y → Hom Y Z → Hom X Z
  id_comp : ∀ {X Y : Obj} (f : Hom X Y), comp id f = f
  comp_id : ∀ {X Y : Obj} (f : Hom X Y), comp f id = f
  assoc : ∀ {W X Y Z : Obj} (f : Hom W X) (g : Hom X Y) (h : Hom Y Z),
    comp (comp f g) h = comp f (comp g h)

対象の集合、対象間の射、恒等射、合成、そして三つの法則（左単位律、右単位律、結合律）。圏の教科書的な定義そのものです。

Functor

structure Functor (C : SmallCategory) (D : SmallCategory) where
  objMap : C.Obj → D.Obj
  homMap : {X Y : C.Obj} → C.Hom X Y → D.Hom (objMap X) (objMap Y)
  map_id : ∀ {X : C.Obj}, homMap (C.id (X := X)) = D.id
  map_comp : ∀ {X Y Z : C.Obj} (f : C.Hom X Y) (g : C.Hom Y Z),
    homMap (C.comp f g) = D.comp (homMap f) (homMap g)

対象を対象に、射を射に写し、恒等射と合成を保存する。構造を壊さない写像です。

`FullSubcategory` と `ReflectiveSubcategory`

structure FullSubcategory (C : SmallCategory) where
  pred : C.Obj → Prop

structure ReflectiveSubcategory (C : SmallCategory) where
  sub : FullSubcategory C
  reflector : Functor C (sub.toCategory)
  inclusion : Functor (sub.toCategory) C := FullSubcategory.inclusion sub

充満部分圏は対象を述語で選択し、射は全て引き継ぐ。反射的部分圏は「部分圏に射影する関手」を持つ。ReflectiveSubcategoryは第5部の拡張理論への接続点として、第4部で器だけ用意しておきます。

依存グラフから圏へ——`ComponentCategory`

ここが第3部までの世界と第4部を接続する鍵です。

inductive Reachable {C : Type u} (G : ArchGraph C) : C → C → Prop where
  | refl (c : C) : Reachable G c c
  | step {c d e : C} : d ∈ G.deps c → Reachable G d e → Reachable G c e

def ComponentCategory {C : Type u} (G : ArchGraph C) : SmallCategory where
  Obj := C
  Hom := Reachable G
  id := Reachable.refl _
  comp := fun f g => Reachable.trans f g
  id_comp := by intro X Y f; apply Subsingleton.elim
  comp_id := by intro X Y f; apply Subsingleton.elim
  assoc := by intro W X Y Z f g h; apply Subsingleton.elim

依存グラフの各コンポーネントを対象、到達可能性を射とする薄い圏（thin category）を生成します。薄い圏とは、任意の2対象間に射が高々1本しか存在しない圏のことで、前順序（preorder）と同じ構造です。Hom X Y が Prop（命題）として定義されているため、射の等号は証明の一意性で自動的に成立し、圏の公理（結合律・単位律）は Subsingleton.elim 一発で片付きます。

3. 分解可能性——Layered vs Spaghetti

Webアプリケーションの典型的な構成を思い浮かべてください。

Controller → Service → Repository → Database

上位が下位に依存し、逆方向の依存はない。Controllerを変更してもDatabaseは影響を受けない。Repositoryにバグがあっても、Controllerのテストは単体で回せる。これが「分解可能」な構造です。

一方、こういうコードベースもあります。

UserService → OrderService → NotificationService → UserService

ユーザーが注文に依存し、注文が通知に依存し、通知がユーザーに依存する。どこから手をつけても循環に巻き込まれる。テストを書こうにも全部モックしないと動かない。これが「分解不能」な構造です。

定義

圏論的な分解可能性は「層化が存在すること」です。

def Filtration (C : SmallCategory) : Type u := C.Obj → Nat
def LayerMonotone (C : SmallCategory) (L : Filtration C) : Prop :=
  ∀ {X Y : C.Obj}, C.Hom X Y → L Y ≤ L X
def Category.Decomposable (C : SmallCategory) : Prop :=
  ∃ L : Filtration C, LayerMonotone C L

依存グラフ版は生成辺での厳密単調性です。

def StrictLayered (G : ArchGraph C) (L : Layering C) : Prop :=
  ∀ c d, d ∈ G.deps c → L d < L c
def Decomposable (G : ArchGraph C) : Prop :=
  ∃ L : Layering C, StrictLayered G L

そして橋渡し定理。グラフ版の分解可能性から圏論版の分解可能性が従います。

theorem categoricalDecomposable_of_decomposable {G : ArchGraph C}
    (h : Decomposable G) : Category.Decomposable (ComponentCategory G)

生成辺での厳密単調性が、到達可能性射の（非厳密）単調性を帰納法で誘導します。

正例：Layered

inductive Comp where | api | app | domain | infra
def G : ArchGraph Comp where
  deps := fun
    | .api => [.app] | .app => [.domain] | .domain => [.infra] | .infra => []
def L : Layering Comp
  | .infra => 0 | .domain => 1 | .app => 2 | .api => 3

api → app → domain → infra の4層構造。依存は必ず下位層に向かう。StrictLayered G L が成立し、Decomposable G が証明されます。

反例：Spaghetti

inductive Comp where | a | b | c
def G : ArchGraph Comp where
  deps := fun | .a => [.b] | .b => [.c] | .c => [.a]

a → b → c → a の3点循環。いかなる層割当 L に対しても L(b) < L(a)、L(c) < L(b)、L(a) < L(c) が要求され、L(a) < L(a) という矛盾に至ります。

theorem not_decomposable : ¬ Decomposable G

循環が分解を殺す。 これが「スパゲッティコードはなぜ壊れやすいか」の代数的回答です。

4. 商と射影——FreeBase vs StrongBase

こんなコードを見たことはないでしょうか。

// PaymentServiceとShippingServiceは両方とも IOrderRepository に依存
interface IOrderRepository { findById(id: string): Order }

class PaymentService { constructor(private repo: IOrderRepository) {} }
class ShippingService { constructor(private repo: IOrderRepository) {} }

PaymentServiceとShippingServiceは同じインターフェース IOrderRepository を通じて注文データにアクセスする。実装が PostgresOrderRepo でも MongoOrderRepo でも、上位のサービスは気にしない。これが「射影が整合している」状態——DIPが効いている状態です。

では、もし PaymentService が PostgresOrderRepo の内部メソッド runRawSQL() を直接呼んでいたら？ MongoOrderRepo に差し替えた瞬間に壊れます。同じインターフェースに見えるのに、振る舞いが違う——これが「商がwell-definedでない」状態です。

DIPの圏論的意味

依存性逆転原則（DIP）は「高水準モジュールは低水準モジュールに直接依存すべきでなく、抽象に依存すべき」と言います。圏論的に言い換えると：同じ抽象に見える実装は、抽象世界で同じ振る舞い（依存）を誘導する——これが「商がwell-defined」の直感的な意味です。

定式化します。

structure InterfaceProjection (C : Type u) (A : Type v) where
  expose : C → A

def QuotientWellDefined (G : ArchGraph C) (π : InterfaceProjection C A) : Prop :=
  ∀ c₁ c₂, π.expose c₁ = π.expose c₂ → projectedDeps G π c₁ = projectedDeps G π c₂

def DIPCompatible (G : ArchGraph C) (π : InterfaceProjection C A)
    (GA : AbstractGraph A) : Prop :=
  RespectsProjection G π GA ∧ QuotientWellDefined G π

InterfaceProjectionは実装コンポーネントを抽象に写す対象写像。RespectsProjectionがあれば、実装圏から抽象圏への関手が構成できます。

def projectionFunctor (G : ArchGraph C) (π : InterfaceProjection C A)
    (GA : AbstractGraph A) (h : RespectsProjection G π GA) :
    Functor (ComponentCategory G) (AbstractCategory GA)

DIPとは「射影関手が存在し、かつ商がwell-definedであること」。 同じ抽象に写る実装コンポーネントが、同じ抽象依存を誘導する——実装の詳細が抽象の世界に漏れ出さないという条件です。

正例：FreeBase

inductive Comp where | logStore | readModel | projector
def G : ArchGraph Comp where
  deps := fun
    | .logStore => [] | .readModel => [.logStore] | .projector => [.logStore]

logStoreは依存を持たない自由基盤。3ポート射影（core, query, projection）でDIP整合。

反例：StrongBase

inductive Comp where | storage | validator | writer
def G : ArchGraph Comp where
  deps := fun
    | .storage => [.validator] | .validator => [.storage] | .writer => [.storage]

storageとvalidatorが相互依存（循環）。1ポート射影（core）に潰すと、storageとwriterが同一抽象coreに写るが、射影依存の長さが 1 ≠ 2 で商がwell-definedでない。

theorem not_dip_compatible : ¬ DIPCompatible G π GA

修復操作

StrongBaseの循環辺（storage → validator）を1本切るだけで分解不能→分解可能に回復します。同時にrelationCountが4→3に減少。第2部の格子構造——関係式が多いほど故障モードが増える——との接続です。

theorem repair_restores_decomposable :
    ¬ Decomposable G ∧ Decomposable repairedG
theorem repair_reduces_relationCount :
    relationCount comps repairedG < relationCount comps G

5. 継承の病理——実装継承が商を壊す

Javaで書かれた古いコードベースでよく見る光景です。

class BaseRepository {
    private ConnectionPool pool;  // DB接続プールに依存
    private CacheManager cache;   // キャッシュに依存
    
    protected ResultSet query(String sql) { /* pool + cache を使う */ }
}

class UserRepository extends BaseRepository {
    // query() を使うだけのつもりが、pool と cache にも暗黙的に依存している
    public User findById(String id) { return map(query("SELECT ...")); }
}

UserRepository は BaseRepository の query() だけを使いたかった。しかし extends した瞬間に、ConnectionPool と CacheManager への依存が丸ごと伝播する。BaseRepository が CacheManager のバージョンを上げたら、UserRepository も巻き添えで壊れる。

もし代わりにインターフェースを切っていたら：

interface QueryExecutor { ResultSet query(String sql); }

class UserRepository {
    UserRepository(QueryExecutor executor) { /* executor だけに依存 */ }
}

依存は QueryExecutor の契約だけ。内部実装が何であれ、契約を守っている限り UserRepository は壊れない。

これが実装継承と契約継承の違いです。形式的に定義します。

二つの継承モデル

def implementationInheritance [DecidableEq C] (G : ArchGraph C)
    (parent child : C) : ArchGraph C where
  deps := fun c =>
    if c = child then parent :: (G.deps c ++ G.deps parent) else G.deps c

def interfaceInheritance [DecidableEq C] (G : ArchGraph C)
    (parent child : C) : ArchGraph C where
  deps := fun c =>
    if c = child then parent :: G.deps c else G.deps c

実装継承は親の依存を子に丸ごと伝播する。契約継承は子が親への依存だけを追加する。

3段階の証明チェーン

継承導入前（G0）： baseServiceとderivedServiceはともにinfraにのみ依存。両者を同一抽象serviceに射影 → 商well-defined、LSP成立、DIP整合。

実装継承後（Gimpl）： derivedServiceの依存が [baseService, infra, infra] に膨張。なぜ膨張するか——実装継承を「依存の伝播」としてモデル化しているためです。子は parent を経由して親の依存 G.deps parent を丸ごと引き継ぐので、射影後の依存列が伸びます（重複も許容）。この「依存列の伸長」が商の破壊を生みます。射影依存の長さ 1 ≠ 3 → 商が壊れる。

theorem impl_not_quotient_well_defined : ¬ QuotientWellDefined Gimpl πSub

同じ反例がLSP違反でもあります。

theorem impl_lsp_violation :
    LSPViolationAt Gimpl πSub .baseService .derivedService

LSP違反 → 商破壊の一般定理

theorem not_quotient_of_lspViolationAt
    (h : LSPViolationAt G π base sub) : ¬ QuotientWellDefined G π

LSP違反が1点でもあれば商はwell-definedでない。ObservationalEq（同じ抽象に見える）なのにObservedBehavior（射影された依存振る舞い）が異なる——これが「置換できない」の数学的な意味であり、商圏が構成できないことと同値です。

契約継承後（Giface）： derivedServiceの依存は [baseService, infra]。infra(0) → baseService(1) → derivedService(2) の層構造が成立。Decomposable、DIP整合。

theorem iface_decomposable : Decomposable Giface
theorem iface_dip_compatible : DIPCompatible Giface πIface GAIface

6. SOLID 5原則の圏論的定式化

セクション3〜5で、分解可能性・射影整合・商のwell-defined性・LSPといった概念を個別に定義し、具体例で検証してきました。ここで自然に浮かぶ疑問があります。実務で広く使われている設計原則は、この枠組みの中でどう位置づけられるのか？

SOLID 5原則はその最も有名な候補です。Robert C. Martinが整理したこの5原則は、オブジェクト指向設計の基本指針として30年以上にわたって参照されてきました。しかし、各原則が何を保証し、何を保証しないかは自然言語の議論にとどまっています。圏論的な定式化を与えることで、その守備範囲を精密に特定できます。

各原則の定義

SRP（単一責任）： 依存先は同一責任か、依存を持たない基底責任に限る。

def SRPFor (G : ArchGraph C) (resp : C → Nat) : Prop :=
  ∀ c d, d ∈ G.deps c → resp d = resp c ∨ G.deps d = []

OCP（開放閉鎖）： 既存コンポーネントの依存は不変（閉）、拡張対象には新依存が追加される（開）。

def OCPFor (base ext : ArchGraph C) (fixed targets : C → Prop) : Prop :=
  ClosedForModification base ext fixed ∧ OpenForExtension base ext targets

ISP（インターフェース分離）： 各コンポーネントの抽象依存が、そのオーナーの必要に合致する。

def ISPFor (π : InterfaceProjection C A) (GA : AbstractGraph A)
    (owner : C → Client) (needs : Client → A → Prop) : Prop :=
  ∀ c a, a ∈ GA.deps (π.expose c) → needs (owner c) a

LSP（リスコフ置換）と DIP（依存性逆転） は既存定義の別名です。

abbrev LSPFor := LiskovSubstitutableAt
abbrev DIPFor := DIPCompatible

成立例と違反例

原則	圏論的意味	成立例	違反例
SRP	依存が責任境界を跨がない	FreeBase ✓	StrongBase ✗
OCP	既存不変 ∧ 拡張対象に新依存	契約継承 ✓	baseService改変 ✗
ISP	抽象依存がクライアントの必要に合致	FreeBase ✓	StrongBase ✗
LSP	同一抽象に写る実装の観測振る舞い一致	継承前G0 ✓	実装継承Gimpl ✗
DIP	射影関手存在 ∧ 商well-defined	FreeBase ✓	StrongBase ✗

全10個の定理（各原則について成立と違反の対）が機械検証されています。

theorem solid_five_good_bad_suite :
    (SRPFor Samples.FreeBase.G freeResp ∧ ¬ SRPFor Samples.StrongBase.G strongResp) ∧
    (OCPFor Samples.Inheritance.G0 Samples.Inheritance.Giface fixedInh targetInh ∧
      ¬ OCPFor Samples.Inheritance.G0 GocpBad fixedInh targetInh) ∧
    (ISPFor Samples.FreeBase.π Samples.FreeBase.GA freeOwner freeNeeds ∧
      ¬ ISPFor Samples.StrongBase.π Samples.StrongBase.GA strongOwner strongNeeds) ∧
    (LSPFor ... ∧ LSPViolationAt ...) ∧
    (DIPFor ... ∧ ¬ DIPFor ...)

原則間の関係

5原則は完全に独立ではありません。

theorem not_dip_of_lspViolationAt
    (h : LSPViolationAt G π base sub) : ¬ DIPFor G π GA

LSP違反 → DIP不整合。 商がwell-definedでなければDIPは成立しえない。

一方、OCPとDIPの間にはこの含意関係がありません。

theorem ocp_violation_does_not_force_dip_failure :
    (¬ OCPFor Samples.Inheritance.G0 GocpBad fixedInh targetInh) ∧
      DIPFor GocpBad Samples.Inheritance.πIface GAocpBadIface

OCP違反でもDIPは成立しうる。 baseServiceの依存が変わっても（OCP違反）、射影が整合していれば関手は構成できる。

SOLID 5原則は分解可能性を含意しない

ここが第4部最大の発見です。

2点循環グラフ a → b → a を構成します。

def GsolidButCycle : ArchGraph CounterComp where
  deps := fun | .a => [.b] | .b => [.a]

このグラフはSOLID 5原則を全て満たします——ただし真空的・自明に。

SRP：同一責任割当（resp = 0）で充足
OCP：base = ext、targets = False で真空的に真
ISP：needs = True で真空的に真
LSP：base = sub で自明
DIP：1点に潰す射影で充足

しかし ¬ Decomposable。L(b) < L(a) かつ L(a) < L(b) は矛盾するからです。

-- 具体反例：GsolidButCycleはSOLID5を満たすが分解不能
theorem solid5_not_imply_decomposable_counterexample :
    SOLID5For GsolidButCycle GsolidButCycle respCounter πCounter GACounter
      ownerCounter needsCounter fixedCounter targetCounter .a .a ∧
      ¬ Decomposable GsolidButCycle

-- 一般否定：そのような反例が存在する（存在量化版）
theorem solid5_not_imply_decomposable :
    ∃ (C : Type) (G baseG : ArchGraph C) ...,
      SOLID5For G baseG resp π GA owner needs fixed targets base sub ∧
      ¬ Decomposable G

SOLIDは射影整合・契約整合・拡張規律を縛るが、依存循環を禁止しない。

追記: 非真空的な反例

先ほどの反例には真空充足が含まれていました。では、全ての原則が実際にデータを検査した上で成立する反例は作れるでしょうか？

作れます。

同じ循環グラフ a → b → a に対して、パラメータを以下のように設定します。

-- 責任: 同一の非自明な定数（全員42番チーム）
def resp_nv : NVComp → Nat := fun _ => 42

-- 射影: 両方を同一抽象αに写す
def π_nv : InterfaceProjection NVComp NVAbst where
  expose := fun _ => .alpha

-- 抽象グラフ: α → α（自己ループ。依存が実在する）
def GA_nv : AbstractGraph NVAbst where
  deps := fun | .alpha => [.alpha]

-- ニーズ: engineeringチームはαを必要とする（具体的にTrue）
def needs_nv : NVClient → NVAbst → Prop := fun
  | .engineering, .alpha => True

-- OCP: aはfixed（依存不変）、bはtargets（新依存aが追加された）
def fixed_nv : NVComp → Prop := fun | .a => True  | .b => False
def targets_nv : NVComp → Prop := fun | .a => False | .b => True

各原則の成立を確認します。

原則	成立理由	なぜ非真空か
SRP	`resp a = resp b = 42` → `resp d = resp c`	両方とも依存を持つ。量化子が `a→b`, `b→a` の2辺で実際に走る
OCP	`fixed a`: deps不変。`targets b`: 新依存aが追加	fixed, targetsとも実在するコンポーネント。拡張前→拡張後の差分が具体的
ISP	`GA.deps α = [α]`, `needs engineering α = True`	抽象依存が非空。量化子が走り、needsが具体的にTrueを返す
LSP	`π a = π b = α`（前件が真）, `projectedDeps a = [α] = projectedDeps b`	前件が偽の真空充足ではない。実際に観測的振る舞いの一致を検証
DIP	`projectedDeps a = projectedDeps b = [α]`	`π a = π b` なので商の等式が実際にチェックされ、一致する

theorem solid5_nonvacuous_not_imply_decomposable :
    SOLID5For G_nv baseG_nv resp_nv π_nv GA_nv
      owner_nv needs_nv fixed_nv targets_nv .a .b ∧
    ¬ Decomposable G_nv

5原則が全て非真空的に成立し、それでも ¬ Decomposable。

この反例が示しているのは、先ほどの真空充足が「モデルの穴」ではなかったということです。パラメータを非真空にしても結果は変わらない。SOLIDの5原則には、どうパラメータを選んでも循環を禁止する構造が入っていない。 分解可能性を保証するには、第3層——レイヤードアーキテクチャの層制約——が必要です。

分解可能性に必要な追加条件

何を足せば分解可能になるか？形式化の過程で見つかった条件がこれです：

def ResponsibilityStrictlyDecreasing (G : ArchGraph C) (resp : C → Nat) : Prop :=
  ∀ c d, d ∈ G.deps c → resp d < resp c

この定義を見てください。StrictLayeredの定義と同型です。

def StrictLayered (G : ArchGraph C) (L : Layering C) : Prop :=
  ∀ c d, d ∈ G.deps c → L d < L c

文字が違うだけで同じ命題。そしてStrictLayeredはまさにレイヤードアーキテクチャの数学的定義——依存は必ず下位層に向かう。

theorem solid5_plus_responsibilityStrict_implies_decomposable
    (_hSolid : SOLID5For G baseG resp π GA owner needs fixed targets base sub)
    (hStrict : ResponsibilityStrictlyDecreasing G resp) :
    Decomposable G

つまり：

SOLID + レイヤードアーキテクチャ → 分解可能
SOLIDだけ → 分解可能とは限らない

SOLIDはミクロの規律（コンポーネント単位の健全性）、レイヤードアーキテクチャはマクロの規律（システム全体の依存方向の制約）。両者は独立で補完的であり、どちらか一方では不十分です。

設計パターンの3層分類

ここまでの結果をまとめると、設計パターンが「何を保証するか」で3層に再分類できることが見えてきます。

層	保証するもの	対応する原則・パターン	主要定理
射影整合	射影関手の存在 + 商well-defined	DIP, ISP, SRP	`DIPCompatible`, `ISPFor`, `SRPFor`
置換整合	同一抽象に写る実装の観測一致	LSP	`LiskovSubstitutableAt`
分解可能性	循環の非存在 = 層化の存在	レイヤードアーキテクチャ	`StrictLayered`

注目すべきは第3層です。SOLIDの5原則は第1層と第2層をカバーするが、第3層を保証するパターンがSOLIDの中にない。レイヤードアーキテクチャが第3層を単独で担っています。

そして層間には依存関係があります。not_dip_of_lspViolationAt は「第2層（置換整合）が崩れると第1層（射影整合）も崩れる」ことを示しています。一方、ocp_violation_does_not_force_dip_failure はOCPが第1層と独立であることを示す。

この3層分類は、従来「良い作法」として一括りにされていた設計パターンを、何を保証し、何を保証しないかで精密に比較する枠組みを与えます。あるパターンが第1層だけを保証するのか、第2層まで保証するのか、第3層も保証するのか——それが明示されれば、パターンの選択は「好みの問題」ではなく「保証の選択」になります。

7. One more thing——OOPとFPの意外な共通項

ここまでの議論はSOLIDと分解可能性の関係に集中していました。しかし、第4部の圏論基盤はもう一つの問いにも答えを出します。

OOPとFPは本当に対立するパラダイムなのか？

ただし、ここで言う「OOP」には注意が必要です。多くのエンジニアが「OOP」と聞いてJavaやC++を思い浮かべますが、それらの言語が採用している実装継承を中心としたOOPと、Alan Kayが提唱したメッセージパッシングと契約（インターフェース）を中心としたOOPは、代数的に見るとまったく異なる構造を持ちます。以下の議論は、この区別の上に成り立っています。

答えは「対立していない」です。しかもこれは感想ではなく、定理です。

theorem fp_and_kay_share_goal_against_pathologies :
    (Decomposable Samples.FreeBase.G ∧
      DIPCompatible Samples.FreeBase.G Samples.FreeBase.π Samples.FreeBase.GA) ∧
    (Decomposable Samples.Inheritance.Giface ∧
      DIPCompatible Samples.Inheritance.Giface Samples.Inheritance.πIface
        Samples.Inheritance.GAIface) ∧
    (¬ DIPCompatible Samples.Inheritance.Gimpl Samples.Inheritance.πSub
        Samples.Inheritance.GASub ∧
      ¬ Decomposable Samples.StrongBase.G)

FP的モデル（FreeBase）とKay的OOP（契約継承）は Decomposable ∧ DIPCompatible を共有する。実装継承とStrongBaseはそれを欠く。

モデル	Decomposable	DIPCompatible
FP的モデル（FreeBase）	✓	✓
Kay的OOP（契約継承）	✓	✓
Java/C++的OOP（実装継承）	—	✗
強基盤（StrongBase）	✗	✗

FPは合成構造の保存から、Kay的OOPは射影構造の保存から、同じ目標——分解可能性とDIP整合性——に到達する。方向が違うだけです。

対立の焦点は実装継承に局所化できます。実装継承は親の内部実装への暗黙的依存を導入し、商をwell-definedでなくする。これはFP側から見れば「射影関手が合成を保存しない」であり、OOP側から見れば「LSP違反」です。同じ現象を異なるパラダイムの言葉で記述しているに過ぎません。

両陣営は実は同じ不変量——Decomposable ∧ DIPCompatible——を追っている。対立の焦点はパラダイムの違いではなく、実装継承にある。

8. ここまでで見えたこと

SOLIDとレイヤードの関係

第4部の主テーマを回収します。

SOLIDはミクロの規律です。各コンポーネントの責任分離、契約整合、射影整合を保証する。しかしシステム全体の分解可能性——マクロの構造——は保証しない。分解可能性を保証するのはレイヤードアーキテクチャの層制約であり、それはSOLIDとは独立な条件です。

実務への示唆は明確です。「SOLIDを守りましょう」と「レイヤードアーキテクチャにしましょう」はこれまで別々のベストプラクティスとして語られてきました。この定理はその関係を精密にする——両方必要であり、どちらか一方では不十分。

OOPとFPの共通項

セクション7で見た通り、FP的モデルとKay的OOPは同じ代数的目標を共有しています。パラダイム戦争の原因は実装継承であり、FPとOOPの違いではありませんでした。

設計パターンとは何か

二つの結果を統合すると、設計パターンの再定義が見えてきます。

設計パターンとは、射影整合・置換整合・分解可能性のいずれかをアーキテクチャに付与する操作である。SOLIDは前二者を、レイヤードアーキテクチャは第三層を担う。

従来「良い作法」として一括りにされていたパターンが、何を保証するかで分類できる。そしてどのパターンも3層全てをカバーするわけではない。この枠組みがあれば、パターンの選択は「好み」ではなく「どの層の保証が足りないか」という診断に基づく判断になります。

PatternKitはこの最小データです。分解証人 + 境界 + 局在性のバンドル。

theorem decomposable_of_patternKit (k : PatternKit C G) : Decomposable G

PatternKitがあれば分解可能。設計パターンの適用とは、このデータを構成する行為です。

第4部で圏論基盤を整えたことで、第5部の拡張理論が自然に定式化できる準備が整いました。ReflectiveSubcategoryが第5部で本格的に動き出します。

9. コード全体

本稿のLean 4コードは以下のファイルで構成されています。

ファイル	内容
`Category/Basic.lean`	SmallCategory, Functor, FullSubcategory, inclusion
`Category/Quotient.lean`	QuotientPresentation, WellDefinedOn
`Category/Decomposition.lean`	Filtration, LayerMonotone, Category.Decomposable, ReflectiveSubcategory, Category.PatternKit
`Core.lean`	ArchGraph, ComponentCategory, 橋渡し定理, 射影関手, DIPCompatible, LSP, 継承モデル
`SOLID.lean`	SRPFor, OCPFor, ISPFor, LSPFor, DIPFor, SOLID5For, ResponsibilityStrictlyDecreasing
`Samples/Layered.lean`	4層アーキテクチャ（分解可能の正例）
`Samples/Spaghetti.lean`	3点循環（分解不能の反例）
`Samples/FreeBase.lean`	自由基盤（DIP整合の正例）
`Samples/StrongBase.lean`	基盤内循環（DIP不整合の反例）+ 修復操作
`Samples/Inheritance.lean`	継承の3段階証明チェーン
`Samples/SOLIDCases.lean`	SOLID 5原則の成立/違反例 + SOLID⇏Decomposable反例
`Comparisons.lean`	全対比定理の束ね

機械検証された主要な定理をまとめます。

定理	内容
`categoricalDecomposable_of_decomposable`	グラフ版→圏論版の分解可能性の橋渡し
`layered_vs_spaghetti`	Layered: 分解可能、Spaghetti: 分解不能
`not_quotient_of_lspViolationAt`	LSP違反 → 商破壊（一般定理）
`not_dip_of_lspViolationAt`	LSP違反 → DIP不整合（一般定理）
`implementation_vs_interface_inheritance`	実装継承: 商破壊+DIP不整合、契約継承: 分解可能+DIP整合
`solid_five_principles_suite`	SOLID 5原則の成立/違反を一括確認
`solid5_not_imply_decomposable`	SOLID 5原則全充足でも分解不能（存在量化版）
`solid5_not_imply_decomposable_counterexample`	上の具体反例（GsolidButCycle）
`ocp_violation_does_not_force_dip_failure`	OCP違反 ⇏ DIP不整合（独立性の反例）
`fp_and_kay_share_goal_against_pathologies`	FPとKay的OOPは同じ設計目標を共有
`repair_operation_effect`	循環辺切断で分解可能性回復 + relationCount減少
`solid5_plus_responsibilityStrict_implies_decomposable`	SOLID + レイヤード制約 → 分解可能

GitHubリポジトリ公開準備中！

10. 次回予告

第5部：「なぜ機能追加でバグが出るのか」

機能追加を圏論的な構造保存拡張として定式化し、バグを不変量保存圏からの逸脱として定義します。

第4部で導入した二つの道具が鍵になります。

-- 「良い部分圏」に射影する関手の存在（第4部で器だけ用意した）
structure ReflectiveSubcategory (C : SmallCategory) where
  sub : FullSubcategory C
  reflector : Functor C (sub.toCategory)

-- SOLID + レイヤード → 分解可能（第4部で証明済み）
theorem solid5_plus_responsibilityStrict_implies_decomposable ...

第5部では、ReflectiveSubcategory の reflector を「機能追加後のアーキテクチャを健全な部分圏に引き戻す操作」として解釈し、solid5_plus_responsibilityStrict_implies_decomposable が保証する分解可能性が機能追加後も保存されるための条件を特定します。

おわりに

第4部では、SOLID 5原則とレイヤードアーキテクチャの関係を圏論的に定式化し、Lean 4で機械検証しました。

最大の発見は「本稿の定式化では、SOLIDだけでは分解可能性が保証されない」ことです。5原則を完璧に守っても循環依存は排除できない。分解可能性にはレイヤードアーキテクチャの層制約が必要であり、その追加条件は分解可能性の定義と数学的に同型でした。SOLIDはミクロの健全性、レイヤードはマクロの分解可能性——両者は独立で補完的です。

副産物として「OOPとFPは同じ代数的目標を共有している」ことも証明しました。戦争の原因は実装継承であり、パラダイムの違いではありません。

全ての主張は「たぶんそうだよね」ではなく「型が通りました」として提示されています。

第5部に続きます。お楽しみに！