第1部はこちら

はじめに

こんにちは！
第1部では、ACIDを「状態空間上の構造保存の四次元分解」として再解釈し、Lean 4で機械検証しました。「公理が少ないほどモデル集合が広く、摂動に対して頑健」という反単調性定理も証明しました。

第2部では視点を変えます。

Event Sourcing、CRUD、Sagaという三つのアーキテクチャパターンを、同じ代数的言語で記述して比較します。

この三者は実務で「トレードオフ」として語られることが多いですよね。でも、何と何をトレードしているのか——意外と精密に説明されていません。「Event Sourcingはログが残るから安心」「CRUDはシンプルだけど履歴が消える」「Sagaは補償で戻せるけど完全には戻らない」。直感的にはわかる。でも、なぜそうなるのか？

本稿では、三者を状態遷移の代数的構造として統一的に定義し、「関係式が増えるほど故障モードが増える」という格子構造をLean 4で証明します。

三つのパターンとは

本題に入る前に、三つのパターンを簡単に紹介しておきます。これらはいずれもマイクロサービスアーキテクチャの文脈で頻繁に登場し、サービス間のデータ管理戦略として検討されるものです。

Event Sourcing（イベントソーシング）
状態を直接保存するのではなく、「何が起きたか」をイベントとして全てログに記録するアーキテクチャです。現在の状態が知りたければ、ログを最初から順に再生して復元します。ECサイトなら、「ユーザーAが商品Xをカートに追加した」「ユーザーAが注文を確定した」といったイベントが次々とログに追記されていく。状態は常にログから導出されるので、ログさえ無事なら過去の任意の時点の状態を再現できます。マイクロサービス間の通信もイベントを介して行われるため、サービス同士の結合度が低く保たれます。

CRUD
Create（作成）、Read（読み取り）、Update（更新）、Delete（削除）の四操作でデータを直接書き換えるアーキテクチャです。リレーショナルDBの典型的な使い方そのもの。ユーザーの住所が変われば、テーブルの該当行をUPDATEする。以前の住所は上書きされて消えます。シンプルで直感的ですが、「昨日の時点ではどうだったか」を知るには別途履歴テーブルなどの仕組みが必要です。マイクロサービスでCRUDベースのサービスが互いのAPIを同期的に呼び合うと、サービス間の結合が密になり、いわゆる「分散モノリス」に陥りやすいことが知られています。

Saga（サーガ）
複数のサービスにまたがる長時間トランザクションを、「前進操作と補償操作の対」の連鎖として実現するパターンです。マイクロサービスアーキテクチャでは、単一のDBトランザクションでまとめられない処理をSagaで協調させることが多くなっています。例えば、ECサイトの注文処理で「在庫サービスで在庫確保 → 決済サービスで決済 → 配送サービスで配送手配」と進んでいき、途中の決済で失敗したら「在庫確保を取り消す」という補償操作で巻き戻す。ただし、補償は完全な巻き戻しではありません。「一度在庫を確保して取り消した」という事実は残ります。

マイクロサービスの設計では、この三者をどう選び、どう組み合わせるかが重要な判断になります。しかし、その判断の根拠はしばしば経験則にとどまっています。本稿では、三者の構造的な違いを代数的に明らかにすることで、この判断に理論的な基盤を与えることを目指します。

この記事で扱うこと

Event Sourcingを「自由モノイドから状態モノイドへの準同型」として定式化する
CRUDを「Kleisli射の合成」として定式化し、履歴消失性を型で表現する
Sagaの補償条件を「片側逆元 up to 観測同値」として定義する
三者の故障モードを型として分離し、格子上の順序関係を証明する
全てLean 4で機械検証する

この記事で扱わないこと

P-観測同値と商モノイドの構成（次回以降）
依存グラフと故障モード移送定理（次回以降）
分散アーキテクチャへの拡張（次回以降）

1. 三者を同じ土俵に載せる

第1部で定義した Model を思い出しましょう。状態空間 S、トランザクション Txn、不変量 inv の三つ組でした。第2部では、この枠組みの上にEvent Sourcing / CRUD / Sagaを具体的に載せていきます。

共通の言語は状態遷移です。どのパターンも、結局は「ある状態を受け取って、次の状態を返す（か、失敗する）」という操作の集まりです。違いは、その操作にどれだけの**関係式（制約）**が課されているかです。

三者を代数的に並べると、こうなります：

パターン	表示
Event Sourcing	`⟨ E \| ∅ ⟩ →^{fold} ⟨ S \| R_S ⟩`
Saga	`M_P / ≈_P`（片側逆元つき）
CRUD	`⟨ Create, Update, Delete \| C_schema, C_FK, C_unique, C_cascade, ... ⟩`

左辺の関係式が増えるほど、右辺の制約が増える。制約が増えるほど壊れ方が多様になる。これが第1部の robust_of_weaker の具体的な現れです。

2. Event Sourcing——自由モノイドの力

最小モデル

Event Sourcingの核はシンプルです。イベント型 E と状態型 S に対して、初期状態と1イベントの適用関数だけを持つ：

structure EventSourcingModel (S : Type u) (E : Type v) where
  init : S
  applyEvent : E → S → S

これだけ。ログ（イベントの列）は List E で表現します：

abbrev Log (E : Type v) := List E

List E は E を生成元とする自由モノイドです。連結（++）がモノイド演算、空リスト [] が単位元。そして関係式は結合律だけ——それ以外の等式は一切課されていません。

fold：自由モノイドから状態への写像

ログを状態に変換する fold を定義します：

def fold (M : EventSourcingModel S E) : List E → S
  | es => M.foldFrom M.init es

def foldFrom (M : EventSourcingModel S E) (s0 : S) : List E → S
  | [] => s0
  | e :: es => M.applyEvent e (foldFrom M s0 es)

空のログは初期状態を返し、イベント e を先頭に持つログは、残り es を先に末尾側から畳み込んだ結果に e を適用します。つまり、この定義ではリストの右側（末尾）から左側（先頭）へ再生する形になっています。[e1, e2, e3] なら、applyEvent e1 (applyEvent e2 (applyEvent e3 init)) ——e3 → e2 → e1 の順で適用されます。

