consistency の設計

設計目標

immut と mutable は同じ中核演算を、異なるストレージと異なるカーネルで二度実装しており、MatrixFn はそれを遅延的に三度目の実装をしています。consistency パッケージは、これらの実装が同じ数学を表していることを検査します。これにより、ユーザーは結果を変えずに表現を切り替えられ、一方のパッケージでのカーネル最適化が意味論を黙って変えてしまうこともなくなります。

数学的背景

準同型性としての一致

$\iota : \texttt{@immut.Matrix[T]} \to \texttt{@mutable.Matrix[T]}$ を、形状と要素を保つ変換とします。$\iota$ が演算 $\omega$ と可換であるとき、2 つのパッケージはその演算について一致します。

$$\iota\big(\omega_{\text{immut}}(A, B)\big) = \omega_{\text{mutable}}\big(\iota A, \iota B\big).$$

テストは両辺を共通の観測（to_array、to_2d_array、to_string）を通じて比較します。この観測は、形状がわかっている行列に対して単射です。

例ではなく法則で検査する

一致に加えて、テストは両パッケージで代数法則を検査します。単位元の法則、$(AB)^{\mathsf T} = B^{\mathsf T} A^{\mathsf T}$、積の結合律、分配律、$\operatorname{tr}(A^{\mathsf T}) = \operatorname{tr}(A)$ です。転置と積の法則には可換なスカラーが必要なので、テストでは Int を使います。

小さな整数を使う理由

すべての検査で Int を使います。整数演算はオーバーフローしても厳密な環 $\mathbb{Z}/2^{32}\mathbb{Z}$ なので、すべての法則を == でテストでき、失敗はすべて本当の不一致です。Double では、総和の順序が異なれば丸めによって正当に結果が異なり（mutable の設計 を参照）、テストには本物のバグを隠しかねない許容誤差が必要になります。プロパティベースのテストは quickcheck でランダムな $2 \times 2$ 整数行列を生成し、各サンプルで法則を検査します。

設計上の判断

独立したパッケージ

検査には immut と mutable の両方が必要ですが、どちらのパッケージも他方に依存すべきではありません。テスト専用に両方をインポートする 3 つ目のパッケージを置くことで、依存グラフをきれいに保てます。テストはホワイトボックステスト（*_wbtest.mbt）なので、修飾なしのヘルパー名を使えます。

ドキュメント化された違いもテストする

パッケージ間で意図的に異なる箇所（たとえば set は mutable では変更を行い、immut では新しい値を返す）は、テストでその違いを固定し、偶然ではなく判断として維持されるようにしています。

正しさと不変条件

このパッケージは、テストしたすべての入力について次を表明します。+、*、転置、トレース、pow、行列式（整数入力）、コンストラクタ、変換の結果が等しいこと。行列演算の半環の法則。$2 \times 0$ のような退化した形状についてドキュメント化された振る舞い。

却下した代替案

• 浮動小数点の一致テスト。 許容誤差が必要になり、意味論ではなく丸めをテストすることになります。数値精度は代わりに mutable の中でテストしています。
• 例だけをテストする。 ランダムな入力は、負の要素やゼロのように作者が思いつかなかった値での不一致を見つけます。

境界

このパッケージには公開 API がなく、利用向けに公開されてもいません。一方のパッケージにしかない数値ルーチン（逆行列、Cholesky、固有値）や性能はテストしません。