第26章
Schorr–Waite のアルゴリズム
（やさしい版）
Pearls of Functional Algorithm Design（関数プログラミングによるアルゴリズム設計の真珠）
どんな問題？
コンピュータのメモリの中には、あちこちが「ポインタ（矢印）」でつながったデータがたくさんあります。ガーベジコレクション（不要領域の回収）などでは、「ある出発点のノードから、矢印をたどって到達できるノードすべてに印を付けたい」という場面がよく出てきます。
ふつうにやるなら、深さ優先探索（DFS）を スタック（訪問予定のノードを積んでおく箱）を使って行います。ところが、大きなグラフになるとこのスタック自体が大量のメモリを消費してしまいます。
この章のテーマ
Schorr–Waite（シャー–ウェイト）のアルゴリズムは、追加のスタックを一切使わずにグラフのマーキングを行う、非常に有名で「ちょっと難しい」アルゴリズムです。トリックは、グラフの矢印を一時的に付け替えることで、スタックの役割をグラフ自身に肩代わりさせることにあります。処理が終わる頃には、グラフはちゃんと元通りに戻っています。
本章のねらいは、この難物アルゴリズムを、単純な版から出発して段階的に変換していくことで導き出すことです。3 段階の書き換えを経て、最終形にたどり着きます。
- スタート地点：ふつうのスタック版 DFS
- 変換1：スタックから重複要素をなくす
- 変換2：スタックを「グラフの辺でつなぐ」（スレッド化）
- 変換3：スタックをグラフの中に埋め込む（連結リスト化）
問題の設定
グラフの型と操作
グラフは 出次数が 2（各ノードから外に出る矢印がちょうど 2 本）に限定します。ノードは正の整数で表し、次のような型で表現します。
type Node = Int
type Graph = Node → (Node, Node)
Dart
typedef Node = int;
// グラフは「ノード → (左の子, 右の子)」の写像。
// ここでは Map で可変に持ち、setl / setr で辺を張り替える。
typedef Graph = Map<Node, (Node, Node)>;
Node left(Graph g, Node x) => g[x]!.$1;
Node right(Graph g, Node x) => g[x]!.$2;
Graph setl(Graph g, Node x, Node y) {
final (_, r) = g[x]!;
return {...g, x: (y, r)};
}
Graph setr(Graph g, Node x, Node y) {
final (l, _) = g[x]!;
return {...g, x: (l, y)};
}
グラフから情報を取り出す関数と、書き換える関数を用意します。
left g x, right g x：ノード x から出る左右の矢印の先を返す。setl g x y：ノード x の左の矢印を y に張り替える（setr は右の矢印を張り替える）。
すなわち、left (setl g x y) x = y が成り立ちます（張り替えた直後に読み出せばその値が返る、という自然な性質です）。
マーキング関数の仕様
マーキング関数 mark はグラフ g と出発ノード root を受け取り、真偽値を返す関数 m を返します。m x = True となるのは、x が root から到達可能なとき、そのときに限ります。
ただし、最終アルゴリズムでは処理の途中で g を書き換えてしまうので、後で「元と同じかどうか」を比べられるように mark は グラフと真偽値関数の両方を返す形にしておきます。
mark :: Graph → Node → (Graph, Node → Bool)
Dart
// mark はグラフと出発ノードから、書き換え後のグラフとマーク関数を返す。
typedef MarkFn = bool Function(Node);
typedef MarkResult = (Graph, MarkFn);
ポイント
各版の mark が同じ入力に対して同じ グラフ と同じ マーク関数 を返すことを示せれば、「途中でグラフを書き換えても、最後にはちゃんと元に戻っている」ことも同時に保証できます。
出発点：ふつうのスタック版 DFS
まずは、ごく普通のスタックベース深さ優先探索から始めます。
mark g root = seek0 (g, const False) [root]
seek0 (g, m) [ ] = (g, m)
seek0 (g, m) (x : xs)
| not (m x) = seek0 (g, set m x) (left g x : right g x : xs)
| otherwise = seek0 (g, m) xs
Dart
// 出発点：ふつうのスタック版 DFS。
MarkResult mark0(Graph g, Node root) => seek0(g, (Node _) => false, [root]);
MarkResult seek0(Graph g, MarkFn m, List<Node> stack) {
var mm = m;
var st = [...stack];
while (st.isNotEmpty) {
final x = st.removeLast(); // 末尾をスタック先頭とみなす
if (!mm(x)) {
mm = setMark(mm, x);
// left, right を push（left が先に取り出されるよう後に積む）
st.add(right(g, x));
st.add(left(g, x));
}
}
return (g, mm);
}
スタックの先頭 x がまだ未マークなら、マークを付けて左右の子をスタックに積む。すでにマーク済みなら捨てる。それだけの単純な仕組みです。set と unset は、あるノードだけ True / False に書き換える補助関数です。
set, unset :: (Node → Bool) → Node → (Node → Bool)
set f x = λy → if y == x then True else f y
unset f x = λy → if y == x then False else f y
Dart
// あるノード x だけ True / False に書き換えた新しい関数を返す。
MarkFn setMark(MarkFn f, Node x) => (Node y) => y == x ? true : f(y);
MarkFn unsetMark(MarkFn f, Node x) => (Node y) => y == x ? false : f(y);
準備：安全な置換
これから何度も使うことになる小さな道具を紹介しておきます。安全な置換（safe replacement）とは、「関数 f の x における値だけをこっそり書き換えたけれど、実は結果に影響しない」という状況のことです。
replace :: Eq a ⇒ (a → b) → a → b → (a → b)
replace f x y = λz → if z == x then y else f z
Dart
// f の x における値だけを y に差し替える汎用ヘルパ。
B Function(A) replace<A, B>(B Function(A) f, A x, B y) =>
(A z) => z == x ? y : f(z);
たとえば次の等式は、リスト xs に x が入っていないときに成り立ちます。
map f xs = map (replace f x y) xs
filter p xs = filter (replace p x y) xs
なぜ大事？
「x は今このリストには出てこないから、f の x における値を好きに変えても map や filter の結果は変わらない」というのが安全な置換です。以降の計算では、この事実を 「安全な置換」 というヒントとともに何度も使います。
変換1：スタックから重複をなくす
ねらい
seek0 のスタックには、まだ処理していないノードが並んでいます。ここにすでにマーク済みのノードだけを載せるように改造すると、同じノードが 2 度以上載ることがなくなります。これは後の変換の下ごしらえです。
新しい関数 seek1 を、次のような関係で定義します。
seek1 (g, m) x xs = seek0 (g, m) (x : map (right g) xs)
そして次の不変条件が成り立つとします。
- xs の要素はすべてマーク済み（all m xs）
- xs に重複はない（nodups xs）
これを clean（きれい）な状態と呼びます。直接的な定義を導くと、次のようになります。
mark g root = seek1 (g, const False) root [ ]
seek1 (g, m) x xs
| not (m x) = seek1 (g, set m x) (left g x) (x : xs)
| null xs = (g, m)
| otherwise = seek1 (g, m) (right g (head xs)) (tail xs)
Dart
// スタックにはマーク済みノードだけを載せる版。重複が生じない。
MarkResult mark1(Graph g, Node root) =>
seek1(g, (Node _) => false, root, const []);
MarkResult seek1(Graph g, MarkFn m, Node x, List<Node> xs) {
var mm = m;
var cur = x;
var st = [...xs]; // 先頭が xs の先頭
while (true) {
if (!mm(cur)) {
mm = setMark(mm, cur);
st.insert(0, cur); // x を先頭に積む
cur = left(g, cur); // 左の子へ
} else if (st.isEmpty) {
return (g, mm);
} else {
final head = st.removeAt(0);
cur = right(g, head); // 親の右の子へ
}
}
}
動きのポイント
- x が未マークなら、x にマークして x をスタックの先頭に積み、次に 左の子 を見に行く。
- x がマーク済み（＝左側を探索し終えて戻ってきた）なら、スタック先頭のノード（親）の 右の子 を見に行く。
x がスタックに積まれるのはマークされた瞬間だけなので、同じノードは決して 2 度スタックに乗りません。
変換2：スタックを「グラフの辺でつなぐ」
スレッド化とは？
次の狙いは、スタックの中身を グラフの辺そのもので表現できるようにすることです。それには、スタックが次の条件（threaded：スレッド化）を満たしていてほしい。
スレッド化の条件
スタックの隣り合う 2 要素 x, y（x が上、y がその下）について、必ず
「x = left g y」もしくは「x = right g y」
のどちらかが成り立つ。つまり、スタック上で隣接するノードは グラフ上でも親子関係にある。
問題点と解決策
ところが seek1 だと、たとえば「親 x の左の子が終わって、右の子に進む」タイミングで、スタック先頭の x が right g x に置き換わってしまい、下の要素との親子関係が壊れることがあります。
そこで、2 つ目のマーキング関数 p を導入します。p x はこの x について「今、左の子を探索中か（True）、それとも右の子まで進んだか（False）」を覚えておく目印です。x をスタックに残しつつ、その状態を p で管理する、というアイデアです。
seek2 (g, m) p x xs = seek1 (g, m) x (filter p xs)
不変条件は threaded g m p x xs：
threaded g m p x xs = clean m xs ∧
and [link u v | (u, v) ← zip (x : xs) xs]
where link u v = if p v then u = left g v else u = right g v
Dart
// スレッド化条件：clean（マーク済み・重複なし）かつ隣接ノードが親子関係。
bool clean(MarkFn m, List<Node> xs) =>
xs.every(m) && xs.toSet().length == xs.length;
bool threaded(Graph g, MarkFn m, MarkFn p, Node x, List<Node> xs) {
if (!clean(m, xs)) return false;
final zipped = [x, ...xs];
for (var i = 0; i < xs.length; i++) {
final u = zipped[i], v = xs[i];
final ok = p(v) ? (u == left(g, v)) : (u == right(g, v));
if (!ok) return false;
}
return true;
}
また、以下の「スレッド性」の事実を後で使います：m x かつ x ∉ xs なら、
threaded g m p x xs ⇒ threaded g m (set p x) (left g x) (x : xs) ∧
threaded g m (unset p x) (right g x) (x : xs)
seek2 の直接定義を導く
初期呼び出しは mark g x = seek2 (g, const False) (const False) x [ ] とすればよいので、あとは seek2 の直接的な計算式を求めます。not (m x) の場合を計算すると：
seek2 (g, m) p x xs
= {定義}
seek1 (g, m) x (filter p xs)
= {場合分けの仮定 not (m x)}
seek1 (g, set m x) (left g x) (x : filter p xs)
= {安全な置換：x ∉ xs ゆえ}
seek1 (g, set m x) (left g x) (x : filter (set p x) xs)
= {set p x x = True ゆえ}
seek1 (g, set m x) (left g x) (filter (set p x) (x : xs))
= {seek2 の定義とスレッド性}
seek2 (g, set m x) (set p x) (left g x) (x : xs)
m x の場合には、次に処理すべきノード（p を満たすスタック中の先頭）を探す必要があります。これを find2 という関数として切り出します。
find2 (g, m) p xs = seek1 (g, m) x (filter p xs)
場合分けで直接定義を作ると：
- 空リストなら find2 (g, m) p [ ] = (g, m)。
- xs = y : ys かつ not (p y) なら、単に先頭を捨てて find2 (g, m) p ys。
- p y の場合は、安全な置換と seek2 の定義から seek2 に戻る。
まとめると次のようになります。
mark g root = seek2 (g, const False) (const False) root [ ]
seek2 (g, m) p x xs
| not (m x) = seek2 (g, set m x) (set p x) (left g x) (x : xs)
| otherwise = find2 (g, m) p xs
find2 (g, m) p [ ] = (g, m)
find2 (g, m) p (y : ys)
| not (p y) = find2 (g, m) p ys
| otherwise = seek2 (g, m) (unset p y) (right g y) (y : ys)
Dart
// p は「今 x について左の子を探索中か？」を覚える 2 つ目のマーク。
// スタックはノードそのものを保持し、状態を p で区別する。
MarkResult mark2(Graph g, Node root) => seek2(
g, (Node _) => false, (Node _) => false, root, const [],
);
MarkResult seek2(
Graph g, MarkFn m, MarkFn p, Node x, List<Node> xs) {
if (!m(x)) {
return seek2(g, setMark(m, x), setMark(p, x), left(g, x), [x, ...xs]);
}
return find2(g, m, p, xs);
}
MarkResult find2(Graph g, MarkFn m, MarkFn p, List<Node> xs) {
if (xs.isEmpty) return (g, m);
final y = xs.first;
final ys = xs.sublist(1);
if (!p(y)) return find2(g, m, p, ys);
return seek2(g, m, unsetMark(p, y), right(g, y), [y, ...ys]);
}
ここまでの成果
seek2 と find2 はどちらも 末尾再帰 なので、単純な while ループとして手続き型で書けます。しかも、スタックは常にスレッド化されている（＝グラフの辺だけをたどれば下のノードに行ける）ので、いよいよ次で「スタックそのものをグラフに埋め込む」準備が整いました。
変換3：スタックをグラフに埋め込む
アイデア
Schorr と Waite のトリックは、スタックのつながりをグラフの辺自体に格納することです。スタックの隣接関係はスレッド化のおかげで「親子関係」になっているので、その辺を一時的に逆向きにして「下向きのリンク」として使えばよい、というわけです。
結果
実行速度は元と同じですが、スタック用の追加メモリがゼロになります。各ノードにつき必要な追加情報は、マークビット m と目印 p の 2 ビットだけです。
抽象化関数 stack と復元関数 restore
まず、グラフの中に埋め込まれたリンクから本来のスタックを取り出す関数 stack を定義します。特別なノード 0 が「リストの終わり」を表します。
stack :: Graph → (Node → Bool) → Node → [Node]
stack g p x | x == 0 = [ ]
| p x = x : stack g p (left g x)
| not (p x) = x : stack g p (right g x)
Dart
// グラフの辺に埋め込まれた「スタック」を x から辿って取り出す。
// 特別なノード 0 が末尾を表す。
List<Node> stackOf(Graph g, MarkFn p, Node x) {
final result = <Node>[];
var cur = x;
while (cur != 0) {
result.add(cur);
cur = p(cur) ? left(g, cur) : right(g, cur);
}
return result;
}
次に、スタックに新しいノード x ≠ 0 を積む操作は、グラフ側では次の式で表せます（あとで大活躍する等式です）。
x : stack g p y = stack (setl g x y) (set p x) x (26.1)
また、マーキングが終わったあとにグラフを元通りに戻すための関数 restore も用意します。
restore :: Graph → (Node → Bool) → Node → [Node] → Graph
restore g p x [ ] = g
restore g p x (y : ys) | p y = restore (setl g y x) p y ys
| not (p y) = restore (setr g y x) p y ys
Dart
// スタック xs を辿って、書き換えた辺を元に戻す。
Graph restore(Graph g, MarkFn p, Node x, List<Node> xs) {
var gg = g;
var prev = x;
for (final y in xs) {
gg = p(y) ? setl(gg, y, prev) : setr(gg, y, prev);
prev = y;
}
return gg;
}
stack と restore を使えば、seek3 と find3 は次のように「グラフ埋め込み版」として定義できます。
seek3 (g, m) p x y = seek2 (restore g p x xs, m) p x xs
where xs = stack g p y
find3 (g, m) p x y = find2 (restore g p x xs, m) p xs
where xs = stack g p y
初期化と seek3 の直接定義
restore g p x [ ] = g という性質から、初期呼び出しは次のようにまとまります。
mark g root = seek3 (g, const False) (const False) root 0
次に、seek3 の直接定義を場合分けで作っていきます。not (m x) の場合の計算は、xs = stack g p y、g′ = restore g p x xs と略記して：
seek3 (g, m) p x y
= {上記の略記}
seek2 (g′, m) p x xs
= {場合 not (m x)}
seek2 (g′, set m x) (set p x) (left g′ x) (x : xs)
= {安全な置換：x ∉ xs ゆえ}
seek2 (g′, set m x) (set p x) (left g x) (x : xs)
= {主張：後述}
seek2 (restore (setl g x y) (set p x) (left g x) (x : xs), set m x)
(set p x) (left g x) (x : xs)
= {(26.1) と seek3 の定義}
seek3 (setl g x y, set m x) (set p x) (left g x) x
途中で使った「主張」は次の等式です。証明は restore の定義を 1 段展開し、setl の性質と安全な置換を使うだけです（詳細は原文参照）。
restore g p x xs = restore (setl g x y) (set p x) (left g x) (x : xs)
m x の場合は素直に find3 に落ちます。
seek3 (g, m) p x y
= seek2 (g′, m) p x xs
= {場合 m x}
find2 (g′, m) p xs
= find3 (g, m) p x y
find3 の場合分け
find3 も 3 つの場合に分けて計算します。
- y = 0（スタックが尽きた）：処理終了。find3 (g, m) p x 0 = (g, m)。
- y ≠ 0 かつ not (p y)（右の子から戻ってきた）：この y はもう処理し尽くしたので、さらに親へ戻る。
- y ≠ 0 かつ p y（左の子から戻ってきた）：右の子へ探索を進める。最も込み入った場合。
2 番目の場合の計算は次のとおり（ys = stack g p (right g y) と略記）：
find3 (g, m) p x y
= find2 (restore g p x (y : ys), m) p (y : ys)
= {not (p y) の場合の restore}
find2 (restore (setr g y x) p y ys, m) p (y : ys)
= {not (p y) の場合の find2}
find2 (restore (setr g y x) p y ys, m) p ys
= {安全な置換}
find3 (setr g y x, m) p y (right g y)
3 番目（最も面白いケース）では、「一時変数 swing g y x」を導入します。これは y の左右のリンクを組み替えて、探索を左から右へ切り替える働きをします。
swing g y x = setr (setl g y x) y (left g y)
Dart
// y の左右のリンクを組み替え、探索を「左から右」へ切り替える。
Graph swing(Graph g, Node y, Node x) => setr(setl(g, y, x), y, left(g, y));
計算の結果、次が得られます。
find3 (g, m) p x y = seek3 (swing g y x, m) (unset p y) (right g y) y
最終形（Schorr–Waite のアルゴリズム）
すべてを合わせると、これが Schorr–Waite のマーキング・アルゴリズムです。
mark g root = seek3 (g, const False) (const False) root 0
seek3 (g, m) p x y
| not (m x) = seek3 (setl g x y, set m x) (set p x) (left g x) x
| otherwise = find3 (g, m) p x y
find3 (g, m) p x y
| y == 0 = (g, m)
| p y = seek3 (swing g y x, m) (unset p y) (right g y) y
| otherwise = find3 (setr g y x, m) p y (right g y)
where swing g y x = setr (setl g y x) y (left g y)
Dart
// Schorr–Waite の最終形：スタックをグラフの辺に埋め込む。
// 追加メモリは各ノードあたり m と p の 2 ビットだけ。
MarkResult mark3(Graph g, Node root) => seek3(
g, (Node _) => false, (Node _) => false, root, 0,
);
MarkResult seek3(Graph g, MarkFn m, MarkFn p, Node x, Node y) {
if (!m(x)) {
// 新しいノード x：辺を y へ逆向けにし、左の子へ潜る。
return seek3(
setl(g, x, y), setMark(m, x), setMark(p, x), left(g, x), x,
);
}
return find3(g, m, p, x, y);
}
MarkResult find3(Graph g, MarkFn m, MarkFn p, Node x, Node y) {
if (y == 0) return (g, m);
if (p(y)) {
// 左の子から戻ってきた：右の子へ進む（swing で辺を組み替え）。
return seek3(swing(g, y, x), m, unsetMark(p, y), right(g, y), y);
}
// 右の子から戻ってきた：辺を復元してさらに親へ。
return find3(setr(g, y, x), m, p, y, right(g, y));
}
動きのイメージ
- seek3 は「新しいノード x の探索を始める」フェーズ。未マークならマークして左の子へ潜っていく。
- find3 は「子から戻ってきた後、次に何を見るか」を決めるフェーズ。p y なら右の子へ進み、そうでなければさらに親へ戻る。
- グラフの辺を setl / setr で書き換えているが、戻ってきた時にはちゃんと元の値が復元される。
Dart
// 動作確認：小さなグラフでマーキング（0 は「終端」用の予約ノード）。
//
// 1
// / \
// 2 3
// / \ / \
// 4 5 5 0 (5 は 2 と 3 の共通の子、右子が 0 のノードは葉扱い)
//
void main() {
final g = <Node, (Node, Node)>{
1: (2, 3),
2: (4, 5),
3: (5, 0),
4: (0, 0),
5: (0, 0),
};
final (g2, m) = mark3({...g}, 1);
final reached = [1, 2, 3, 4, 5].where(m).toList();
print('reachable = $reached'); // reachable = [1, 2, 3, 4, 5]
// グラフが元通りに復元されていることを確認。
print('restored = ${g2.toString() == g.toString()}'); // restored = true
}
結び
Schorr–Waite のアルゴリズムは Schorr and Waite (1967) が最初に提案しました。以来、ループ不変条件による正当性証明（Bornat, Butler, Gries, Morris, Topor など）、関係代数を用いた証明（Möller）、可変な更新関数を使った証明（Mason）など、多くの研究がなされてきました。最近では分離論理（separation logic）を用いた O’Hearn らのアプローチもあります。
本章のように「単純な版から段階的に変換していく」やり方は、詳細で少し骨は折れるものの、各ステップに明確な動機があり、順を追えば理解できるという利点があります。これがこの難物アルゴリズムを説明する一つの良い方法である、というのが著者の主張です。
参考文献
Bornat, R. (2000). Proving pointer programs in Hoare logic. LNCS 1837: 5th Mathematics of Program Construction Conference, pp. 102–26.
Butler, M. (1999). Calculational derivation of pointer algorithms from tree operations. Science of Computer Programming 33 (3), 221–60.
Gries, D. (1979). The Schorr–Waite graph marking algorithm. Acta Informatica 11, 223–32.
McCarthy, J. (1960). Recursive functions of symbolic expressions and their computation by machine. Communications of the ACM 3, 184.
Mason, I. A. (1988). Verification of programs that destructively manipulate data. Science of Computer Programming 10 (2), 177–210.
Möller, B. (1997). Calculating with pointer structures. IFIP TC2/WG2.1 Working Conference on Algorithmic Languages and Calculi. Chapman and Hall, pp. 24–48.
Möller, B. (1999). Calculating with acyclic and cyclic lists. Information Sciences 119, 135–54.
Morris, J. M. (1982). A proof of the Schorr–Waite algorithm. Proceedings of the 1981 Marktoberdorf Summer School, ed. M. Broy and G. Schmidt. Reidel, pp. 25–51.
O’Hearn, P. W., Yang, H. and Reynolds, J. C. (2004). Separation and information hiding. 31st Principles of Programming Languages Conference. ACM Publications, pp. 268–80.
Schorr, H. and Waite, W. M. (1967). An efficient machine-independent procedure for garbage collection in various list structures. Communications of the ACM 10, 501–6.
Topor, R. W. (1979). The correctness of the Schorr–Waite marking algorithm. Acta Informatica 11, 211–21.