Пролог предшественник математики

Question

У меня есть предикат add2, который разрешается следующим образом: s(0) - преемник 0, т. Е. 1

?- add2(s(0)+s(s(0)), s(s(0)), Z).
Z = s(s(s(s(s(0)))))

?- add2(0, s(0)+s(s(0)), Z).
Z = s(s(s(0)))

?- add2(s(s(0)), s(0)+s(s(0)), Z).
Z = s(s(s(s(s(0)))))

и т. Д.

Япытаясь добавить add в предикате-предшественнике, который будет работать примерно так:

?- add2(p(s(0)), s(s(0)), Z).
Z = s(s(0))

?- add2(0, s(p(0)), Z).
Z = 0

?- add2(p(0)+s(s(0)),s(s(0)),Z).
Z = s(s(s(0)))

?- add2(p(0), p(0)+s(p(0)), Z).
Z = p(p(0))

Кажется, я не могу найти способ сделать это. Мой код ниже.

numeral(0).
numeral(s(X)) :- numeral(X).
numeral(X+Y) :- numeral(X), numeral(Y).
numeral(p(X)) :- numeral(X).


add(0,X,X).
add(s(X),Y,s(Z)) :- add(X,Y,Z).
add(p(X),Y,p(Z)) :- add(X,Y,Z).


resolve(0,0).
resolve(s(X),s(Y)) :-
    resolve(X,Y).
resolve(p(X),p(Y)) :-
    resolve(X,Y).
resolve(X+Y,Z) :-
    resolve(X,RX),
    resolve(Y,RY),
    add(RX,RY,Z).

add2(A,B,C) :-
    resolve(A,RA),
    resolve(B,RB),
    add(RA,RB,C).

Answer 1

В общем случае добавление с арифметикой-преемником означает обработку следующих терминов, которые имеют форму 0 или s(X), где X также является последующим термином. Это полностью решается с помощью этой части вашего кода:

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

Теперь вам нужно принять решение;вы можете либо обработать предшественники и условия добавления здесь, в add/3, либо вы можете заключить этот предикат в другой, который будет обрабатывать их. Вы, кажется, решили обернуть add/3 с add2/3. В этом случае вам определенно потребуется создать сокращающий термин, такой как вы создали здесь с resolve/2, и я согласен с вашей реализацией part этого:

resolve(0,0).
resolve(s(X),s(Y)) :-
    resolve(X,Y).
resolve(X+Y,Z) :-
    resolve(X,RX),
    resolve(Y,RY),
    add(RX,RY,Z).

Это все хорошо. Что вам не хватает сейчас, так это способ обработки p(X) терминов. Правильный способ сделать это - заметить, что у вас уже есть способ вычитать один, используя add/3 с s(0):

resolve(p(X), R) :-
    resolve(X, X1),
    add(s(0), R, X1).

Другими словами, вместо вычисления X с использованием X =Y - 1, мы вычисляем X, используя X + 1 = Y.

Если ваши входные данные никогда не бывают отрицательными, ваш предикат add2/3 теперь будет работать.