12.96 util.unification - ユニフィケーション ¶

Module: util.unification ¶

ユニフィケーションのアルゴリズムを実装します。

基本APIは、抽象的な木に対して動作しますが、木が実際にどう実装されているかは 関知しません。 呼び出し側は、ユニファイする木といっしょに、比較器や操作手続きを渡します。

抽象的な木は、次の構造を持っていると考えます。

Tree : Variable | Value | Tuple
Tuple : { Tree ... }

ここで、{...}は単に木の並びを表します。

変数(Variable)は木に束縛されます。値(Value)はそれ自身とのみマッチします。

この木を扱うために、APIは以下の比較器と手続きを引数として取ります。

Variable comparator: var-cmpr

要素が変数であるかどうかを調べ、また二つの変数が同じかどうかを判定 するための比較器です。ハッシュ可能でなければなりません。 比較器については基本的な比較器を参照してください。

Value comparator: val-cmpr

要素が値であるかどうかを調べ、また二つの値が等しいかどうかを 判定するための比較器です。var-cmprもval-cmprも 満たさない要素はタプルであるとみなされます。

Tuple folder: tuple-fold

(tuple-folde proc seed tuple1 [tuple2])の形で呼び出される手続きです。 この手続きは、タプル中の要素についてfoldのように動作します (リストをたどる手続き参照)。常にひとつかふたつのタプルを引数とします。

Tuple constructor: make-tuple

(make-tuple proto elements)の形式で呼び出される手続きです。 protoはタプルで、elementsは木のリストです。 protoと同じ型のタプルで、要素だけをelementsと置き換えた 新たなタプルを作成して返します。 unifyはこの手続きを必要としません。

Function: unify a b var-cmpr val-cmpr tuple-fold ¶

{util.unification} 二つの木、aとbを単一化し、置換辞書を返します。 置換辞書は、変数をその値にマップするものです。

引数var-cmpr、val-cmpr、tuple-foldに関しては 上のutil.unificationの説明を参照してください。

(dict->alist (unify '(a 3 (c b)) '(c b (2 e))
                    symbol-comparator
                    number-comparator
                    fold))
 ⇒ ((e . 3) (a . c) (b . 3) (c . 2))

この例にも見られるように、一つの変数の値が別の変数であったり、 別の変数を含む木であったりする場合があります。 元の木に置換を適用する場合は、辞書にある変数がすべて消去されるまで 再帰的に置換を行う必要があります。

二つの木が単一化できない場合は#fが返されます。

(unify '(a (a)) '(x x) symbol-comparator number-comparator fold)
 ⇒ #f

Function: unify-merge a b var-cmpr val-cmpr tuple-fold make-tuple ¶

{util.unification} 二つの木、aとbを単一化し、結果の置換を適用して変数を消去した 新たな木を返します。

引数var-cmpr、val-cmpr、tuple-fold、make-tupleに関しては 上のutil.unificationの説明を参照してください。

(unify-merge '(a 3 (c b)) '(c b (2 e))
             symbol-comparator
             number-comparator
             fold
             (^[_ elts] elts))
 ⇒ (2 3 (2 3))

二つの木が単一化できなければ、#fが返されます。