Division in prolog

Question

I'm trying to define the division in prolog using the remainder theorem and the well-ordering principle.

I've got thus far:

less(0, s(0)).

less(0, s(B)) :- less(0, B).
less(s(A), s(s(B))) :- less(A, s(B)).

add(A,0,A)       :- nat(A).
add(A,s(B),s(C)) :- add(A,B,C).  % add(A,B+1,C+1) = add(A,B,C)

add2(A,0,A).
add2(A,s(B),s(C)) :- add2(A,B,C).  % add(A,B+1,C+1) = add(A,B,C)

times(A,0,0).
times(A,s(B),X) :- times(A,B,X1),
               add(A,X1,X).

eq(0,0).
eq(s(A), s(B)) :- eq(A, B).

% A / B = Q (R) => A = B * Q + R
div(A, B, Q, R) :- less(R, B), eq(A, add(times(Q, R), R)).

But the definition of div is somehow wrong. Could someone please give me a hint?

PS: I shouldn't be using eq, but I couldn't get is or = to work.

Answer 1

In SWI-Prolog, you can try ?- gtrace, your_goal. to use the graphical tracer and see what goes wrong. Instead of eq(A, add(times(Q, R), R)), you should write for example: times(Q, R, T), add(T, R, A), since you want to use the "times/3" and "add/3" predicates, instead of just calling the "eq/2" predicate with a compound term consisting of "add/2" and "times/2" as its second argument. There are other problems with the code as well, for example, the definition of nat/1 is missing, but I hope this helps somewhat.