注意： これは Haskell でいう foldr に相当する構造です。foldl（左畳み込み）ではありません。再帰の展開方向とイベント適用の順序を混同しやすいので注意してください。リストの先頭 e が「最後に」適用される関数になる、という点が直感に反するかもしれませんが、これは applyEvent e を状態自己準同型と見たときの関数合成の順序（f ∘ g は g を先に適用してから f）と整合しています。

準同型性

fold の最も重要な性質は、ログの連結に対する準同型性です：

theorem fold_append (xs ys : List E) :
    M.fold (xs ++ ys) = M.foldFrom (M.fold ys) xs

ログを連結してから畳み込むのと、分けて畳み込むのは同じ結果になる。 これは第1部の replay_append と本質的に同じ構造です。リスト連結（自由モノイドの演算）が状態遷移の合成に対応する。

replayEndo として関数の合成の言葉で書くと、さらに明確になります：

theorem replayEndo_append (xs ys : Log E) :
    M.replayEndo (xs ++ ys) = M.replayEndo xs ∘ M.replayEndo ys

ログ連結 → 関数合成。 これはモノイド準同型そのものです。

一意性

fold は「初期値から始めて末尾側から1イベントずつ適用する」という再帰方程式を満たす写像として一意です：

def IsFoldLike (f : Log E → S) : Prop :=
  f [] = M.init ∧ ∀ e es, f (e :: es) = M.applyEvent e (f es)

theorem fold_unique {f : Log E → S} (hf : M.IsFoldLike f) :
    f = M.fold

これは自由モノイドの普遍性の最小形式化です。自由モノイドから任意の代数への準同型は、生成元の行き先を決めれば一意に定まる——その「生成元の行き先」が applyEvent であり、一意に定まる準同型が fold です。

「何を言っているかはわかるけど、何が嬉しいの？」と思うかもしれません。嬉しさは故障の分離にあります。

故障の三層分離

Event Sourcingの故障モードを型として定義します：

inductive ESFaultLayer where
  | freeStructure
  | homomorphism
  | quotientInvariant

inductive ESFault where
  | logCorruption
  | foldBug
  | invariantViolation

三つの層に対応します：

層	故障	意味
層1：自由構造	`logCorruption`	ログ自体が壊れた（ディスク故障、ネットワーク破損）
層2：準同型	`foldBug`	fold関数にバグがある（リプレイが正しくない）
層3：商側制約	`invariantViolation`	ビジネスロジックの違反（存在しない商品の注文など）

そして決定的に重要な定理：

theorem fault_layer_separation :
    ESFault.layer .logCorruption ≠ ESFault.layer .foldBug ∧
    ESFault.layer .foldBug ≠ ESFault.layer .invariantViolation

三つの故障は異なる層に属する。 つまり、故障が局在化されている。

なぜこれが起きるか？ ログが自由モノイドだからです。自由モノイドには結合律以外の関係式がない。関係式がないから、「関係式に違反する」という故障モードが存在しない。自由構造の破壊は代数の外部（ディスク故障など）からしか起きえない。これが「自由対象は頑健」の精密な意味です。

層2（foldバグ）は検出・修復が可能です。ログが無傷なら、foldを修正して全ログを再生するだけで状態を正しく再構築できる。層3（不変量違反）はビジネスロジックの問題であり、アーキテクチャとは独立に対処できる。

故障が層ごとに分離されているから、各層を独立に対処できる。 これがEvent Sourcingの構造的な強さです。

本稿での定理の分類について： 以降、各定理に definitional または proved という注釈をつけています。definitional は「定義の構造上自動的に成り立つ性質」——Lean上では rfl や decide で即座に閉じるもの。proved は「非自明な補題や構成を経て証明された性質」——定義だけからは自明でなく、他の定理を組み合わせて初めて示せるもの。この区別は「何がLeanの力で保証されているか」を正直に示すためのものです。

ここまでの ESFault / ESFaultLayer は列挙型による分類ラベルでした（fault_layer_separation は decide で終わる definitional な性質）。これだけでは「三層分離が代数構造に由来する」とは言い切れません。

そこでもう一段踏み込み、各層の故障を命題として定義します：

/-- 層2故障（命題版）：fold が append に対する準同型性を破っている。 -/
def FoldNotHomomorphic (f : Log E → S) : Prop :=
  ∃ xs ys : Log E, f (xs ++ ys) ≠ M.foldFrom (f ys) xs

/-- 層3故障（命題版）：ログ再生後の不変量違反。 -/
def InvariantViolated (inv : S → Prop) (log : Log E) : Prop :=
  ¬ inv (M.fold log)

FoldNotHomomorphic f は「関数 f が、ログの連結に対する準同型方程式を破る入力が存在する」ことを言っています。これは非自明な命題です——任意の f について成立するわけではありません。

そして核心の定理：

/-- 正しい fold は層2故障を起こさない。（proved: fold_append を使用） -/
theorem fold_no_layer2_fault : ¬ M.FoldNotHomomorphic M.fold := by
  intro ⟨xs, ys, hneq⟩
  exact hneq (M.fold_append xs ys)

正しい fold は準同型方程式を満たすから、層2故障を起こしえない。 この証明は自明ではなく、先に証明した fold_append（準同型性）を本質的に使っています。逆に、バグのある fold を渡せば FoldNotHomomorphic は成立する——層2故障は「代数構造からの逸脱」として精密に特徴づけられたわけです。

3. CRUD——Kleisli射と履歴の消失

エラー型とKleisli射

CRUDの世界では、操作は失敗しうる状態遷移です。これを Except モナドのKleisli射として表現します：

inductive CrudErr where
  | schema
  | constraint
  | conflict

abbrev TxnK (S : Type u) (Err : Type v) := S → Except Err S

TxnK S CrudErr は「状態 S を受け取って、成功すれば新しい状態を返し、失敗すればエラーを返す」関数です。FK違反なら constraint、一意制約違反なら schema、楽観ロック競合なら conflict。

合成はKleisli合成です：

def kcomp (g f : TxnK S Err) : TxnK S Err :=
  fun s =>
    match f s with
    | .ok s' => g s'
    | .error e => .error e

f が失敗したらそこで停止し、エラーを伝播する。成功したら g に渡す。モナドの >>= そのものですね。

