如何验证涉及 diff/2 约束的交换性? [英] How to validate commutativity involving the dif/2 constraint?

问题描述

围绕 dif/2 约束有很多炒作，特别是作为对 (\=)/2 和 (\==)/2 的某些非声明性的拯救.这种非陈述性通常被描述为非单调性，并给出了非交换性的例子.

但是测试涉及 dif/2 的测试用例是否可交换的方法是什么.这是我想要做的元解释:

<块引用>

我做了一个交换性测试，我想探究这两个变体给出相同的结果:

?- A, B.-  相对  -?- B, A.

所以通常你可以检查单调性，如果它归结为检查交换性，使用 (==)/2 内置谓词.因为这个谓词跟在实例化的变量之后.

但是如果你正在测试产生约束的案例，调用_with_residue/2是不够的，你还需要有平等的约束.哪个行有点棘手，如下例所示:

欢迎使用 SWI-Prolog(多线程，64 位，版本 7.3.23)版权所有 (c) 1990-2015 阿姆斯特丹大学，VU 阿姆斯特丹?- 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),差异(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 收集剩余目标.

There is a lot of hype around the dif/2 constraint, especially as a rescue for some non-declarativity of (\=)/2 and (\==)/2. This non-declarativity is often characterized as non-monotonicity and examples of non-communtativity are given.

But what would be the means to test whether test cases involving dif/2 are commutative. Here is a meta explanation what I want to do:

I make a commutativity test, and I want to probe that both variants give the same result:

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

So usually you can check monotonicity, if it boils down to checking commutativity, with the (==)/2 built-in predicate. Since this predicate follows instantiated variables.

But if you are testing cases that produce constraints, call_with_residue/2 is not enough, you need also to have equality of constraints. Which can be tricky, as the following example shows:

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

Any ideas how to proceed?

Disclaimer, its a trap:
I don't endorse commutativity testing as a good testing method, where you can separate good and bad predicates versus a specification. Since usually both the good and bad predicates might have no problems with commutativity.

I am using commutativity testing as a vehicle to find out about methods for equality of dif/2 constraints. This equality can then be used in more traditional test cases as a validation point.

解决方案

There are several ways. Maybe the easiest in this case is to simply re-post the collected residual constraints.

In this example, we get:

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

The goal is now much simpler!

You can collect residual goals with copy_term/3 and call_residue_vars/2.

这篇关于如何验证涉及 diff/2 约束的交换性?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！