情報科学 › ソフトウェア開発 › バージョン管理システム Git

ハッシュによる履歴全体の同定

定理 3.3（「バージョン管理システム Git」§3） ・ ✓公理まで証明済み

オブジェクトの有限集合 OO と O′O' を考える（例えば手元のクローンと相手のリポジトリ）。各オブジェクト oo はその直列化 σ(o)\sigma(o) と同一視され、σ(o)\sigma(o) は oo が参照する子オブジェクトの ID をすべて含むとする。h(o)=H(σ(o))h(o) = H(\sigma(o)) とおき、HH は {σ(o):o∈O∪O′}\{\sigma(o) : o \in O \cup O'\} 上で単射である（この集合の中に衝突が存在しない）と仮定する。oo から到達可能なオブジェクト全体を R(o)R(o) と書く。

このとき、o∈Oo \in O、o′∈O′o' \in O' に対して

h(o)=h(o′)  ⟹  R(o)=R(o′)h(o) = h(o') \;\Longrightarrow\; R(o) = R(o')

が成り立つ。すなわち、オブジェクト ID が一致すれば、そこから辿れるオブジェクトの集合とその中身は完全に一致する。

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

閉包の状態

✓ 公理まで証明済み

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

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

前提をたどる 証明が使う定理・定義

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

これを使っている定理

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

関連するノック 3 問