Narrowingの意味論と論理プログラミングへの応用
スポンサーリンク
概要
- 論文の詳細を見る
Narrowingは等式論理に基づく拡張ユニフィケーションの基本手続きである.論理プログラムのユニフィケーションを拡張する方法は,関数記法を導入するなどの目的で数多くの提案がされている。Hullotは等式集合を項書き換えシステムとみなすとき,narrowingの繰り返しと恒等公理を用いることによりユニファイアの完備集合が得られることを示している.完備集合は従来のmguに相当するから,SLD導出におけるmguを完備集合でおきかえることが考えられる.しかし,完備集合は一般に無限集合であるため,この考え方をそのまま実現すると,SLD導出が一向に進展しない事態が生じる。また,プログラムの不動点意味論はHerbrand基底の商集合を用いるので, narrowingについて記述できない。本稿では,narrowingのHerbrand基底を用いた不動点意味論を明らかにし,narrowingとSLD導出の整合を考察する。そして確定節に制限をおくことにより,確定節と等式からなるプログラムに対して, narrowingとSLD導出を同等な手続きとする反駁を与える。この反駁を用いると,ユニフィケーションの一部を待避させSLD導出を優先させて無限探索を回避する方法などが考えられる。また, Herbrand基底を用いた不動点意味論を与え,等式に[3]と同様の条件を与えて反駁の完全性を議論する。
- 1986-10-01