How to fix this recursive multiplication?

Question

I am new to logic programming and Prolog. The following Prolog program defines a predicate mul/3 for multiplying the first argument to the second argument, which results in the third argument, based on the equation x * y = z which is equivalent to (x − 1) * y + y = z:

mul(0, _, 0).
mul(X, Y, Z) :-
  ground(X),
  succ(U, X),
  add(V, Y, Z),
  mul(U, Y, V).
mul(X, Y, Z) :-
  var(X),
  add(V, Y, Z),
  mul(U, Y, V),
  succ(U, X).

add(0, Y, Y).
add(X, Y, Z) :-
  ground(X),
  ground(Z),
  succ(U, X),
  succ(V, Z),
  add(U, Y, V).
add(X, Y, Z) :-
  ground(X),
  var(Z),
  succ(U, X),
  add(U, Y, V),
  succ(V, Z).
add(X, Y, Z) :-
  ground(Z),
  var(X),
  succ(V, Z),
  add(U, Y, V),
  succ(U, X).

But it exhausts resources with queries in this argument mode:

?- mul(X, Y, 2).
   X = 1, Y = 2
;  X = 2, Y = 1
;
Stack limit (0.2Gb) exceeded
  Stack sizes: local: 0.2Gb, global: 20.8Mb, trail: 10.4Mb
  Stack depth: 452,739, last-call: 0%, Choice points: 452,716
  In:
    [452,739] add(_1326, 0, 0)
    [452,738] add(_1354, 0, 1)
    [452,737] add(_1382, 0, 2)
    [452,736] mul(_1410, 0, 2)
    [452,735] mul(_1438, 0, 2)

How to fix this recursive multiplication?

Answer 1

The program works okay in the sense that it gives the two solutions, X = 1, Y = 2 and X = 2, Y = 1. It then goes into an infinite search for other solutions.

The problem is with this rule:

mul(X, Y, Z) :-
  var(X),
  add(V, Y, Z),
  mul(U, Y, V),
  succ(U, X).

Here mul(U, Y, V) recurses in a way that the first argument is not ground, but the previous rules assume that it is (when V is not zero). Simply swapping the first two arguments solves the problem.

It is still not perfect though, consider

?- mul(2, 3, X).
   false.

Here the problem is in the previous rule:

mul(X, Y, Z) :-
  ground(X),
  succ(U, X),
  add(V, Y, Z),
  mul(U, Y, V).

The call to add(V, Y, Z) becomes add(V, 3, Z), which is under-defined. Swapping it with the next mul solves this:

mul(X, Y, Z) :-
  ground(X),
  succ(U, X),
  mul(U, Y, V),
  add(V, Y, Z).

So is it okay now? Not really, e.g.

?- mul(X, 3, 6).
   false.

Try to go through it with

?- trace, mul(X,3,6).

and find where the problem lies.

--- EDIT ---

Okay, so let's try this from scratch.

To simplify things, first look at the case when the first two arguments are not variables:

% add1(+X, +Y, ?Z) [semidet]
add1(0, Y, Y) :-
  !.
add1(X, Y, Z) :-
  succ(X1, X),
  add1(X1, Y, Z1),
  succ(Z1, Z).

% mul1(+X, +Y, ?Z) [semidet]
mul1(0, _, 0) :-
  !.
mul1(X, Y, Z) :-
  succ(X1, X),
  mul1(X1, Y, Z1),
  add1(Z1, Y, Z).

Then the other case, when the sum/product is known:

% add2(?X, ?Y, +Z) [nondet]
add2(0, Y, Y).
add2(X, Y, Z) :-
  succ(Z1, Z),
  add2(X1, Y, Z1),
  succ(X1, X).

% mul2(?X, ?Y, +Z) [nondet]
mul2(X, Y, 0) :-
  !,
  (X = 0; Y = 0).
mul2(X, Y, Z) :-
  nonvar(Y),
  !,
  succ(Y1, Y),
  add2(Z1, X, Z),
  mul2(X, Y1, Z1).
mul2(X, Y, Z) :-
  add2(Z1, Y, Z),
  mul2(X1, Y, Z1),
  succ(X1, X).

Note that when the third rule in mul2 recurses, its second argument will be known, and that is used by the second rule. This is very similar to what you have written originally.

Finally, you can create a rule to choose the one you need:

add(X, Y, Z) :-
  nonvar(Z) -> add2(X, Y, Z); add1(X, Y, Z).

mul(X, Y, Z) :-
  nonvar(Z) -> mul2(X, Y, Z); mul1(X, Y, Z).

(Of course, you can unite these rules using var(X) etc., but I think it is much clearer this way.)