依赖规则顺序

为了计算两个相同长度列表之间的汉明距离，我使用foldl(hamm, A, B, 0, R).有了这个定义hamm/4:

hamm(A, A, V, V) :- !.
hamm(A, B, V0, V1) :- A \= B, V1 is V0 + 1.

第一条规则的删减可以防止不必要的回溯。然而，第二条规则可以有不同的写法：

hamm2(A, A, V, V) :- !.
hamm2(_, _, V0, V1) :- V1 is V0 + 1.

and hamm2/4仍然是正确的foldl/5或者对于 A 和 B 都接地的查询。

那么，是否有真正充分的理由选择其中一种而不是另一种呢？或者是否有理由保持规则的顺序或改变它们？

我知道查询

hamm(a, B, 0, 1).

是假的，而

hamm2(a, B, 0, 1).

确实如此，但我无法确定哪一个更有意义。 。 。

OP 实现了两个累加器式谓词来计算汉明距离 (hamm/4 and hamm2/4），但不确定是哪一个制作的more sense.

让我们读一下令OP感到困惑的查询：“是否存在一个X使得距离（a，X）为1？”。以下是 Prolog 给出的“答案”：

?- hamm(a,X,0,1). 
false.                          % wrong: should succeed conditionally
?- hamm2(a,X,0,1).              % wrong: should succeed, but not unconditionally
true.

从逻辑的角度来看，both在上述测试中实现行为不当。让我们做一些测试坚定:

?- hamm(a,X,0,1),X=a.           % right
false.
?- hamm(a,X,0,1),X=b.           % wrong: should succeed as distance(a,b) is 1
false.

?- hamm2(a,X,0,1),X=a.          % wrong: should fail as distance(a,a) is 0
X = a.
?- hamm2(a,X,0,1),X=b.          % right 
X = b.

请注意，在之前的查询中hamm/4正确地失败时hamm2/4错误地成功了，反之亦然。 所以both一半对/一半错，并且neither一 是坚定的。

可以做什么？

基于if_/3 and (=)/3由 @false 提出这个答案 https://stackoverflow.com/a/27358600/4609915，我为谓词实现了以下纯代码hamm3/4:

:- use_module(library(clpfd)).

hamm3(A,B,V0,V) :-
   if_(A = B, V0 = V, V #= V0+1).

现在让我们使用重复上面的查询hamm3/4:

?- hamm3(a,X,0,1). 
dif(X,a).
?- hamm3(a,X,0,1),X=a.
false.
?- hamm3(a,X,0,1),X=b.
X = b.

有用！最后，我们再问一下最一般的查询查看整个解决方案集hamm3/4:

?- hamm3(A,B,N0,N).
A = B,    N0 = N ;
dif(A,B), N0+1 #= N.