変成関係の検査が検出できる誤り

定理 6.2（「性質ベーステスト」§6）・ ✓公理まで証明済み

$f : X \to Y$ を関数、 $\mathcal{R}$ を $f$ の変成関係の集合とする。写像 $\tilde f : X \to Y$ のうち、 $\mathcal{R}$ のすべての関係をすべての入力で満たすものの全体を

U(\mathcal{R}) = \{\, \tilde f \mid \text{すべての } (g, h) \in \mathcal{R} \text{ と } x \in X \text{ について } \tilde f(g(x)) = h(\tilde f(x)) \,\}

とおく。

$f \in U(\mathcal{R})$ である。実装 $\tilde f$ について、 $\mathcal{R}$ の検査がある関係とある入力で不合格になることは、 $\tilde f \notin U(\mathcal{R})$ と同値である。とくに $\tilde f \in U(\mathcal{R})$ ならば、 $\tilde f \ne f$ であっても、検査の入力をどう選んでも誤りは検出されない。
$\mathcal{R} \subseteq \mathcal{R}'$ ならば $U(\mathcal{R}') \subseteq U(\mathcal{R})$ で、 $U(\mathcal{R} \cup \mathcal{R}') = U(\mathcal{R}) \cap U(\mathcal{R}')$ である。
写像 $c : Y \to Y$ が $\mathcal{R}$ のすべての $(g, h)$ について $c \circ h = h \circ c$ を満たすならば、 $c \circ f \in U(\mathcal{R})$ である。写像 $k : X \to X$ が $\mathcal{R}$ のすべての $(g, h)$ について $k \circ g = g \circ k$ を満たすならば、 $f \circ k \in U(\mathcal{R})$ である。

閉包の状態

✓ 公理まで証明済み

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

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

証明は Rikai の他の定理を参照していません（定義と論理だけで示されています）。

証明で明示的に参照している定理は、まだありません。