Thuật toán "unifier chung nhất" tối ưu là gì?

Question

Câu hỏi

Thuật toán MGU hiệu quả nhất là gì? Độ phức tạp của nó là gì? Có đủ đơn giản để mô tả như là một câu trả lời tràn ngăn xếp không?

Tôi đã cố gắng tìm câu trả lời trên Google nhưng tiếp tục tìm các tệp PDF riêng tư mà tôi chỉ có thể truy cập thông qua đăng ký ACM.

Tôi tìm thấy một cuộc thảo luận trong SICP: here

Giải thích về những gì một "hầu hết các thuật toán thống nhất chung" là: Hãy hai cây biểu thức có chứa "biến tự do" và "hằng số" ... ví dụ

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

Sau đó, thuật toán Tổng hợp chung nhất trả về tập hợp kết hợp chung nhất làm cho hai biểu thức tương đương.

ví dụ:

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

By "nhất chung", bạn thay vì có thể ràng buộc (x = 1) và (z = 1) và đó cũng sẽ làm cho e1 và e2 tương đương nhưng nó sẽ cụ thể hơn.

Bài viết SICP có vẻ ngụ ý rằng nó là khá đắt tiền.

Để biết thông tin, lý do tôi hỏi là vì tôi biết rằng suy luận kiểu cũng liên quan đến thuật toán "thống nhất" này và tôi muốn hiểu nó.

Answer 1

Thuật toán đơn giản được sử dụng trong thực tế (ví dụ: trong Prolog) là số mũ cho các trường hợp bệnh lý. Có một thuật toán hiệu quả về mặt lý thuyết của Martelli và Montanari (IIRC nó là tuyến tính), nhưng nó chậm hơn nhiều đối với các trường hợp đơn giản xảy ra trong thực tế, do đó nó không được sử dụng nhiều.

Answer 2

Baader and Snyder xuất bản một số thuật toán hợp nhất, cho cả thống nhất cú pháp và thống nhất bình đẳng.

Họ tuyên bố rằng thuật toán thống nhất cú pháp thứ ba của họ (trong phần 2.3) chạy trong O (n alpha (n)) trong đó alpha (n) là hàm đảo ngược Ackermann - trong các tình huống thực tế tương đương với một hằng số nhỏ.