prolog unification resolution

Question

Why does this work:

   power(_,0,1) :- !.
   power(X,Y,Z) :-
      Y1 is Y - 1,
      power(X,Y1,Z1),
      Z is X * Z1.

And this gives a stack overflow exception?

power(_,0,1) :- !.
power(X,Y,Z) :-
  power(X,Y - 1,Z1),
  Z is X * Z1.

Answer 1

Because arithmetic operations are only performed on clauses through the is operator. In your first example, Y1 is bound to the result of calculating Y - 1. In the later, the system attempts to prove the clause power(X, Y - 1, Z1), which unifies with power(X', Y', Z') binding X' = X, Y' = Y - 1, Z' = Z. This then recurses again, so Y'' = Y - 1 - 1, etc for infinity, never actually performing the calculation.

Prolog is primarily just unification of terms - calculation, in the "common" sense, has to be asked for explicitly.