第四層: 不可能性と限界の数学

連載序論はこちら。「何を諦めるか」を定理で決める層。設計の最初期に参照する価値が最も高い。

4.1 計算可能性の限界: 停止性問題と Rice の定理

概念: プログラムの自明でない意味的性質（「このコードは仕様Sを満たすか」を含む）は一般に決定不能（Rice 1953）。したがって完全自動の検証は原理的に存在せず、実務の検証はどこかで必ず妥協する: (a) 健全な過大近似——全実行を覆う代わりに偽陽性を許す（静的解析）、(b) 過小近似——見つけた反例は本物だが探索範囲外の見逃しを許す（テスト・有界検査。bound内では網羅的でも、無反例は無制限の安全を意味しない）、(c) 決定可能な断片への制限（有限モデル・制限された論理）、(d) 人間が補題・不変条件を与えて個別に証明を構築する（定理証明）。

刷新での適用: 検証計画は必ずこの四極のポートフォリオになる。「どの性質を (a)〜(d) のどれで守るか」の割当表を作ることが、検証戦略の設計そのもの。

4.2 分散合意の不可能性: FLP と CAP

概念: FLP（Fischer–Lynch–Paterson 1985）: 完全非同期システムでは、たった一つのプロセス故障の可能性があるだけで、決定的な合意アルゴリズムは存在しない。実務のタイムアウトは「部分同期」という追加仮定の購入であり、Paxos/Raftはこの仮定の上で安全性を無条件・活性を条件付きで達成する。CAP（Brewer予想、Gilbert–Lynch 2002証明）: ネットワーク分断時に一貫性と可用性は両立しない。分断は選べない（起きる）ので、実際の選択は「分断時にCを取るかAを取るか」＋「平常時にレイテンシと一貫性をどう取引するか」（PACELCによる精密化）。

刷新での適用: 「切替時に新旧どちらを正とするか」「照合不一致時に止めるか流すか」は、対象操作と障害モデルをCAPと同じ形に定義しない限り定理の直接の帰結ではないが、有用な構造的類推である。いずれにせよ技術ではなく経営判断としてあらかじめ決めておくべき項目。定理は「決めなくて済む設計は存在しない」ことを保証してくれる——これが不可能性定理の実務価値。

4.3 実現可能性と自動合成 [理論先行]

概念: LTL仕様からの実装自動合成（Pnueli–Rosner 1989）は2EXPTIME完全。一般には絶望的な計算量だが、GR(1)という制限クラスなら多項式時間で合成でき、ロボティクス・ハードウェアで実用例がある。仕様を書いた時点で「実現可能か」を検査できること自体に、合成しない場合でも価値がある——実現不能な仕様（環境の悪意ある挙動で必ず破られる仕様）を早期検出できる。

4.4 状態爆発と計算複雑性

概念: モデル検査はLTLでPSPACE完全、並行部品の積で状態空間は指数爆発する。対抗手段の系譜: 記号的モデル検査（BDD、10^20状態の壁を破った）、有界モデル検査（SMTに還元）、半順序簡約、対称性簡約、抽象化による偽反例駆動の精緻化（CEGAR）。Alloyの小スコープ仮説——「多くのバグは小さな反例を持つ」——は経験則だが、有界検査の費用対効果を正当化する実務的に重要な仮説。

刷新での適用: 「全数は無理」を前提に、どの抽象化で状態を潰すかが検証設計の中心になる。切替手順の検証なら、口座を数個・店舗を2-3個に抽象化したモデルで手順の論理だけ全数検査する、が定石（AmazonのTLA+運用もこの規模感）。

連載: システム設計と大規模刷新のための数学

1. 序論 — 地図の全体像
2. 第一層: 仕様を書くための数学
3. 第二層: 仕様と実装の関係の数学
4. 第三層: 合成の数学
5. 第四層: 不可能性と限界の数学（この記事）
6. 横断層: 検証を実行する手段の数学
7. 総括: 実績濃淡マップと大規模刷新への適用