prolog - 依赖规则顺序

Question

为了计算两个相同长度列表之间的汉明距离，我使用 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.

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

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

我知道查询

hamm(a, B, 0, 1).

为假，而

hamm2(a, B, 0, 1).

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

Answer 1

OP 实现了两个累加器式谓词来计算汉明距离(hamm/4 和 hamm2/4)，但不确定哪一个使得更多意义。

让我们读一下令 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.

从逻辑角度来看，两种实现在上述测试中都表现错误。让我们做一些坚定性测试:

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

请注意，在之前的查询中，当 hamm2/4 错误成功时，hamm/4 正确地失败，反之亦然。所以两者都是一半对/一半错，并且都没有一个很坚定。

<小时/>

可以做什么？

基于 @false 在 this answer 中提出的 if_/3 和 (=)/3 ，我为谓词实现了以下纯代码 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.