CRUDモデル

structure CRUDModel (S : Type u) where
  Op : Type v
  step : Op → TxnK S CrudErr
  inv : S → Prop
  relationTags : List ConstraintTag
  constraints : List (DBConstraint S)

Op は操作型（INSERT, UPDATE, DELETEなど）。step は各操作のKleisli射としての意味論。relationTags は制約の種類を記録するタグのリストです：

inductive ConstraintTag where
  | schema
  | foreignKey
  | unique
  | cascade
  | custom

スキーマ制約、外部キー制約、一意制約、カスケード削除、カスタム制約——CRUDの世界には大量の関係式があります。Event Sourcingの ⟨ E | ∅ ⟩（関係式なし）と対比すると、⟨ Op | C_schema, C_FK, C_unique, C_cascade, ... ⟩ です。

操作列の実行

def run (M : CRUDModel S) : List M.Op → TxnK S CrudErr
  | [] => fun s => .ok s
  | op :: ops => kcomp (M.run ops) (M.step op)

空の操作列は恒等（そのまま成功を返す）。op :: ops は op を実行してから残りを実行する。

履歴消失性

CRUDの決定的な性質は履歴が消えることです：

def OverwritesHistory : Prop :=
  ∀ ops : List M.Op, ∀ s : S, ∃ r : Except CrudErr S, M.run ops s = r

theorem overwritesHistory : M.OverwritesHistory := by
  intro ops s
  exact ⟨M.run ops s, rfl⟩

run は最終状態（かエラー）だけを返し、中間状態を一切返さない。この定理は定義上自明に成立します（definitional）。これは「CRUDのインターフェースが履歴を返す手段を持たない」ことの最小形式化——run の型 List Op → TxnK S CrudErr 自体が中間状態を外部に公開する経路を持っていないことを明示しています。

しかし、本当に言いたいのは「履歴の情報が失われる」ことです。これを非自明な命題として定式化します：

/-- 履歴消失性（非単射版）：異なる操作列が同じ最終結果を生みうる。 -/
def HistoryLoss : Prop :=
  ∃ (ops₁ ops₂ : List M.Op) (s : S),
    ops₁ ≠ ops₂ ∧ M.run ops₁ s = M.run ops₂ s

HistoryLoss は「異なる操作履歴が同じ最終状態に潰れる」——情報が非可逆的に失われることの形式化です。これは OverwritesHistory と違い、具体的なモデルを与えないと証明できません。

そこで最小の具体例を構成します。2セルメモリ（Nat 値を持つ2つのセル）：

structure Mem2 where
  cell0 : Nat
  cell1 : Nat

inductive Mem2Op where
  | write0 (val : Nat)
  | write1 (val : Nat)

このモデルで HistoryLoss を証明します（proved）：

/-- 「cell0に1を書いてから2を書く」と「cell0に2を書く」は同じ最終状態。 -/
theorem mem2_historyLoss : mem2Model.HistoryLoss

操作列 [write0 1, write0 2] と [write0 2] は異なる履歴ですが、同じ最終状態 { cell0 := 2, cell1 := 0 } を生みます。最初の書き込みは2回目の書き込みで上書きされ、「1を書いた」という情報は最終状態からは復元不能です。

Event Sourcingなら、ログが無傷であれば任意の時点の状態を再構築できます。CRUDではそれが原理的に不可能です。「3日前の状態はどうだった？」に答えられない。操作が直接状態を上書きし、以前の状態は消えている。mem2_historyLoss はこの現象を最小の具体例で数学的に実証しています。

故障の融合

CRUDの故障モードはEvent Sourcingとは根本的に異なります：

inductive CRUDFaultLayer where
  | fusedStructureInvariant
  | runtimeConflict

inductive CRUDFault where
  | schemaViolation
  | constraintViolation
  | conflictFailure

注目すべきは fusedStructureInvariant です。Event Sourcingでは分離されていた層1（構造の破壊）と層3（不変量違反）が融合しています：

def CRUDFault.layer : CRUDFault → CRUDFaultLayer
  | .schemaViolation => .fusedStructureInvariant
  | .constraintViolation => .fusedStructureInvariant
  | .conflictFailure => .runtimeConflict

スキーマ違反も制約違反も同じ fusedStructureInvariant 層に分類される。なぜなら、CRUDでは状態空間自体が制約で切り取られており（S = { s ∈ ∏ᵢ Tableᵢ | C(s) }）、「自由な構造」が存在しないからです。自由なログがないから、「ログを再生して状態を再構築する」という層2（準同型）も存在しない。

三層分離が成立しない——これがCRUDの代数的な弱さです。故障が融合しているから、何が壊れたのかを切り分けにくく、一つの問題が他の問題にカスケードしやすい。

4. Saga——補償という「片側逆元」

ステップとモデル

Sagaは「前進操作と補償操作の対」の列です：

structure SagaStep (S : Type u) (Err : Type v) where
  forward : S → Except Err S
  compensate : S → Except Err S

structure SagaModel (S : Type u) (Err : Type v) where
  steps : List (SagaStep S Err)
  inv : S → Prop

各ステップは forward（前に進む操作）と compensate（戻す操作）を持っています。ECサイトでいえば、「在庫を確保する / 在庫確保を取り消す」「決済する / 返金する」のような対です。

片側逆元 up to 観測同値

Sagaの補償条件を正確に定義するのは意外と難しい。compensate ∘ forward = id と書きたくなりますが、これは強すぎます。在庫確保してから取り消しても、「一度確保された」という履歴は残るかもしれない。完全に元の状態には戻らない。

そこで観測同値を使います：

def LeftInverseUpTo (Obs : S → S → Prop) (st : SagaStep S Err) : Prop :=
  ∀ s s', st.forward s = .ok s' →
    ∃ s'', st.compensate s' = .ok s'' ∧ Obs s'' s

これは何を言っているかというと：

forward が状態 s から s' への遷移に成功したなら
compensate を s' に適用するとある s'' に成功し
その s'' は元の状態 s と観測同値 Obs の関係にある

代数的に書くと c ⋆ f ≈_P pure です。補償 c を前進 f の後に適用すると、恒等操作 pure と観測的に区別できない——完全な逆元ではなく片側逆元、しかも厳密等号ではなく観測同値まで。

