Prolog谓词 - 无限循环

Question

我需要用自然数为2的幂创建一个Prolog谓词。 自然数：0，S（O），S（S（0））ANS等..

例如：

?- pow2(s(0),P). 
P = s(s(0)); 
false. 
?- pow2(P,s(s(0))). 
P = s(0); 
false. 

这是我的代码：

times2(X,Y) :- 
    add(X,X,Y). 

pow2(0,s(0)). 
pow2(s(N),Y) :- 
    pow2(N,Z), 
    times2(Z,Y). 

它和第一个例子完美地结合，但是在第二个例子中进入了一个无限循环..
我该如何解决这个问题？

Answer 1

这是因为pow2的评估顺序而发生的。 如果您切换pow2的顺序，您将有第一个例子卡在无限循环.. 因此，您可以先检查，如果Y是var或nonvar。

像这样：

times2(X,Y) :- 
    add(X,X,Y). 

pow2(0,s(0)). 
pow2(s(N),Y) :- 
    var(Y), 
    pow2(N,Z), 
    times2(Z,Y). 
pow2(s(N),Y) :- 
    nonvar(Y), 
    times2(Z,Y), 
    pow2(N,Z). 

Answer 2

这里是终止第一个或第二个参数被绑定一个版本：

 
pow2(E,X) :- 
    pow2(E,X,X). 

pow2(0,s(0),s(_)). 
pow2(s(N),Y,s(B)) :- 
    pow2(N,Z,B), 
    add(Z,Z,Y). 

您可以用determine its termination conditions CTI。

那么，我是怎么想出这个解决方案的？这个想法是找到第二个参数如何决定第一个参数大小的方法。关键的想法是，对于所有我 ∈ ñ：2 ^我 > 我。

所以我又加了一个参数来表达这种关系。也许你可以进一步加强它？

---

这就是原始程序不终止的原因。我给出了原因为failure-slice。查看标签了解更多详情和其他示例。

 
?- pow2(P,s(s(0))), false. 

pow2(0,s(0)) :- false. 
pow2(s(N),Y) :- 
    pow2(N,Z), false, 
    times2(Z,Y). 

这是一个非终止源的小片段！看看Z这是一个新的新变量！为了解决这个问题，这个片段必须被修改某种程度上。

---

这里是为什么@守护者的解决方案不终止pow2(s(0),s(N))的原因。

 
?- pow2(s(0),s(N)), false. 

add(0,Z,Z) :- false. 
add(s(X),Y,s(Z)) :- 
    add(X,Y,Z), false. 

times2(X,Y) :- 
    add(X,X,Y), false. 

pow2(0,s(0)) :- false. 
pow2(s(N),Y) :- false, 
    var(Y), 
    pow2(N,Z), 
    times2(Z,Y). 
pow2(s(N),Y) :- 
    nonvar(Y), 
    times2(Z,Y), false, 
    pow2(N,Z).