Prolog predicate - infinite loop

问题:

I need to create a Prolog predicate for power of 2, with the natural numbers. Natural numbers are: 0, s(0), s(s(0)) ans so on..

For example:

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

This is my code:

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

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

And it works perfectly with the first example, but enters an infinite loop in the second..
How can I fix this?

回答1:

This happends because the of evaluation order of pow2. If you switch the order of pow2, you'll have the first example stuck in infinite loop.. So you can check first if Y is a var or nonvar.

Like so:

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

回答2:

Here is a version that terminates for the first or second argument being bound:

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

You can determine its termination conditions with cTI.

So, how did I come up with that solution? The idea was to find a way how the second argument might determine the size of the first argument. The key idea being that for all i ∈ N: 2ⁱ > i.

So I added a further argument to express this relation. Maybe you can strengthen it a bit further?

---

And here is the reason why the original program does not terminate. I give the reason as a failure-slice. See tag for more details and other examples.

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

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

It is this tiny fragment which is the source for non-termination! Look at Z which is a fresh new variable! To fix the problem, this fragment has to be modified somehow.

---

And here is the reason why @Keeper's solution does not terminate for 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).