Prolog: Là f (X) = X unifiable hay không?

Question

Sự hiểu biết của tôi về sự hợp nhất là một chút ít. Tôi hiểu sự thống nhất cơ bản, nhưng tôi đang gặp vấn đề với các thuật ngữ vòng đầu của tôi mà không phải là không thể xác định.

Tôi đã xem hướng dẫn về thống nhất trên youtube nêu rõ một biến đang cố gắng thống nhất với cụm từ chứa biến đó, sau đó nó không phải là không thể xác định.

Tuy nhiên khi tôi gõ ?- f(X) = X vào prolog, nó sẽ trả về một cái gì đó dọc theo dòng của ... f(f(f(f(f(f(...)))))) ?

Tôi hiểu tại sao điều này là ... nhưng tôi không hiểu nếu điều này có nghĩa là nó là unifiable hay không, như tôi đã mong đợi nó chỉ để trả lại 'không' nếu nó không phải là không thể nhận ra. Tôi có nghĩ rằng cố gắng thống nhất f (X) = X thất bại trong việc kiểm tra xảy ra, do đó làm cho chúng không thể xác định được?

Answer 1

Vâng, bạn là đúng: Trong logic, một biến x là tất nhiên không cú pháp unifiable với thời hạn f (x) với lý do biến bản thân xảy ra như một subterm nghiêm ngặt của f (x).

Vì lý do này, cái gọi là occurs check làm cho việc hợp nhất thất bại.

Như được ghi chú chính xác trong bài viết đó, việc triển khai Prolog thường là bỏ qua kiểm tra xảy ra vì lý do hiệu quả và điều đó có thể dẫn đến suy luận không rõ ràng.

Tuy nhiên, bạn luôn có thể thực hiện hợp nhất với xảy ra kiểm tra trong Prolog bằng cách sử dụng vị từ ISO unify_with_occurs_check/2. Đúng như mong đợi, sự thống nhất bạn đang hỏi về không trong trường hợp đó:

 
?- unify_with_occurs_check(X, f(X)). 
false. 

Lưu ý rằng trong một số hệ thống Prolog, bạn có thể đặt một lá cờ để cho phép xảy ra kiểm tra cho tất cả unifications.

Ví dụ, trong SWI-Prolog:

 
?- set_prolog_flag(occurs_check, true). 
true. 

?- X = f(X). 
false. 

tôi khuyên bạn nên bật cờ này để có được kết quả âm thanh.

Thông báo rằng yêu cầu kiểm tra xảy ra thường biểu thị lỗi lập trình. Vì lý do này, bạn có thể đặt cờ để ném các lỗi thay vì không âm thầm.

Xem thêm số related question được liên kết bởi @false trong các nhận xét ở trên và tham chiếu được trích dẫn.