最適な「最も一般的な統合子」アルゴリズムは何ですか?

Question

質問

最も効率的な MGU アルゴリズムは何ですか?その時間計算量はどれくらいですか?スタック オーバーフローの答えとして説明できるほど単純ですか?

Google で答えを見つけようとしていますが、ACM サブスクリプションを介してのみアクセスできるプライベート .PDF が見つかり続けています。

SICP で次のディスカッションを見つけました。 ここ

「最も一般的な統合アルゴリズム」とは何かについての説明:「自由変数」と「定数」を含む 2 つの式ツリーを考えてみましょう...例えば

 e1 = (+ x? (* y? 3) 5)
 e2 = (+ z? q? r?)

次に、Most General Unifier アルゴリズムは、2 つの式を同等にする最も一般的なバインディングのセットを返します。

つまり

mgu(e1,e2) = (x = z), q = (* y 3), y = unbound, r = 5

「最も一般的」とは、代わりに (x = 1) と (z = 1) をバインドすることもできます。これにより、e1 と e2 も等価になりますが、より具体的になります。

SICP の記事は、それがかなり高価であることを示唆しているようです。

参考までに、私が質問している理由は、型推論にもこの「統合」アルゴリズムが含まれていることを知っており、それを理解したいからです。

Answer 1

実際に使用される単純なアルゴリズム (例:Prolog) は病理学的症例では指数関数的です。

Martelli と Montanari による理論的にはより効率的なアルゴリズム (IIRC は線形です) がありますが、実際に発生する単純なケースでははるかに遅いため、あまり使用されません。

Answer 2

バーダーとスナイダー 構文的統合と等式的統合の両方について、いくつかの統合アルゴリズムを公開しました。

彼らは、3 番目の構文統一アルゴリズム (セクション 2.3) は O(n alpha(n)) で実行されると述べています。ここで、alpha(n) は逆アッカーマン関数です。実際の状況では、それは小さな定数に相当します。