Prolog 谓词 - 无限循环

Question

我需要使用自然数为 2 的幂创建一个 Prolog 谓词。 自然数有：0, s(0), s(s(0)) 等等..

例如：

?- 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), 添加（Z，Z，Y）。

您可以使用 cTI determine its termination conditions。

那么，我是如何想出这个解决方案的？这个想法是找到一种方法，第二个参数如何确定第一个参数的大小。关键思想是对于所有 i ∈ N：2ⁱ > i .

所以我添加了一个进一步的论据来表达这种关系。也许你可以进一步加强它？

---

这就是原始程序不终止的原因。我给出的原因是failure-slice。有关更多详细信息和其他示例，请参见标签。

?- pow2(P,s(s(0))), 假。 pow2(0,s(0)) :- false。 pow2(s(N),Y) :- pow2(N,Z), 假, 次2(Z,Y)。

正是这个微小的片段是不终止的源泉！看看Z，这是一个全新的变量！要解决此问题，必须以某种方式修改此片段。

---

这就是@Keeper 的解决方案对于pow2(s(0),s(N)) 没有终止的原因。

?- pow2(s(0),s(N)), false。 add(0,Z,Z) :- false。 添加（s（X），Y，s（Z））：- 添加（X，Y，Z），假。 次2（X，Y）：- 添加（X，X，Y），假。 pow2(0,s(0)) :- false。 pow2(s(N),Y) :- false, var(Y), pow2(N,Z), 次2(Z,Y)。 pow2(s(N),Y) :- 非变量（Y）， times2(Z,Y), 假, pow2(N,Z)。