決定論的ソフトウェアとは何か？

ソフトウェアが決定論的であるとは、同じ入力が常に同じ出力を生むことをいう。たいていそうなる、という話でも、許容誤差の範囲内という話でもない。すべての実行で、すべての機械で、厳密に一致するということだ。

形式的には、システム内のすべての関数 f について:

∀ x: f(x) = f(x)

自明に見える。しかし現代のシステムでこれを満たすものはほとんどない。

なぜ多くのシステムは決定論的でないのか

非決定性はふつう偶然に忍び込む。

• 環境的な時刻と乱数 — now()、Math.random()、シードなし UUID。
• 反復順序 — 実行やバージョンによって順序が変わるハッシュマップや集合。
• 並行性 — スケジューラ負荷によって変わるインターリーブ。
• 隠れた可変状態 — グローバル変数、キャッシュ、シングルトン、遅延初期化フィールド。
• 浮動小数点のずれ — プラットフォーム間での精度や命令選択の差異。
• 言語モデル — 分布からのサンプリングにより、呼び出しごとに出力が変わる。

個々には対処できる。しかし合わさると、「昨日は動いた」は運についての言明にすぎず、システムについての言明ではなくなる。

決定論は機能ではなく、安全性の性質である

決定論の一般的な擁護論は利便性だ。再現可能なビルド、安定したテスト、容易なデバッグ。それでは過小評価である。規制業務において決定論とは、主張を検査可能にするものだ。

• 再現性。 再現できない結果は証拠ではない。
• 監査可能性。 監査人は物語を信用する代わりに、パイプラインを再実行してダイジェストを比較できる。
• 帰属。 出力が変わったなら、原因は入力かコードの変更であり、決して「その日の運」ではない。
• 改竄検知。 記録されたダイジェストと再実行のダイジェストが一致しなければ、何かが誤っており、それが即座に分かる。

だからこそ「モデルはたいてい正しい」は決済システムを変換する根拠として受け入れられず、daitai では決定論をあれば良い性質ではなくプラットフォームの性質として扱う。

daitai における決定論の強制

決定論は慣習では生き残らない。構造的に強制されなければならない。

1. 既定で決定論的（P01）。 同じ入力、同じ出力、常に。
2. 明示的な非決定性（P02）。 乱択が本当に必要な場合は @nondeterministic で印付けし、型付けし、隔離する — 本体に隠さず、シグネチャに現す。
3. 隠れ状態なし。 値は不変であり、等価性は参照的ではなく構造的である。
4. 記録されたモデル呼び出し。 AI を用いた段は記録済みカセットからリプレイされるため、モデル呼び出しは決定論保証の外ではなく内に入る。
5. ブロッキング CI ゲート。 代数的不変条件は毎ビルドで検査される。法則が破れればビルドは失敗する。

その強制の測定結果は次のとおり。500回反復の独立した2回の実行が差異ゼロでバイト単位に同一のイベントストリームを生成。代数的不変条件はブロッキング・ゲートとして 20 件中 20 件合格。Java 等価性スイートでは JDK 17 と標準出力がバイト単位で一致。成果物は証明ページにある。

決定論と形式検証

両者は代替ではなく補完である。

決定論は安価な性質であり、かつ前提条件である。決定論がなければ、ある実行についての証明は次の実行について何も語らない。もう半分については形式検証とは何か？を参照。

自分のシステムが決定論的か確かめる方法

厳しさの順に並べた実践的な検査。

1. 同じジョブを2回走らせ、「抜き取り確認」ではなくバイト単位で差分をとる。
2. 別の機械・別の OS で走らせ、再び差分をとる。
3. 先月記録したジョブを今日再実行し、ダイジェストを比較する。
4. 意味的に順序が無関係な入力の順序を入れ替え、出力が変わらないことを確認する。

いかなる差分も指摘事項である。多くのチームは第1段階で、そもそも一度も試したことがなかったと気づく。

次に読む

• 原則 (P01–P23)
• オーケストレーション問題としての COBOL・RPG 近代化
• 証明