固有の故障モード

Sagaには固有の故障モードがあります：

inductive SagaFault where
  | forwardFailure
  | compensationFailure

def CompensationFailure (st : SagaStep S Err) : Prop :=
  ∃ s s', st.forward s = .ok s' ∧
    ∀ s'', st.compensate s' ≠ .ok s''

CompensationFailure は「前進操作は成功したが、補償操作が全ての出力状態に対して失敗する」状態です。前にも進めず、後ろにも戻れない。これはEvent SourcingにもCRUDにも存在しないSaga固有の故障モードです。

なぜ固有なのか？ Event Sourcingにはそもそも「戻す」という概念がない（ログは追記のみ）。CRUDには「対になる補償操作」がない。「前進と補償の対」という構造を持つからこそ、「補償が失敗する」という新たな壊れ方が生まれるのです。

しかし、現実のSagaの事故はこれだけではありません。もう一つの重要な故障モードがあります：

/-- 補償は成功するが、観測同値に戻らない故障。 -/
def CompensationDrift (Obs : S → S → Prop) (st : SagaStep S Err) : Prop :=
  ∃ s s' s'', st.forward s = .ok s' ∧
    st.compensate s' = .ok s'' ∧
    ¬ Obs s'' s

CompensationDrift は「補償操作は .ok を返すが、戻った状態 s'' が元の状態 s と観測同値ではない」という故障です。返金はしたが手数料は戻らない。在庫は解放したが予約履歴が残る。補償は「成功した」のに、状態はズレている——これが現実のSagaで最も厄介な壊れ方です。

この二つの故障モードは、同一の状態に対して排他的であることが証明できます（proved）：

