exponentiation - Prolog predicate - infinite loop

Question

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?

Answer 1

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