Деление в прологе

Question

Я пытаюсь определить деление в прологе, используя теорему об остатке и принцип упорядочения.

До сих пор я получил:

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)).

Но определениеdiv как-то не так.Может кто-нибудь дать мне подсказку?

PS: я не должен был использовать eq, но я не мог заставить is или = работать.

Answer 1

В SWI-Prolog вы можете попробовать ?- gtrace, your_goal. использовать графический трассировщик и посмотреть, что идет не так. Вместо eq(A, add(times(Q, R), R)) вы должны написать, например: times(Q, R, T), add(T, R, A), поскольку вы хотите использовать предикаты "times / 3" и "add / 3" вместо простого вызова предиката "eq / 2" с составным термином состоящий из "add / 2" и "times / 2" в качестве второго аргумента. Есть и другие проблемы с кодом, например, отсутствует определение nat / 1, но я надеюсь, что это поможет.