theorem failureAt_and_driftAt_exclusive
    (Obs : S → S → Prop) (st : SagaStep S Err) (s s' : S) :
    CompensationFailureAt st s s' →
    ¬ CompensationDriftAt Obs st s s'

ある状態 s' に対して、補償が失敗する（CompensationFailureAt）なら、補償が成功してドリフトする（CompensationDriftAt）ことはありえない。補償は「失敗するか、成功するがズレるか」の二択であり、同時に起きることはない。

5. 三者の格子構造——関係式と故障の単調性

比較のための抽象化

三者を比較するために、共通の抽象点を定義します：

inductive FailureMode where
  | externalCorruption     -- 物理層の破壊
  | semanticsBug           -- 意味論のバグ（ES: fold準同型破壊、CRUD: step実装バグ）
  | invariantViolation     -- 不変量違反
  | compensationFailure    -- Saga: 補償が失敗
  | compensationDrift      -- Saga: 補償は成功するが観測同値に戻らない
  | fusedFailure           -- CRUD: 構造と不変量の融合故障

structure ArchitecturePoint where
  relationComplexity : Nat
  modes : FailureMode → Prop

relationComplexity は関係式の強さ（大きいほど制約が多い）。modes は想定される故障モードの集合です。

旧版では failureVariety : Nat という数値指標を持っていましたが、数値の割り当てが恣意的になるため廃止し、modes の包含関係のみで順序を定義するように改めました。

また、旧版の homomorphismBug（準同型バグ）は semanticsBug（意味論バグ）に統一しました。Event Sourcingでは「foldの準同型破壊」、CRUDでは「step/runの実装バグ」と意味が異なりますが、「意味論が正しくない」という共通の抽象としてまとめることで、三者間の modes 包含が自然に成立します。

順序の定義

def ArchitecturePoint.LE (a b : ArchitecturePoint) : Prop :=
  a.relationComplexity ≤ b.relationComplexity ∧
    ∀ m, a.modes m → b.modes m

制約が弱く故障モードが少ないほど下位。これが前順序の定義です。反射律と推移律を証明します（proved）：

theorem le_refl (a : ArchitecturePoint) : a ≤ a
theorem le_trans {a b c : ArchitecturePoint} : a ≤ b → b ≤ c → a ≤ c

三者の代表点

def eventSourcingPoint : ArchitecturePoint where
  relationComplexity := 0
  modes := fun m =>
    m = .externalCorruption ∨ m = .semanticsBug ∨ m = .invariantViolation

def sagaPoint : ArchitecturePoint where
  relationComplexity := 1
  modes := fun m =>
    m = .externalCorruption ∨ m = .semanticsBug ∨
    m = .invariantViolation ∨
    m = .compensationFailure ∨ m = .compensationDrift

def crudPoint : ArchitecturePoint where
  relationComplexity := 2
  modes := fun m =>
    m = .externalCorruption ∨ m = .semanticsBug ∨
    m = .invariantViolation ∨
    m = .compensationFailure ∨ m = .compensationDrift ∨
    m = .fusedFailure

Event Sourcingは relationComplexity = 0（関係式なし）で、故障は3種（外部破壊・意味論バグ・不変量違反）。Sagaは relationComplexity = 1 で、ESの3種に補償失敗と補償ドリフトが加わり5種。CRUDは relationComplexity = 2 で、さらに融合故障が加わり6種です。

crudPoint が compensationFailure / compensationDrift を含む理由： modes は「このアーキテクチャで起きうる故障モードの保守的上界（may-fail集合）」として設計しています。CRUD単体には補償操作はありませんが、実務ではCRUDの上にSaga的な補償ロジックを手動で組むことがあり、その場合に補償失敗やドリフトが発生しえます。modes を保守的上界として定義することで、≤ の包含関係が自然に成立し、格子構造がきれいに閉じます。「CRUDが固有に持つ故障」と「CRUDの上で起きうる故障」の区別が重要な場合は、fusedFailure だけがCRUD固有の故障モードです。

核心の定理

theorem eventSourcing_le_saga : eventSourcingPoint ≤ sagaPoint
theorem saga_le_crud : sagaPoint ≤ crudPoint

Event Sourcing ≤ Saga ≤ CRUD（proved）。

推移律と合わせると eventSourcingPoint ≤ crudPoint も得られます。そして単調性定理（proved）：

theorem modes_monotone_of_le {a b : ArchitecturePoint} (h : a ≤ b) :
    ∀ m, a.modes m → b.modes m

theorem relation_increase_implies_modes_monotone :
    (∀ m, eventSourcingPoint.modes m → sagaPoint.modes m) ∧
    (∀ m, sagaPoint.modes m → crudPoint.modes m)

本モデルでは、関係式の複雑性が上がるほど、故障モードの集合は単調に包含関係で拡大する。

注意すべきは、これは「一般にあらゆるアーキテクチャで成立する」という主張ではなく、eventSourcingPoint ≤ sagaPoint ≤ crudPoint という三者のモデル化に対する比較定理だということです。Lean上で証明されているのはこの具体的な順序関係と、順序から導かれる単調性です。

これは第1部の robust_of_weaker（公理が少ないほど頑健）を具体的なアーキテクチャパターンの比較として実現したものです。抽象的な定理が、Event Sourcing / CRUD / Sagaという現実のパターンの比較に降りてきた。

三者の全体像

Event Sourcing                    ← 関係式なし。最大の自由度。
  ⟨ E | ∅ ⟩                         故障は代数外部のみ。
  故障モード: 3種                    ログがあれば何度でも再構築可能。
        ↓ ≤
Saga                              ← 観測商上の近似逆元を持つ中間点。
  M_P / ≈_P（片側逆元つき）           固有故障：補償失敗＋補償ドリフト。
  故障モード: 5種                    「ほぼ戻せる」が完全ではない。
        ↓ ≤
CRUD                              ← 強い関係式を持つ高制約点。
  ⟨ Op | C_schema, C_FK, ... ⟩      故障：全層融合、局在化不能。
  故障モード: 6種                    履歴は消え、再構築不能。

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

Event Sourcingはなぜ「壊れにくい」のか

「ログを残しておけば安心」というのは現場の知恵ですが、代数的に見るとその理由がはっきりします。ログが自由モノイドだから、関係式に起因する故障がそもそも存在しない。故障が三層に分離されるから、各層を独立に対処できる。foldにバグがあっても、ログが無傷ならfoldを直して再生すればいい。

CRUDはなぜ「壊れやすい」のか

関係式（FK制約、一意制約、カスケード削除など）が大量にあるから。関係式が多いほど、違反のパターンが多くなる。しかも履歴が消えるから、「いつ何が壊れたか」を遡って調べることが難しい。故障の層1と層3が融合しているから、原因の切り分けも困難。

Sagaはなぜ「中間」なのか

Event Sourcingほど自由ではないが、CRUDほど制約に縛られてもいない。「片側逆元 up to 観測同値」という構造を持つことで、ある程度の巻き戻しが可能。ただし、補償失敗と補償ドリフトという二つの固有故障モードが新たに生まれる。特に補償ドリフト——補償は「成功」したのに状態がズレている——は、現実のマイクロサービスで最も厄介な壊れ方です。

これは「定性的な感想」ではない

上の比較は全てLean 4で型検査を通過した定理に基づいています。eventSourcing_le_saga も saga_le_crud も relation_increase_implies_modes_monotone も、機械検証済みです。「たぶんそうだよね」ではなく「型が通りました」。

マイクロサービスへの示唆

この格子構造は、マイクロサービスの設計判断に直接つながります。CRUDベースのサービスが互いのAPIを同期的に叩き合う構成は、関係式の密な結合をネットワーク上に持ち出しただけで、故障の融合がサービス境界を超えて伝播します。あるサービスのスキーマ変更が他のサービスを巻き込んで壊れる——分散モノリスと呼ばれる現象の代数的な正体がここにあります。

一方、Event Sourcingでサービス間をイベントで接続する構成は、各サービスが自由なログを持ち、サービス間の結合は「イベントの購読」という緩い関係にとどまります。故障が各サービスの内部に局在化されやすい。Sagaはその中間で、サービス間の協調を補償で実現するが、補償失敗という結合点が生まれる。

格子の順序 Event Sourcing ≤ Saga ≤ CRUD は、マイクロサービスにおけるサービス間結合の強さとも対応しているわけです。

7. コード全体

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

ファイル	内容
`EventSourcing.lean`	ES最小モデル、fold、準同型性、一意性、故障三層分離（列挙型＋命題版）
`CRUD.lean`	Kleisli射、CRUDモデル、操作列実行、履歴消失性（インターフェース版＋非単射版）、故障融合
`Saga.lean`	Sagaステップ、片側補償条件、補償失敗、補償ドリフト、排他性
`Lattice.lean`	ArchitecturePoint、順序、三者の代表点、modes包含による単調性定理

機械検証された主要な定理をまとめます。性質欄の definitional は定義から自動的に成り立つ性質（rfl / decide で閉じる）、proved は非自明な証明を要する性質です：

定理	内容	性質
`fold_append`	ログ連結に対するfoldの準同型性	proved
`replayEndo_append`	ログ連結→関数合成のモノイド準同型	proved
`fold_unique`	foldはIsFoldLikeを満たす唯一の写像（普遍性）	proved
`fault_layer_separation`	ES故障の三層分離（列挙型）	definitional
`fold_no_layer2_fault`	正しいfoldは層2故障を起こさない	proved
`overwritesHistory`	CRUDのインターフェース上の履歴消失性	definitional
`mem2_historyLoss`	2セルメモリでの履歴情報の非可逆的消失	proved
`failureAt_and_driftAt_exclusive`	補償失敗と補償ドリフトの排他性	proved
`eventSourcing_le_saga`	ES ≤ Saga（格子順序）	proved
`saga_le_crud`	Saga ≤ CRUD（格子順序）	proved
`modes_monotone_of_le`	故障モード集合の単調性	proved
`relation_increase_implies_modes_monotone`	関係式増加→故障モード集合拡大	proved

コード

EventSourcing.lean

namespace AcidLean.Part2

universe u v

/-- Event Sourcing のログ（自由モノイド）。 -/
abbrev Log (E : Type v) := List E

/-- Event Sourcing の故障層。 -/
inductive ESFaultLayer where
  | freeStructure
  | homomorphism
  | quotientInvariant
deriving DecidableEq, Repr

/-- Event Sourcing の故障モード（三層分離）。 -/
inductive ESFault where
  | logCorruption
  | foldBug
  | invariantViolation
deriving DecidableEq, Repr

/-- 故障モードを三層へ分類する。 -/
def ESFault.layer : ESFault → ESFaultLayer
  | .logCorruption => .freeStructure
  | .foldBug => .homomorphism
  | .invariantViolation => .quotientInvariant

theorem fault_layer_separation :
    ESFault.layer .logCorruption ≠ ESFault.layer .foldBug ∧
    ESFault.layer .foldBug ≠ ESFault.layer .invariantViolation := by
  constructor <;> decide

/-- Event Sourcing の最小モデル。 -/
structure EventSourcingModel (S : Type u) (E : Type v) where
  init : S
  applyEvent : E → S → S

namespace EventSourcingModel

variable {S : Type u} {E : Type v} (M : EventSourcingModel S E)

/-- 1イベントの意味論（状態自己準同型）。 -/
def eventEndo (M : EventSourcingModel S E) (e : E) : S → S :=
  M.applyEvent e

/-- ログ全体の意味論（状態自己準同型）。 -/
def replayEndo (M : EventSourcingModel S E) : Log E → S → S
  | [] => id
  | e :: es => M.eventEndo e ∘ replayEndo M es

/-- 任意の初期状態 `s0` からログを再生する。 -/
def foldFrom (M : EventSourcingModel S E) (s0 : S) : List E → S
  | [] => s0
  | e :: es => M.applyEvent e (foldFrom M s0 es)

/-- ログを状態へ畳み込む `fold`。 -/
def fold (M : EventSourcingModel S E) : List E → S
  | es => M.foldFrom M.init es

@[simp] theorem fold_nil : M.fold [] = M.init := rfl

@[simp] theorem fold_cons (e : E) (es : List E) :
    M.fold (e :: es) = M.applyEvent e (M.fold es) := rfl

@[simp] theorem foldFrom_nil (s0 : S) : M.foldFrom s0 [] = s0 := rfl

@[simp] theorem foldFrom_cons (s0 : S) (e : E) (es : List E) :
    M.foldFrom s0 (e :: es) = M.applyEvent e (M.foldFrom s0 es) := rfl

theorem foldFrom_append (s0 : S) (xs ys : List E) :
    M.foldFrom s0 (xs ++ ys) = M.foldFrom (M.foldFrom s0 ys) xs := by
  induction xs with
  | nil =>
      simp [foldFrom]
  | cons x xs ih =>
      simp [foldFrom, ih]

/--
`fold` は `List E` の連結に対して準同型的に振る舞う。
右辺は「先に `ys` を反映した状態を初期値に、`xs` を再生する」形。
-/
theorem fold_append (xs ys : List E) :
    M.fold (xs ++ ys) = M.foldFrom (M.fold ys) xs := by
  simpa [fold] using M.foldFrom_append M.init xs ys

/-- `replayEndo` は `Log` 連結を合成へ写す（準同型）。 -/
theorem replayEndo_append (xs ys : Log E) :
    M.replayEndo (xs ++ ys) = M.replayEndo xs ∘ M.replayEndo ys := by
  induction xs with
  | nil =>
      simp [replayEndo]
  | cons x xs ih =>
      funext s
      simp [replayEndo, ih, Function.comp]

/-- `fold` は `replayEndo` を `init` へ適用したもの。 -/
theorem fold_eq_replayEndo_apply (xs : Log E) :
    M.fold xs = M.replayEndo xs M.init := by
  induction xs with
  | nil =>
      simp [fold, foldFrom, replayEndo]
  | cons x xs ih =>
      have htail : M.foldFrom M.init xs = M.replayEndo xs M.init := by
        simpa [fold] using ih
      simp [fold, foldFrom, replayEndo, htail, eventEndo]

/-- `fold` を特徴づける再帰方程式。 -/
def IsFoldLike (f : Log E → S) : Prop :=
  f [] = M.init ∧ ∀ e es, f (e :: es) = M.applyEvent e (f es)

/-- `fold` は `IsFoldLike` を満たす。 -/
theorem fold_isFoldLike : M.IsFoldLike M.fold := by
  refine ⟨by simp [fold], ?_⟩
  intro e es
  simp [fold, foldFrom]

/-- `fold` は `IsFoldLike` を満たす写像として一意。 -/
theorem fold_unique {f : Log E → S} (hf : M.IsFoldLike f) :
    f = M.fold := by
  funext xs
  induction xs with
  | nil =>
      simpa [IsFoldLike] using hf.1
  | cons e es ih =>
      have hcons := hf.2 e es
      simp [hcons, ih, fold, foldFrom]

section FaultPropositions

/--
層1故障（命題版）: ログが外部要因で破損している。
モデル内部からは直接導けないため、外部与件として扱う。
-/
def LogCorrupted (actual expected : Log E) : Prop :=
  actual ≠ expected

/--
層2故障（命題版）: `append` に対する準同型性が破れている。
`f` が「正しい `fold` 方程式」から逸脱することとして定義する。
-/
def FoldNotHomomorphic (f : Log E → S) : Prop :=
  ∃ xs ys : Log E, f (xs ++ ys) ≠ M.foldFrom (f ys) xs

/-- 層3故障（命題版）: ログ再生後の不変量違反。 -/
def InvariantViolated (inv : S → Prop) (log : Log E) : Prop :=
  ¬ inv (M.fold log)

/--
層1と層2は独立:
ログ破損が起きていない状況でも、層2故障を起こす `f` は存在しうる。
-/
theorem layer1_independent_of_layer2
    (hBuggy : ∃ f : Log E → S, M.FoldNotHomomorphic f) :
    ¬ (∀ (f : Log E → S),
        (¬ LogCorrupted ([] : Log E) []) →
        ¬ M.FoldNotHomomorphic f) := by
  intro hAll
  rcases hBuggy with ⟨f, hf⟩
  have hClean : ¬ LogCorrupted ([] : Log E) [] := by
    simp [LogCorrupted]
  exact (hAll f hClean) hf

/-- 正しい `fold` は層2故障を起こさない。 -/
theorem fold_no_layer2_fault : ¬ M.FoldNotHomomorphic M.fold := by
  intro hFault
  rcases hFault with ⟨xs, ys, hneq⟩
  exact hneq (M.fold_append xs ys)

end FaultPropositions

end EventSourcingModel
end AcidLean.Part2

CRUD.lean

namespace AcidLean.Part2

universe u v

/-- CRUD の故障層（2.2の議論に対応）。 -/
inductive CRUDFaultLayer where
  | fusedStructureInvariant
  | runtimeConflict
deriving DecidableEq, Repr

/-- CRUD の代表故障モード。 -/
inductive CRUDFault where
  | schemaViolation
  | constraintViolation
  | conflictFailure
deriving DecidableEq, Repr

/-- CRUD では層1（構造）と層3（不変量）が融合して現れる。 -/
def CRUDFault.layer : CRUDFault → CRUDFaultLayer
  | .schemaViolation => .fusedStructureInvariant
  | .constraintViolation => .fusedStructureInvariant
  | .conflictFailure => .runtimeConflict

/-- CRUD + RDB で想定する代表的エラー。 -/
inductive CrudErr where
  | schema
  | constraint
  | conflict
deriving DecidableEq, Repr

/-- スキーマ／整合性制約。 -/
abbrev DBConstraint (S : Type u) := S → Prop

/-- CRUD で管理される関係式（制約）の種類。 -/
inductive ConstraintTag where
  | schema
  | foreignKey
  | unique
  | cascade
  | custom
deriving DecidableEq, Repr

/-- Kleisli 射としての状態遷移。 -/
abbrev TxnK (S : Type u) (Err : Type v) := S → Except Err S

/-- `Except` 上の Kleisli 合成。 -/
def kcomp {S : Type u} {Err : Type v} (g f : TxnK S Err) : TxnK S Err :=
  fun s =>
    match f s with
    | .ok s' => g s'
    | .error e => .error e

/-- CRUD の最小モデル。 -/
structure CRUDModel (S : Type u) where
  Op : Type v
  step : Op → TxnK S CrudErr
  inv : S → Prop
  relationTags : List ConstraintTag
  constraints : List (DBConstraint S)

namespace CRUDModel

variable {S : Type u} (M : CRUDModel S)

/-- すべての宣言済み制約を満たす状態。 -/
def SatisfiesConstraints (s : S) : Prop :=
  ∀ c ∈ M.constraints, c s

/-- 操作列の逐次実行。 -/
def run (M : CRUDModel S) : List M.Op → TxnK S CrudErr
  | [] => fun s => .ok s
  | op :: ops => kcomp (run M ops) (M.step op)

@[simp] theorem run_nil : M.run [] = (fun s => Except.ok s) := rfl

@[simp] theorem run_cons (op : M.Op) (ops : List M.Op) :
    M.run (op :: ops) = kcomp (M.run ops) (M.step op) := rfl

/--
CRUD 実行は「最終状態かエラー」だけを返す。
中間履歴を外部値として返さない、という意味での履歴消失性。
-/
def OverwritesHistory : Prop :=
  ∀ ops : List M.Op, ∀ s : S, ∃ r : Except CrudErr S, M.run ops s = r

/-- CRUD モデルは定義上 `OverwritesHistory` を満たす。 -/
theorem overwritesHistory : M.OverwritesHistory := by
  intro ops s
  exact ⟨M.run ops s, rfl⟩

/--
履歴消失性（非単射版）:
異なる操作列が同じ最終結果を生みうる。
-/
def HistoryLoss : Prop :=
  ∃ (ops₁ ops₂ : List M.Op) (s : S),
    ops₁ ≠ ops₂ ∧ M.run ops₁ s = M.run ops₂ s

section ConcreteHistoryLoss

/-- 2セルメモリ。 -/
structure Mem2 where
  cell0 : Nat
  cell1 : Nat
deriving DecidableEq, Repr

/-- 2セルメモリへの操作。 -/
inductive Mem2Op where
  | write0 (val : Nat)
  | write1 (val : Nat)
deriving DecidableEq, Repr

/-- 操作の意味論。 -/
def mem2Step : Mem2Op → TxnK Mem2 CrudErr
  | .write0 v => fun s => .ok { s with cell0 := v }
  | .write1 v => fun s => .ok { s with cell1 := v }

/-- 具体モデル。 -/
def mem2Model : CRUDModel Mem2 where
  Op := Mem2Op
  step := mem2Step
  inv := fun _ => True
  relationTags := []
  constraints := []

/--
2セルメモリは履歴が消える:
`write0 1; write0 2` と `write0 2` は同じ最終状態を生む。
-/
theorem mem2_historyLoss : mem2Model.HistoryLoss := by
  refine ⟨[.write0 1, .write0 2], [.write0 2], { cell0 := 0, cell1 := 0 }, ?_, ?_⟩
  · intro h
    cases h
  · rfl

end ConcreteHistoryLoss

end CRUDModel
end AcidLean.Part2

Saga.lean

namespace AcidLean.Part2

universe u v

/-- Saga の固有故障モード。 -/
inductive SagaFault where
  | forwardFailure
  | compensationFailure
deriving DecidableEq, Repr

/-- Saga の1ステップ（前進操作と補償操作）。 -/
structure SagaStep (S : Type u) (Err : Type v) where
  forward : S → Except Err S
  compensate : S → Except Err S

/-- Saga の最小モデル。 -/
structure SagaModel (S : Type u) (Err : Type v) where
  steps : List (SagaStep S Err)
  inv : S → Prop

namespace SagaStep

variable {S : Type u} {Err : Type v}

/-- ステップの前進実行。 -/
def runForward (st : SagaStep S Err) (s : S) : Except Err S :=
  st.forward s

/-- ステップの補償実行。 -/
def runCompensate (st : SagaStep S Err) (s : S) : Except Err S :=
  st.compensate s

/-- 片側補償条件（観測同値 `Obs` に関して）。 -/
def LeftInverseUpTo (Obs : S → S → Prop) (st : SagaStep S Err) : Prop :=
  ∀ s s', st.forward s = .ok s' → ∃ s'', st.compensate s' = .ok s'' ∧ Obs s'' s

/-- Saga 固有の故障: 前進後に補償が失敗する。 -/
def CompensationFailure (st : SagaStep S Err) : Prop :=
  ∃ s s', st.forward s = .ok s' ∧
    ∀ s'', st.compensate s' ≠ .ok s''

/--
補償は成功するが、観測同値に戻らない故障。
（返金成功だが手数料が残る等）
-/
def CompensationDrift (Obs : S → S → Prop) (st : SagaStep S Err) : Prop :=
  ∃ s s' s'', st.forward s = .ok s' ∧
    st.compensate s' = .ok s'' ∧
    ¬ Obs s'' s

/-- ある開始状態・前進後状態を固定した補償失敗。 -/
def CompensationFailureAt (st : SagaStep S Err) (s s' : S) : Prop :=
  st.forward s = .ok s' ∧ ∀ s'', st.compensate s' ≠ .ok s''

/-- ある開始状態・前進後状態を固定した補償ドリフト。 -/
def CompensationDriftAt (Obs : S → S → Prop) (st : SagaStep S Err) (s s' : S) : Prop :=
  st.forward s = .ok s' ∧ ∃ s'', st.compensate s' = .ok s'' ∧ ¬ Obs s'' s

theorem failureAt_and_driftAt_exclusive
    (Obs : S → S → Prop) (st : SagaStep S Err) (s s' : S) :
    CompensationFailureAt st s s' →
    ¬ CompensationDriftAt Obs st s s' := by
  intro hFail hDrift
  rcases hFail with ⟨_, hcompFail⟩
  rcases hDrift with ⟨_, s'', hcompOk, _⟩
  exact hcompFail s'' hcompOk

end SagaStep
end AcidLean.Part2

Lattice.lean

namespace AcidLean.Part2

universe u

/-- 第2部比較で使う故障カテゴリ。 -/
inductive FailureMode where
  | externalCorruption
  | semanticsBug
  | invariantViolation
  | compensationFailure
  | compensationDrift
  | fusedFailure
deriving DecidableEq, Repr

/--
第2部の三者比較を載せる抽象点。
- `relationComplexity`: 関係式の強さ（大きいほど制約が多い）
- `modes`: 想定される故障モード
-/
structure ArchitecturePoint where
  relationComplexity : Nat
  modes : FailureMode → Prop

/-- 格子上の順序（制約が弱く、故障モードが少ないほど下位）。 -/
def ArchitecturePoint.LE (a b : ArchitecturePoint) : Prop :=
  a.relationComplexity ≤ b.relationComplexity ∧
    ∀ m, a.modes m → b.modes m

instance : LE ArchitecturePoint := ⟨ArchitecturePoint.LE⟩

theorem le_refl (a : ArchitecturePoint) : a ≤ a := by
  exact ⟨Nat.le_refl _, fun _ hm => hm⟩

theorem le_trans {a b c : ArchitecturePoint} :
    a ≤ b → b ≤ c → a ≤ c := by
  intro hab hbc
  refine ⟨Nat.le_trans hab.1 hbc.1, ?_⟩
  intro m hm
  exact hbc.2 m (hab.2 m hm)

/-- Event Sourcing: 最大自由度（関係式ほぼなし）。 -/
def eventSourcingPoint : ArchitecturePoint where
  relationComplexity := 0
  modes := fun m => m = .externalCorruption ∨ m = .semanticsBug ∨ m = .invariantViolation

/-- Saga: 観測商上の近似逆元を持つ中間点。 -/
def sagaPoint : ArchitecturePoint where
  relationComplexity := 1
  modes := fun m =>
    m = .externalCorruption ∨
    m = .semanticsBug ∨
    m = .invariantViolation ∨
    m = .compensationFailure ∨
    m = .compensationDrift

/-- CRUD: 強い関係式を持つ高制約点。 -/
def crudPoint : ArchitecturePoint where
  relationComplexity := 2
  modes := fun m =>
    m = .externalCorruption ∨
    m = .semanticsBug ∨
    m = .invariantViolation ∨
    m = .compensationFailure ∨
    m = .compensationDrift ∨
    m = .fusedFailure

/--
比較原理（弱形式）:
関係式複雑性が上がるほど、潜在故障モードは増えうる。
ここでは `ArchitecturePoint` の順序として明示する。
-/
theorem modes_monotone_of_le {a b : ArchitecturePoint} (h : a ≤ b) :
    ∀ m, a.modes m → b.modes m := h.2

theorem eventSourcing_le_saga : eventSourcingPoint ≤ sagaPoint := by
  refine ⟨by decide, ?_⟩
  intro m hm
  rcases hm with hm | hm | hm
  · exact Or.inl hm
  · exact Or.inr (Or.inl hm)
  · exact Or.inr (Or.inr (Or.inl hm))

theorem saga_le_crud : sagaPoint ≤ crudPoint := by
  refine ⟨by decide, ?_⟩
  intro m hm
  rcases hm with hm | hm | hm | hm | hm
  · exact Or.inl hm
  · exact Or.inr (Or.inl hm)
  · exact Or.inr (Or.inr (Or.inl hm))
  · exact Or.inr (Or.inr (Or.inr (Or.inl hm)))
  · exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inl hm))))

