Nhà nước của nghệ thuật — có, cho đến nay như tôi biết tất cả các thuật toán nhiều hơn hoặc ít hơn có hình dạng giống như (tôi làm theo lý thuyết của chương trình logic, mặc dù chuyên môn của tôi là tiếp tuyến) cung cấp bạn cần đầy đủ bậc cao Huet của phù hợp: các vấn đề con như kết hợp thứ tự cao hơn (thống nhất trong đó một cụm từ được đóng), và phép tính mẫu của Dale Miller, có thể giải quyết được.
Lưu ý rằng thuật toán của Huet là tốt nhất theo nghĩa sau — nó giống như thuật toán bán quyết định, ở chỗ nó sẽ tìm thấy bộ lọc nếu chúng tồn tại, nhưng không đảm bảo chấm dứt nếu chúng không. Vì chúng ta biết rằng sự thống nhất bậc cao hơn (thực sự, sự thống nhất thứ hai) là không thể giải quyết được, bạn không thể làm tốt hơn thế.
Giải thích: Bốn chương đầu tiên của luận án tiến sĩ của Conal Elliott, Extensions and Applications of Higher-Order Unification phải phù hợp với hóa đơn. Đó là một phần nặng gần 80 trang, với một số lý thuyết loại dày đặc, nhưng nó có động lực tốt, và là tài khoản dễ đọc nhất mà tôi đã nhìn thấy.
Ví dụ: Thuật toán của Huet sẽ đưa ra hàng hóa cho ví dụ này: [X (o), Y (succ (0))]; điều cần thiết sẽ làm lúng túng thuật toán thống nhất bậc nhất.
Nguồn
2009-12-23 22:44:32
Một trong những trường hợp hiếm hoi mà câu hỏi thực sự tốt (không thể googleable hoặc khó khăn để google) đã được hỏi, và một khó khăn để đến, câu trả lời chất lượng cao đã được đưa ra. –
+1 cho cả hai bạn - lol có lẽ đó là lý do tại sao số liệu thống kê của bạn là 300-600 thay vì 31.2K hoặc một cái gì đó tương tự. Bạn có thể chỉ trả lời các câu hỏi mà vài người khác có thể trả lời. –
Conal Elliott chính xác bạn trích dẫn cung cấp câu trả lời khác :-D. – Blaisorblade