同値 (Material Equivalence ・ Biconditional - ↔, ⇔)

同値は二つの命題が同じ真偽値を持つことを表し、PならばQとQならばPの両方を要求する。仕様の置換可能性を示すときは便利だが、実装のコストや観測可能な副作用まで同じとは限らない。

仕組みと確認

両方向の含意を別々に証明し、変数の束縛・前提・型の違いを揃える。リファクタリングでは入力と出力だけでなく、例外、順序、性能、ログなどの契約も比較する。

限界と注意点

数学的同値と意味的同値、振る舞いの同一性を区別する。片方向の近似や互換性を同値と呼ばない。