はじめに
「単一化」とか「具体化待ち」といった機能が性能面で有利に働くことはあまりないのですが、たらい回しを例にこれらが有効に働く例を見たいと思います。
たらい回し
Guarded Horn Clauses で素直にたらい回しを書くと以下です。
tarai(X, Y, _, R) :- X =< Y | R = Y.
otherwise.
tarai(X, Y, Z, R) :- true |
X_1 := X - 1, tarai(X_1, Y, Z, R_X),
Y_1 := Y - 1, tarai(Y_1, Z, X, R_Y),
Z_1 := Z - 1, tarai(Z_1, X, Y, R_Z),
tarai(R_X, R_Y, R_Z, R).
このプログラムの意味するところは、
- 述語
tarai(X, Y, Z, R)が呼び出されます。 - X と Y 双方が具体化されているかチェックし、具体化されていれば、ガード条件
X =< Yをチェックします。
2-1.X =< Yであるならば、Y と R を単一化して終了します。 - (otherwise 処理) X と Y どちらかあるいは両方が具体化されていなければ
tarai(X, Y, Z, R)を具体化されていない X あるいは Y, あるいはその両方に具体化待ちとしてフックして終了します。フックされた場合、対象の変数に値が具体的な値が確定したときに再実行されます。 -
X =< Yでないならば
4-1.X_1 = X-1,Y_1 = Y-1,Z_1 = Z-1それぞれを計算し、
4-2. サブゴールtarai(X_1, Y, Z, R_X)、tarai(Y_1, Z, X, R_Y)、tarai(Z_1, X, Y, R_Z)を呼び出し、
4-3. その結果として得られるR_X,R_Y,R_Zをもとにサブゴールtarai(R_X, R_Y, R_Z, R)を呼び出して終了です。
マイ・GHC コンパイラでの実行結果を再掲するとこうでした：
$ \time -o /dev/stdout -f 'real:%e[sec]_user:%U[sec]_sys:%S[sec]_Memory:%M[KB]' sample/tarai 15 5 0
% 12441815848 inferences(1 times resumed), 282.006 CPU seconds (44118930.909221 Lips)
15
real:282.27[sec]_user:281.97[sec]_sys:0.03[sec]_Memory:5880[KB]
計算順序の工夫
ここで、さらに若干の工夫を考えます。
otherwise よりあとが呼ばれるのは、otherwise より前のガード条件が確実に偽であると判定できた（具体化待ちの必要なく偽と判定できた）場合に限ります。つまり、この場合 otherwise よりあとが呼ばれるときは X と Y の具体化が確認できている場合に限ります。
また、tarai/4 の最初の節を見ると、Z の値とは無関係に結果 R が決まっています。
つまり、tarai(X, Y, Z, R) の X, Y の値だけ決まったタイミングで呼び出して結果が得られればそれでよし、それでだめならば後から Z の値を指定して答えを得よう、ということが可能ならば計算量を大幅に削減できるはずです。
というわけで、記述順序を少しだけ変えてみます：
tarai(X, Y, _, R) :- X =< Y | R = Y.
otherwise.
tarai(X, Y, Z, R) :- true |
X_1 := X - 1, tarai(X_1, Y, Z, R_X),
Y_1 := Y - 1, tarai(Y_1, Z, X, R_Y),
tarai(R_X, R_Y, R_Z, R), % この行の位置をずらした
Z_1 := Z - 1, tarai(Z_1, X, Y, R_Z).
必ず必要になる R_X, R_Y の計算だけ済ませ、重要度の低い R_Z は後から計算する、という戦略です。
これを実際に行ってみると、実行時間は以下のようになりました。
$ \time -o /dev/stdout -f 'real:%e[sec]_user:%U[sec]_sys:%S[sec]_Memory:%M[KB]' sample/tarai_reordered 15 5 0
% 195114 inferences(1 times resumed), 0.008488 CPU seconds (22987040.527804 Lips)
15
Command terminated by signal 9
real:352.17[sec]_user:316.46[sec]_sys:23.92[sec]_Memory:29803404[KB]
結果の表示は実行直後に得られており、計算時間はわずか 0.008488 秒となっています。
しかし、time コマンドの出力を見てのとおり、プログラム全体の実行時間は非常に長くなり、またメモリを使いすぎて OOM Killer に KILL されています。
たらい回しの結果を可能な限り早く得る、という目的自体は達成できたのですが、これでは意味がありません。
不要な計算の抑制
必要な計算結果を得た後に計算を続けても意味がありません。計算結果を得た段階で不要な計算をストップできればよいはずです。
また、メモリを大量に使っているのは具体化待ち合わせが大量発生しているからなのですが、計算をストップできればこの無駄な待ち合わせも削減できます。
最終的に必要な結果 R と途中のサブゴールでの結果を分けて考えることにして、途中のサブゴールの値を変数 T で表すことにします。
全てのサブゴールに R （の参照）を渡しておいて、それらサブゴールは R を横目で眺めながら計算を行う、R の具体化を検知したら計算を中止する、という戦略で以下のプログラムを記述することができます：
tarai(X, Y, Z, R) :- tarai_aux(X, Y, Z, R, R).
% R は最終結果。
% T は目先のサブゴールとして得ようとしている結果。
% 最終結果 R の値が確定するまで計算を続ける
tarai_aux(X, Y, _, T, R) :- var(R), X =< Y | T = Y.
tarai_aux(X, Y, Z, T, R) :- var(R), X > Y |
X_1 := X - 1, tarai_aux(X_1, Y, Z, R_X, R),
Y_1 := Y - 1, tarai_aux(Y_1, Z, X, R_Y, R),
tarai_aux(R_X, R_Y, R_Z, T, R),
Z_1 := Z - 1, tarai_aux(Z_1, X, Y, R_Z, R).
otherwise.
tarai_aux(_, _, _, _, _).
途中結果 T の引数が増えたので内部の処理は引数が５つになります。外部からの呼び出しでの引数の数を４つのままにしておくために、内部の引数５つの処理は tarai_aux/5 にしておきます（べつに tarai/5 でもよかったのですが、名前が同じだと紛らわしいので変えました）。
tarai_aux/5 のガード部分に付け加えられた var(R) は、変数 R が未具体化状態であることをチェックする述語です。
R がまだ具体化されていないなら計算を続ける、具体化済みならなにもせず終わる（otherwise. tarai_aux(_, _, _, _, _).）、という記述になっています。
では、これで実行時間はどのように変わったでしょうか：
$ \time -o /dev/stdout -f 'real:%e[sec]_user:%U[sec]_sys:%S[sec]_Memory:%M[KB]' sample/tarai_reordered 15 5 0
% 283482 inferences(1 times resumed), 0.008393 CPU seconds (33776003.812701 Lips)
15
real:0.01[sec]_user:0.00[sec]_sys:0.00[sec]_Memory:5264[KB]
一瞬で終わります。 time コマンドで見た実行時間も 0.01 秒になりました。
通常のたらい回しで 282.006 秒かかっていたのが 0.008393 秒にまでなっているので、ざっと 3 万倍以上の高速化です。
使用メモリも普通にたらい回しを実行したときとほとんど変わりません。
まとめ
GHC の具体化待ち機能を用いて、たらい回しの実行時間を極端に短くすることができました。
ベンチマークとしては邪道（たらい回しの計算を端折っているので「たらい回さず」と言う方が正しいかも）ですが、単一化と具体化待ちの可能性を示す良い例だと思います。