Prolog - 为什么以下代码会永远生成解决方案 X=root?

Prolog - why does the following code generate the solution X=root forever?

black(root). 
black(v1). 
black(v3). 
black(v4). 

edge(root,root).
edge(v1,root). 
edge(v2,v1). 
edge(v3,v1). 
edge(v4,v3). 
edge(v5,v2). 
edge(v5,v4). 
edge(v6,v5). 

foo(root). 
foo(X) :- edge(X,Y), black(Y), foo(Y).

然后我输入 foo(X) 并且只得到 X=root.

我真的想不通为什么。由于 foo 的第一部分,我们得到了第一个 root。然后我们应该去第二部分,然后我们继续寻找边缘(root,root)black(root) returns true foo(root) 所以我们得到另一个根 solution。为什么我们不去边缘(v1,root)?我错过了什么?

因为寻找第三个解决方案是从 Y=root 时重试 foo(Y) 开始的,并且您已经确定至少有 2 种不同的方法可以证明 foo(root)。 (但是,正如@WillemVanOnsem 指出的那样,情况比这更糟。)

这里是一个片段,负责非终止称为。您需要以某种方式修改剩余部分以避免该循环。

black(root).
black(v1) :- false. 
black(v3) :- false. 
black(v4) :- false. 

edge(root,root).
edge(v1,root) :- false. 
edge(v2,v1) :- false. 
edge(v3,v1) :- false. 
edge(v4,v3) :- false. 
edge(v5,v2) :- false. 
edge(v5,v4) :- false. 
edge(v6,v5) :- false. 

foo(root) :- false. 
foo(X) :- edge(X,Y), black(Y), foo(Y), false.

解决此问题的最简单方法是重用 closure0/3

edgeb(X, Y) :-
   edge(X, Y),
   black(Y).

foo(X) :-
   closure0(edgeb, X, root).

...或更改您的事实。上面的 failure-slice 向我们表明 edge(root,root). 是问题的一部分。什么,如果我们只是删除这个事实?或者变成

edge(root,root) :- false.

现在 foo(X) 终止:

?- foo(X).
   X = root
;  X = v1
;  X = v2
;  X = v3
;  X = v4
;  X = v5
;  false.

为了避免锤击 ;SPACE 太多次,您的腕管建议:

?- foo(X), false.
false.

据此我们证明您的程序将总是终止。不可能有任何特殊情况潜伏。