応用情報技術者の本で「単一化(ユニフィケーション)と後戻り(バックトラック)といえば論理型プログラミング」みたいな記述を見たことがあるが、実際に論理型プログラミングをやったことがなかったので、何をしているかがいまいちピンと来ていなかった。
「コンピュータプログラミングの概念・技法・モデル」の単一化についての節を見てちゃんとした理解が得られた。
アルゴリズム的にはxとyを単一化する場合
1．xが同値集合ESx、yが同値集合ESyに属していた場合、ESxとESyを併合する。
2. xが同値集合ESxに属し、yが決定状態にあったときにはESx内の全ての変数にyを束縛する。
3. yが同値集合ESyに属し、xが決定状態にあったときにはESy内の全ての変数にxを束縛する。
4. xがk1、yがk2に束縛されていたとき、k1≠k2であれば失敗する。
5. xがk1、yがk2に束縛されていたとき、k1＝k2であればk1とk2を単一化する。
といったことを行う。(今回は変数の場合のみの場合を書き、レコードに対する処理などを省略した)
循環的構造に対してはレコードなどの場合の再帰処理部分を注意する必要はあるようだが、簡単な理解には上のような内容だけでも十分だった。
基本的には、数学的にx≠yであれば失敗し、x＝yであればxをyに(もしくはyをxに)束縛する、という処理を行っている。
