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

这是一个终止于第一个或第二个参数被绑定(bind)的版本:

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)。

您可以determine its termination conditions与 cTI。

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

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

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

?- pow2(P,s(s(0))), 错误。

pow2(0,s(0)) :- 错误。
pow2(s(N),Y) :-
pow2(N,Z)，假，
次2(Z，Y)。

正是这个微小的片段是不终止的源泉!看Z这是一个全新的变量!要解决此问题，必须修改此片段 不知何故 .

这就是@Keeper 的解决方案不会因pow2(s(0),s(N)) 而终止的原因。 .

?- pow2(s(0),s(N))，假的。

添加(0，Z，Z):-错误。
添加(s(X)，Y，s(Z)):-
添加(X，Y，Z)，假。

次2(X，Y):-
添加(X，X，Y)，假。

pow2(0,s(0)) :- 错误。
pow2(s(N),Y) :- 错误，
各不相同)，
pow2(N,Z),
次2(Z，Y)。
pow2(s(N),Y) :-
非变量(Y)，
次2(Z，Y)，假，
pow2(N,Z)。