Làm cách nào để xác thực tính tương giao liên quan đến giới hạn dif/2?

Question

Có rất nhiều sự cường điệu xung quanh giới hạn dif/2, đặc biệt là giải cứu cho một số không suy giảm (\ =)/2 và (\ ==)/2. Sự không suy giảm này thường được mô tả là không đơn điệu và các ví dụ về không tương giao được đưa ra.

Nhưng điều gì sẽ là phương tiện để kiểm tra xem các trường hợp thử nghiệm có liên quan đến dif/2 có giao hoán hay không. Dưới đây là một lời giải thích meta những gì tôi muốn làm:

tôi thực hiện một thử nghiệm giao hoán, và tôi muốn để thăm dò rằng cả hai biến thể cho kết quả tương tự:

?- A, B. 
-- versus -- 
?- B, A. 

Vì vậy, thông thường bạn có thể kiểm tra tính đơn điệu, nếu nó nhổ xuống để kiểm tra tính tương giao, với vị từ được xây dựng sẵn (==)/2. Vì biến vị ngữ này theo các biến được tạo ra.

Nhưng nếu bạn đang thử nghiệm các trường hợp sản xuất các ràng buộc, call_with_residue/2 là không đủ, bạn cũng cần phải có sự bình đẳng về các ràng buộc. Điều gì có thể là khó khăn, như ví dụ sau đây cho thấy:

Welcome to SWI-Prolog (Multi-threaded, 64 bits, Version 7.3.23) 
Copyright (c) 1990-2015 University of Amsterdam, VU Amsterdam 

?- dif(f(X,X),f(a(U,g(T)),a(g(Z),U))), X=a(g(Z),U). 
X = a(g(Z), U), 
dif(f(a(g(Z), U), U, Z, U, T), f(a(U, g(T)), g(Z), T, g(Z), Z)). 

?- X=a(g(Z),U), dif(f(X,X),f(a(U,g(T)),a(g(Z),U))). 
X = a(g(Z), U), 
dif(f(U, T), f(g(Z), Z)). 

Bất kỳ ý tưởng nào để tiếp tục?

Disclaimer, một cái bẫy của nó:
Tôi không tán thành thử nghiệm giao hoán như một phương pháp thử nghiệm tốt, nơi bạn có thể tách các vị từ tốt và xấu so với một đặc điểm kỹ thuật. Vì thường cả các vị từ tốt và xấu đều không có vấn đề gì với tính tương giao.

Tôi đang sử dụng thử nghiệm giao thoa làm phương tiện để tìm hiểu về phương pháp bình đẳng của dif/2 ràng buộc. Sự bình đẳng này sau đó có thể được sử dụng trong nhiều trường hợp thử nghiệm truyền thống như một điểm xác nhận.

Answer 1

Có một số cách. Có lẽ cách dễ nhất trong trường hợp này là chỉ cần đăng lại các ràng buộc còn lại được thu thập.

Trong ví dụ này, chúng tôi nhận được:

 
?- X = a(g(Z), U), 
    dif(f(a(g(Z), U), U, Z, U, T), f(a(U, g(T)), g(Z), T, g(Z), Z)). 
X = a(g(Z), U), 
dif(f(U, T), f(g(Z), Z)). 

Mục tiêu hiện nay là đơn giản hơn nhiều!

Bạn có thể thu thập các mục tiêu còn lại với copy_term/3 và call_residue_vars/2.