有很多关于 dif/2 约束的炒作，尤其是作为对 (\=)/2 和 (\==)/2 的一些非声明性的拯救。这种非陈述性通常被描述为非单调性，并给出了非交换性的例子。
但是测试涉及 dif/2 的测试用例是否可交换的方法是什么。这是我想要做的元解释:
I make a commutativity test, and I want to probe that both variants give the same result:
?- A, B. -- versus -- ?- B, A.
所以通常你可以检查单调性，如果它归结为检查交换性，使用 (==)/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),
差异(f(U，T)，f(g(Z)，Z))。
现在的目标要简单得多!
您可以使用 copy_term/3 收集剩余目标和 call_residue_vars/2 .
关于prolog - 如何验证涉及 diff/2 约束的交换性？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/38064479/