/-- 関係式増加に伴う故障モード包含（ES ≤ Saga ≤ CRUD）。 -/
theorem relation_increase_implies_modes_monotone :
    (∀ m, eventSourcingPoint.modes m → sagaPoint.modes m) ∧
    (∀ m, sagaPoint.modes m → crudPoint.modes m) := by
  exact ⟨modes_monotone_of_le eventSourcing_le_saga,
    modes_monotone_of_le saga_le_crud⟩

end AcidLean.Part2

8. 次回予告

第2部では三者を「同じ代数的言語」で記述し、格子構造を証明しました。でもまだ大きな問題が残っています。

Sagaの補償条件 LeftInverseUpTo で使った Obs（観測同値）はまだ抽象的なパラメータです。これを不変量 P から導出されるP-観測同値として具体化し、その上で商モノイドを構成すると、Sagaの補償条件が商モノイド上の等式として再定式化できます。

さらに、CRUDのカスケード故障とSagaの補償故障が依存グラフの反転を通じて一対一に対応するという移送定理——これが次回の核心です。

第1部の反単調性定理が「弱いほど壊れにくい」の一般論を与え、第2部の格子構造が「三者の比較」を与えた。次回は「CRUDの壊れ方とSagaの壊れ方が構造的に対応する」という、より深い関係に踏み込みます。