Wie kann die Kommutativität der dif/2-Einschränkung überprüft werden?

Question

Es gibt eine Menge Hype um die Einschränkung dif/2, vor allem als Rettung für einige Nicht-Deklarativität von (\ =)/2 und (\ ==)/2. Diese Nicht-Deklarativität wird oft als Nicht-Monotonie charakterisiert und es werden Beispiele von Nicht-Kommunativität gegeben.

Aber was wäre das Mittel zu testen, ob Testfälle mit dif/2 kommutativ sind. Hier ist eine Meta-Erklärung, was ich tun möchte:

ich einen commutativity Test machen, und ich möchte sondieren, dass beide Varianten das gleiche Ergebnis:

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

Also in der Regel können Sie Überprüfen Sie die Monotonie, wenn es darauf hinausläuft, die Kommutativität mit dem (==)/2 integrierten Prädikat zu überprüfen. Da dieses Prädikat auf instanziierte Variablen folgt. Wenn Sie Fälle testen, die Einschränkungen erzeugen, reicht call_with_residue/2 nicht aus. Welche kann schwierig sein, wie das folgende Beispiel zeigt:

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)). 

Irgendwelche Ideen, wie gehe ich vor?

Haftungsausschluss, es ist eine Falle:
I commutativity Tests als gutes Testverfahren nicht unterstützen, wo Sie gute und schlechte Prädikate im Vergleich zu einer Spezifikation trennen können. Da normalerweise sowohl die guten als auch die schlechten Prädikate keine Probleme mit der Kommutativität haben.

Ich verwende Kommutativitäts-Tests als ein Vehikel, um Methoden für die Gleichheit von dif/2-Constraints herauszufinden. Diese Gleichheit kann dann in traditionelleren Testfällen als Validierungspunkt verwendet werden.

Answer 1

Es gibt mehrere Möglichkeiten. Am einfachsten ist es in diesem Fall, die gesammelten Restriktionen einfach neu zu posten.

In diesem Beispiel erhalten wir:

 
?- 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)). 

Ziel jetzt viel einfacher ist!

Sie können mit copy_term/3 und call_residue_vars/2 Rest Ziele sammeln.