关于dif/2约束有很多炒作，尤其是作为对(\ =)/2和(\ ==)/2的非声明性的挽救。这种非声明性通常被描述为非单调性，并给出了非通信性的示例。
但是，测试涉及dif/2的测试用例是否可交换的方法是什么。这是一个元解释，我想做什么:
因此，通常可以使用(==)/2内置谓词检查单调性(如果归结为检查可交换性)。由于该谓词遵循实例化变量。
但是，如果您要测试产生约束的案例，请call_with_residue/2
还不够，还需要具有相等的约束。哪个行
如下例所示:
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)).
任何想法如何进行？
免责声明，它是一个陷阱:
我不赞成将可交换性测试作为一种好的测试方法，在该方法中，您可以将好的谓词和坏的谓词与规范分开。因为通常情况下，好的谓词和坏的谓词都可能没有可交换性问题。
我将可交换性测试用作一种工具，以找出有关dif/2约束相等的方法。然后，可以在更传统的测试用例中使用这种相等性作为验证点。
最佳答案
有几种方法。在这种情况下，最简单的方法可能是简单地重新发布收集的残差约束。
在此示例中，我们得到:
？-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))。
现在的目标要简单得多!
您可以使用copy_term/3和call_residue_vars/2收集剩余目标。