如何验证涉及dif / 2约束的交换性？
围绕dif / 2约束有很多炒作，特别是作为（ =）/ 2和（ ==）/ 2的某些非声明性的救援。 这种非表达性通常表现为非单调性，并给出了非交换性的例子。
但是，测试涉及dif / 2的测试用例是否可交换的手段是什么？ 这是一个元说明我想要做的事情：
我做了一个交换性测试，并且我想探索两个变种都给出了相同的结果：
?- 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), dif(f(U, T), f(g(Z), Z)).
目标现在更简单了！
您可以使用copy_term/3和call_residue_vars/2收集剩余目标。
上一篇: How to validate commutativity involving the dif/2 constraint?