(将bot 用于其他被认为是zero、null 或0 有点奇怪。格子不是我们这里的主要关注点。)
首先,我们尝试了解程序不终止的原因。这可能非常棘手,特别是在存在! 的情况下,这是 Prolog 的不纯元素之一。它们在一定程度上是需要的,但在这种情况下,它们只是有害的,因为它们阻碍了我们的推理。因此,不要写前两个剪切子句,而是写1
add(bot, X, X).
add(X, bot, X) :- dif(X, bot).
接下来的两次剪辑也是如此。请注意,这两个子句现在是不相交的。在此之后,我们有一个纯单调程序,因此我们可以应用各种推理技术。在这种情况下,failure-slice 正是我们所需要的。为了更好地理解不终止的原因,我将添加目标 false 到程序中,因为我们可以利用一个很好的属性:如果新程序没有终止,那么旧程序也没有终止一个不会终止。通过这种方式,我们可以将问题缩小到原始程序的一小部分。经过几次尝试,我想出了以下失败片段:
add(bot,X,X) :- false.
add(X,bot,X) :- false, diff(X,bot).
add(z(X),z(Y),Res) :- false, add(X,Y,D), Res = z(D).
add(z(X),o(Y),Res) :- false, add(X,Y,D), Res = o(D).
add(o(X),z(Y),Res) :- false, add(X,Y,D), Res = o(D).
add(o(X),o(Y),Res) :- addc(X,Y,D),
false,
Res = z(D)。
addc(bot,X,Res) :- add(X,o(bot),Res),
false。
addc(X,bot,Res) :- 差异(X, bot), add(X,o(bot),Res),
false。
addc(z(X),z(Y),Res) :- false, add(X,Y,D), Res = o(D).
addc(z(X),o(Y),Res) :- false, addc(X,Y,D), Res = z(D).
addc(o(X),z(Y),Res) :- false, addc(X,Y,D), Res = z(D).
addc(o(X),o(Y),Res) :- addc(X,Y,D),
false,
Res = o(D).
?- add(o(o(bot)),X,z(o(o(bot))))。
在大约 2^23 个可能的故障切片中,这似乎是最小的一个。也就是说,任何进一步的false 都会使程序终止。
让我们看一下:Res 无处不在,要么被忽略,要么被进一步传递。 因此第三个参数对终止没有任何影响。但是您可以将所有这些Res = 方程放在:- 之后。这是最早的地方。
add(bot,X,X).
add(X,bot,X):- dif(X,bot).
add(z(X),z(Y), z(D)) :- add(X,Y,D).
add(z(X),o(Y), o(D)) :- add(X,Y,D).
add(o(X),z(Y), o(D)) :- add(X,Y,D).
add(o(X),o(Y), z(D)) :- addc(X,Y,D).
addc(bot,X,Res):- add(X,o(bot),Res).
addc(X,bot,Res):- dif(X, bot), add(X,o(bot),Res).
addc(z(X),z(Y),o(D)):- add(X,Y,D).
addc(z(X),o(Y),z(D)):- addc(X,Y,D).
addc(o(X),z(Y),z(D)):- addc(X,Y,D).
addc(o(X),o(Y),o(D)):- addc(X,Y,D).
另外cTI 给出了有利的终止条件:
% NTI summary: Complete result is optimal.
add(A,B,C)terminates_if b(A),b(B);b(C).
% optimal. loops found: [add(z(_),z(_),z(_)),add(o(bot),o(o(_)),z(z(_))),add(o(o(_)),o(bot),z(z(_)))]. NTI took 8ms,72i,30i
addc(A,B,C)terminates_if b(A),b(B);b(C).
% optimal. loops found: [addc(z(z(_)),z(z(_)),o(z(_))),addc(bot,o(_),z(_)),addc(o(_),bot,z(_))]. NTI took 4ms,96i,96i
所以add/3 在前两个或最后一个参数给出时终止。所以你不需要第一个参数。相反,即使是更一般的查询也会终止:
?- add(X,Y,z(o(o(bot)))).
X = bot, Y = z(o(o(bot)))
; X = z(o(o(bot))), Y = bot
; X = z(bot), Y = z(o(o(bot)))
; X = z(o(o(bot))), Y = z(bot)
; X = z(z(bot)), Y = z(o(o(bot)))
; X = z(z(o(bot))), Y = z(o(bot))
; X = z(z(z(bot))), Y = z(o(o(bot)))
; X = z(z(o(bot))), Y = z(o(z(bot)))
; X = z(o(bot)), Y = z(z(o(bot)))
; X = z(o(o(bot))), Y = z(z(bot))
; X = z(o(z(bot))), Y = z(z(o(bot)))
; X = z(o(o(bot))), Y = z(z(z(bot)))
; X = o(bot), Y = o(z(o(bot)))
; X = o(z(o(bot))), Y = o(bot)
; X = o(z(bot)), Y = o(z(o(bot)))
; X = o(z(o(bot))), Y = o(z(bot))
; X = o(z(z(bot))), Y = o(z(o(bot)))
; X = o(z(o(bot))), Y = o(z(z(bot)))
; X = Y, Y = o(o(bot))
; X = o(o(bot)), Y = o(o(z(bot)))
; X = o(o(z(bot))), Y = o(o(bot))
; X = Y, Y = o(o(z(bot)))
; false.
1 更好的是,将库 reif 的 if_/3 用于 SICStus 和
SWI 使这些条款尽可能确定。
add(A, B, C) :- if_(A = bot, B = C, ( B = bot, A = C ) ).