prolog exponentiation successor-arithmetics

Power with successor arithmetic - how to prevent an infinite loop? [Prolog]

I have been thinking over this the whole day. I finally admit, I do not understand Prolog as good as I thought.

At the start of the day, I had trouble implementing a successor arithmetic, which multiplies 2 s-Numbers, which structure is this:

nat(0).
nat(s(X)):-nat(X).

My first try was this:

 mul(0,_,0).
 mul(s(F1),F2,P):-mul(F1,F2,Tmp),add(F2,Tmp,P)

which worked, but the query mul(X,Y,s(0)) ended in an infinite loop. Why? I have read the following post: Prolog successor notation yields incomplete result and infinite loop

What I understood out of it: If I call mul before calling add, and I have variables in the mul/3 predicate which are NOT used in both mul/3 calls, Prolog tries to find new possibilties for the variables it did not bind. Therefore it goes into an infinite loop.

To solve the problem, I called add first:

mul(0,_,0).
mul(s(F1),F2,P):-add(F2,Tmp,P),mul(F2,F1,Tmp).

That did it. Then i tried to implement the power function, and thought "Well, that's easy now, first try would be:

pow(_,0,s(0)).
pow(B,s(E),R):-pow(B,E,Tmp), mul(Tmp,B,R).

But, I have to put mul first to prevent the left-recursion of R and Tmp.

Easy!" Boy, I was so wrong. I have no idea how to implement it without getting in an infinite loop, even if I put the mul in front.

Any advice is highly appreciated. You can save my saturday work effort and boost my self-esteem! Thank you in advance.

Edit: Added my missing sum predicate:

add(0, Y, Y).
add(s(S1), S2, s(Sum)):-  add(S1,S2,Sum).

Solution

We want that the following termination conditions hold:

pow(B, E, P) terminates_if b(B), b(E).
pow(B, E, P) terminates_if b(P).

or briefly

pow(B, E, P) terminates_if b(B), b(E) ; b(P).

We cannot demand more than that. More than that would be b(B) alone or b(E) alone. But in those cases we need infinitely many answers that imply non-termination. Of course, we could take a definition that is always terminating, and that does succeed for all test cases, like

pow(_B, _E, _P).

Alas, that definition also succeeds for any other case we do not want. So unless you will only get tested for success, you have to take a more elaborate definition.

Another way to avoid non-termination would be to resort into another definition of the natural numbers. Using library(clpz) (SWI's library(clpfd) is a weaker precursor)

pow(B, E, P) :-
   B #>= 0,
   E #>= 0,
   P #= B^E.

But currently, we stick to successor arithmetics. CapelliC already gave you a definition that terminates for b(B), b(E). So let's try to improve it! One way is to somehow use P to restrict the number of inferences to a finite number. A way to do this, is to consider relations between the arguments.

Are there any interesting relations between the arguments of pow/3? I really would like that:

b^e ≥ e, b^e ≥ b for e, b ≥ 0

That is almost true. It holds in fact by adding b ≥ 2.

Just to be sure I will check that I am not completely wrong, I will try this out¹:

?- M #= 10^150, [B,E,P]ins 0..M, P #= B^E, B #>= 2, P #< E.
false.

I will consider this a proof, although it isn't one.

Now for the definition. The idea is to handle the general case by adding additional arguments to limit the number of recursions. One limit LP for pow and one limit LM for mult. These arguments are separated by extra spaces to make clear where they have been added.

pow(_, 0, s(0)).
pow(0, s(_), 0).
pow(s(B), s(0), s(B)).
pow(s(0), s(s(_)), s(0)).
pow(B, E, P) :-
   B = s(s(_)), E = s(s(_)), P = s(s(s(s(_)))), 
   powx(B, E, P,     P, P).
%                    ^^^^^ added arguments to limit pow and mult

sum(0, M, M).
sum(s(N), M, s(K)) :-
    sum(N, M, K).

mul(0,_,0,_).
mul(s(F1),F2,P,    s(LM)) :-
   mul(F1,F2,Tmp,    LM),
   sum(Tmp, F2, P).   % note: arguments exchanged!

powx(_,0,s(0),    _, _).
powx(B,s(E),R,    s(LP), LM) :-
   powx(B,E,Tmp,     LP, LM),
   mul(Tmp,B,R,      LM).

For the simple case pow(b,b,f) the overheads should be minimal. For the new case, pow(f,f,b) the overheads might be reduced by lowering the limits somehow.

^Footnotes

1 I only tried it out with 10¹⁵⁰. No general proof. Let's hope its fine. For some reason, larger values produce a stackoverflow™. It's the last goal P #< E which induces a lot of recalculations. Otherwise it works up to 10^10⁷.