順序ソート付き単一化問題の木オートマトンを用いた解法

高井 利憲 (9651065)

本研究では、順序ソート付き単一化問題を木オートマトンを用いて 解く手続きを提案した。 ここで単一化問題とは、二つの目的項 s,t と等式理論 E が与えられたとき、 E 上の方程式 s=t が解けるか否かを判定する問題である。 この問題は項書換え系など理論的計算機科学の分野で重要であるばかりでなく、 導出原理に基づく自動演繹系や論理型言語・関係データベース・自然言語処理 など応用分野も広い。 等式理論 E が合流性を満たす項書換え系 R によって定義されるとき (例えば Knuth-Bendix 完備化手続きによって E から R が得られるとき)、 単一化問題は、R によって sσ と tσ とが 到達可能な項 u と代入 σ が存在するか否かを判定する問題になる。 以下では等式理論 E の代わりに項書換え系 R が与えられるとする。 この問題は一般には決定不能であるにもかかわらず 演繹メカニズムの心臓部ともいえる重要な問題なので 多くの研究がなされてきた。 その中でも順序ソート付き単一化問題は特に重要で、 項の「型(ソート)」とその包摂関係を表現することができるため、 自動演繹における探索領域の削減や 代数的仕様記述での部分関数の定義などに応用されている。

以下では、提案手法の背後にあるアイデアおよび手続きの概略を簡単に紹介する。 与えられた目的項 s,t に対し、 それぞれの例の集合 W'(s) と W'(t) を考える。 さらに項書換え系 R が与えられているときは、 W'(s) から R によって到達可能な項の集合 W(s) を考える (同様にW'(t)についてもW(t)を考える)。 もし s と t が共通の変数を持たないならば、 s と t が単一化可能であるための 必要十分条件は W(s)∩W(t)≠φ である。 しかし一般に集合 W(t) は正則木言語ではないので この空判定問題は決定不能である。 そこで発表者はまず、 集合 W(s) および W(t) が正則木言語 であるような十分条件を提案した。 提案した条件下では W'(s) および W'(t) を受理する木オートマトン M'(s) および M'(t) を簡単に構成することができる。 次に、書換え規則に応じてこの木オートマトン M'(s) および M'(t) の状態と遷移規則を変更することにより、 W(s) および W(t) を受理する木オートマトン M(s) および M(t) を構成する。 構成された木オートマトンに対し、 その受理言語が空か否かを判定することにより、 単一化可能性の判定を行なうことができる。 発表者は木オートマトンの構成法を提案するとともに その健全性と完全性を証明した。

発表では、提案した手続きの概要および その手続きが正しく動くための十分条件を中心に述べる。