Prolog谓词 - 无限循环

Question

我需要用自然数来创建一个2的幂的Prolog谓词.自然数是:0,s(0),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(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).

您可以使用cTI 确定其终止条件.

那么,我是如何提出这个解决方案的呢？我们的想法是找到第二个参数如何确定第一个参数大小的方法.关键的想法是,所有我 ∈ ñ:2 ^我 > 我.

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

这就是为什么原始程序不会终止的原因.我把理由作为失败片.有关详细信息和其他示例,请参阅标记.

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

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

正是这个微小的片段是非终止的来源!看看Z哪个是新的变量!要解决这个问题,必须以某种方式修改此片段.

这就是为什么@ Keeper的解决方案不会终止的原因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).

Answer 2

发生这种情况是因为 pow2 的求值顺序。如果你切换 pow2 的顺序，你将使第一个例子陷入无限循环。所以你可以首先检查 Y 是否是 avar或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).