How to implement Peano numbers exponentiation in Prolog?

Question

I am trying to implement exponentiation with the code below, but a simple query like 2^1 (ex(s(s(0)), s(0), Z).) hangs forever.

nat(0).
nat(s(X)) :- nat(X).
su(0, X, X) :- nat(X).
su(s(X), Y, s(Z)) :- su(X, Y, Z).

mu(0, _, 0).
mu(s(X), Y, Z) :- su(Y, A, Z), mu(X, Y, A).

ex(_, 0, s(0)).
ex(X, s(Y), Z) :- mu(X, A, Z), ex(X, Y, A).

Answer 1

As far as I can see, it is not efficient, because the mu/3 is called with two free variables. Indeed:

ex(X, s(Y), Z) :- mu(X, A, Z), ex(X, Y, A).

Both A and Z are unknown at that moment (I have put them in boldface).

Now your mu/2 is not capable of handling this properly. If we query mu/3 with mu(s(0), A, Z), we get:

?- mu(s(0), A, Z).
A = Z, Z = 0 ;
ERROR: Out of global stack

So it got stuck in infinite recursion as well.

This is due to the fact that it will tak the second clause of mu/3, and:

mu(s(X), Y, Z) :- su(Y, A, Z), mu(X, Y, A).

So su/3 is called with three unknown variables. The effect of this is that su/3 can keep proposing values "until the end of times":

?- su(A, B, C).
A = B, B = C, C = 0 ;
A = 0,
B = C, C = s(0) ;
A = 0,
B = C, C = s(s(0)) ;
A = 0,
...

even if the recursive mu(X, Y, A) rejects all these proposals, su/3 will never stop proposing new solutions.

Therefore it might be better to keep that in mind when we design the predicates for mu/3, and ex/3.

We can for example use an accumulator here that accumulates the values, and returns the end product. The advantage of this, is that we work with real values when we make the su/3 call, like:

mu(A, B, C) :-
    mu(A, B, 0, C).

mu(0, _, 0, S, S).
mu(s(X), Y, I, Z) :-
    su(Y, I, J),
    mu(X, Y, J, Z).

Now if we enter mu/3 with only the first parameter fixed, we see:

?- mu(s(0), X, Y).
X = Y, Y = 0 ;
X = Y, Y = s(0) ;
X = Y, Y = s(s(0)) ;
X = Y, Y = s(s(s(0))) ;
...
?- mu(s(s(0)), X, Y).
X = Y, Y = 0 ;
X = s(0),
Y = s(s(0)) ;
X = s(s(0)),
Y = s(s(s(s(0)))) ;
X = s(s(s(0))),
Y = s(s(s(s(s(s(0)))))) ;
...
...

So that means that we now at least do not get stuck in a loop for mu/3 with only the first parameter fixed.

We can use the same strategy to define an ex/3 predicate:

ex(X, Y, Z) :-
    ex(X, Y, s(0), Z).

ex(X, 0, Z, Z).
ex(X, s(Y), I, Z) :-
    mu(X, I, J),
    ex(X, Y, J, Z).

We then manage to calculate exponents like 2¹ and 2²:

?- ex(s(s(0)), s(0), Z).
Z = s(s(0)) ;
false.
?- ex(s(s(0)), s(s(0)), Z).
Z = s(s(s(s(0)))) ;
false.

Note that the above has still some flaws, for example calculating for which powers the value is 4 will still loop:

?- ex(X, Y, s(s(s(s(0))))).
ERROR: Out of global stack 

By rewriting the predicates, we can avoid that as well. But I leave that as an exercise.