情報科学 › ソフトウェア設計とテスト › ビルドと依存関係
トポロジカル順の存在と計算
を有限の有向グラフとする。
(a) がトポロジカル順をもつことと、 が有向閉路をもたないことは同値である。
(b) 次の算法（Kahn の算法）は隣接リスト表現のもとで 時間で止まる。 が有向閉路をもたなければ全頂点を出力し、出力した順がトポロジカル順になる。有向閉路をもてば、出力されない頂点が残る。
各頂点 の計数 を入次数で初期化し、 の頂点をすべて待ち行列に入れる。待ち行列が空でないかぎり、頂点 を 1 つ取り出して出力し、 から出る各辺 について を 減らし、 になったら を待ち行列に入れる。
(c) が有向閉路をもたないとき、深さ優先探索の終了時刻 の大きい順に頂点を並べたものはトポロジカル順である。これも 時間で求まる。
閉包の状態
✓ 公理まで証明済み
証明が使う定理を 前提 としてたどると、Rikai の中の証明だけで定義・公理（物理では基本仮定）までつながっています（前提の定理類 7 件、定義なども含めて 7 件）。
印の意味: ✓公理まで証明済み ・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は 閉包の状況。
前提をたどる 証明が使う定理・定義（直接 4 件）
▸ を開くと、その項目の証明が使う前提が出ます。深い先は各項目のページでたどれます。
2 つの表現の計算量✓命題 2.6・グラフアルゴリズム
- 握手補題✓補題 2.5・グラフアルゴリズム
閉路のないグラフには入次数 0 の頂点がある✓補題 3.1・ビルドと依存関係
- 灰色頂点の構造✓補題 4.1・グラフアルゴリズム
有向閉路の検出✓定理 4.2・グラフアルゴリズム
- 灰色頂点の構造✓補題 4.1・グラフアルゴリズム
- 2 つの表現の計算量✓命題 2.6・グラフアルゴリズム（上で展開済み）
これを使っている定理 証明で参照している 1 件
- クリーンビルドの一意性✓定理 4.1・ビルドと依存関係