単一化器: do_unify()

単一化器do_unify()のアルゴリズムについて解説する。

do_unify()のインターフェースは以下のようになっている。

q *do_unify(allocp, x, y)
     q * allocp;
     q x, y;

x, y は単一化対象である項であり、allocpはヒープ割付点のアドレスである。 単一化後、更新されたヒープ割付点のアドレスが返される。

以下でアルゴリズムの説明を行う。

1.

片方の項 x を手繰りつつ型検査を行う。

• x が二重ループであることがわかれば、もう一方の項 y を手繰り、 一重ループかどうか検査する。一重ループであれば、yを具体化して終了。

  • y も二重ループであれば、

    (a)

    x とyが同一でなければ、xがgeneratorであるかどうか検査する (is_generator_suspで検査する)。generatorであれば、 generator_unify()を実行する。 y がgeneratorであれば、その逆。

    (b)

    x, y が共にgeneratorでなければ、共にgoal/consumer ゴールであることが判明するので双方をmergeし終了。 このマージについては、suspendしているゴール群の数に関係なく、 一定コストで行われるように工夫がなされている(ページ、第5.1章参照)。

    
    

      

    Figure 5.1: ゴールチェーンのmerge

    
    
    

  • y が二重ループではない場合には、具体値であることが判明したので x を待つゴールを再開する(resume_goals())。

• xが一重ループであることがわかれば、y が具体値、または一/二重ループ であることがわかるまで手繰りxを具体化する。yを手繰るのは、x と yとが実は 同じ変数である場合に、REFのループができてしまうことを防ぐため。

• x が具体値であることがわかった場合には、yを手繰る。
  • yが一重ループであれば、yをxで具体化して終了。
  • yが二重ループであることがわかれば、y を待つゴールを再開 (resume_goals()。generatorの場合もこれで良い)。
  • yが具体値であることがわかれば、xとを比較する。 同一でなければ、両者を単一化するようなゴールを割りつけ、エンキューする (enqueue_unify_goal())。 単一化を行っている間は割り込み関連の処理がまったく行われない。 何故なら、割り込み処理はゴールのリダクションの合間に行なわれるが、 単一化器のような実行時ライブラリが動作している間には リダクション操作が行われないためである。 これは、あまりに複雑な項同士を単一化する場合(特に並列実装時に) システムのレスポンスがあまりに悪くなる可能性が高いため、ある程度しか 連続して処理が行われないようにするための配慮である。

以上で述べたように、active unifierの内部では さらに副次的な処理が内部で行われる。つまり、ゴールの再開、 generatorの起動、さらに複雑な項同士の単一化である。それらの説明を以下で行う。