情報科学 › ソフトウェア設計とテスト › 事例研究

根拠のある命題の集合は最小不動点である

定理 4.3（「事例研究」§4） ・ ✓公理まで証明済み

写像 Φ:2N→2N\Phi : 2^{N} \to 2^{N} を

Φ(X)=B∪{ s∈P:prem(s)⊆X }\Phi(X) = B \cup \{\, s \in P : \mathrm{prem}(s) \subseteq X \,\}

で定める（「前提がすべて XX に属するなら、結論を加える」）。

(a) Φ\Phi は単調である。すなわち X⊆YX \subseteq Y ならば Φ(X)⊆Φ(Y)\Phi(X) \subseteq \Phi(Y)。

(b) X0=∅X_0 = \emptyset、Xk+1=Φ(Xk)X_{k+1} = \Phi(X_k) とおくと、X0⊆X1⊆X2⊆⋯X_0 \subseteq X_1 \subseteq X_2 \subseteq \cdots で、ある k≤∣N∣k \le |N| で Xk+1=XkX_{k+1} = X_k となる。この XkX_k を X∗X^{*} と書くと、X∗X^{*} は Φ\Phi の最小不動点である。

(c) X∗=Gr(K)X^{*} = \mathrm{Gr}(K)。

本文で読む（証明と前後の説明）→

閉包の状態

✓ 公理まで証明済み

証明が使う定理を 前提 としてたどると、Rikai の中の証明だけで定義・公理（物理では基本仮定）までつながっています（前提の定理類 4 件、定義なども含めて 5 件）。

印の意味: ✓公理まで証明済み ・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は 閉包の状況。

前提をたどる 証明が使う定理・定義（直接 3 件）

▸ を開くと、その項目の証明が使う前提が出ます。深い先は各項目のページでたどれます。

これを使っている定理 証明で参照している 2 件

関連するノック 1 問