Ошибка при замене аргументов в математической формуле

Question

У меня есть некоторые проблемы с рекурсией в замене аргументов в математической формуле.

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

replace(Term,Term,With,With) :-
    !.
replace(Term,Find,Replacement,Result) :-
    Term =.. [Functor|Args],
    replace_args(Args,Find,Replacement,ReplacedArgs),
    Result =.. [Functor|ReplacedArgs].

replace_args([],_,_,[]).
replace_args([Arg|Rest],Find,Replacement,[ReplacedArg|ReplacedRest]) :-
    replace(Arg,Find,Replacement,ReplacedArg),
    replace_args(Rest,Find,Replacement,ReplacedRest).

В 1 случае это работает правильно, когда:

• % Начальная формула: (xy / 5-z) + x y * w
• % Find: x * y
• % Заменить: xa * y + 1
• % подготовленной формулы в виде префикса: + / * xy -5z ** xyw
• % Найти в виде префикса: * xy
• % Заменить в представлении префикса: *-xa+y1

Пример правильной работы

replace1(Result) :- 
    replace(
        f1(+(/(*(x, y), -(5, z)), *(*(x, y), z))), 
        *(x, y), 
        *(-(x, a), +(y, 1)), 
        Result).

% Результат после замены:

?- replace1(Result).
Result = f1((x-a)*(y+1)/(5-z)+(x-a)*(y+1)*z).

В 2 случае это не работает, и я не могу решить проблему, уже несколько дней...

• % Начальная формула: ((x-> z) -> ((y-> z) -> (x / y-> z)) -> (x / y-> z))
• % Найти: A-> B
• % Заменить: нет (A/B)
• Комментарий: логическое правило де Моргана. Импликационная теорема.
• % подготовленной формулы в виде префикса: (-> -> -> xz -> -> yz -> / xyz -> / xyz)
• % Найти в представлении префикса: -> (A, B)
• % Заменить в представлении префикса: нет (/ (A, B))

% Не работает пример 1):

replace3(Result) :- 
    replace(
        f3( ->(->(->(x, z), ->(->(y, z), ->(\/(x, y), z))), ->(\/(x, y), z) )),
        ->(A,B), 
        not(\/(A,B)), 
        Result
    ).

% Результат после замены:

?- replace3(R).
R = f3(not(((x->z)->(y->z)->x\/y->z)\/(x\/y->z))).

Пробовал другой способ, но не удачно достичь цели:

replace3(Result) :- 
    replace(
        f3( ->(->(->(x, z), ->(->(y, z), ->(\/(x, y), z))), ->(\/(x, y), z) )),
        ->(A,B), 
        not(\/(A,B)), 
        Result1
    ),  
    replace(
        Result1,
        ->(A,B), 
        not(\/(A,B)), 
        Result
    ).

% Результат после замены:

?- replace3(R).
R = f3(not(((x->z)->(y->z)->x\/y->z)\/(x\/y->z))).

Но если в новый вызов вручную вставить предыдущий результат, то произойдет еще одна замена.

% ручной вставки предыдущего результата из replace3 в replace4

replace4(Result) :- 
    replace(
        f3(not(((x->z)->(y->z)->x\/y->z)\/(x\/y->z))),
        ->(A,B), 
        not(\/(A,B)), 
        Result
    ).

% Результат после замены:

?- replace4(R).
R = f3(not(not((x->z)\/((y->z)->x\/y->z))\/(x\/y->z))).

Может ли кто-нибудь дать мне совет, что делать не так? Я пытался объяснить как можно полнее. Большое спасибо за вашу помощь!

Answer 1

Это предикатное предложение - ваша проблема, я думаю:

replace(Term,Term,With,With) :- !.

Если все выражение соответствует выражению поиска, оно будет заменено на верхнем уровне, а затем весь процесс замены остановится. В вашем конкретном случае:

replace(
    f3( ->(->(->(x, z), ->(->(y, z), ->(\/(x, y), z))), ->(\/(x, y), z) )),
    ->(A,B), 
    not(\/(A,B)), 
    Result
).

Ваше входное выражение уже имеет форму f3(->(A,B)) так что ваш конечный результат f3(not(\/(A,B))) и дизайн первого предложения предиката для replace/4 гарантирует, что ни A ни B будут дополнительно рассмотрены:

f3(not(((x->z)->(y->z)->x\/y->z)\/(x\/y->z))).

Эта проблема действительно может возникнуть на любом уровне рекурсии. Как только ваш предикат увидит подтерм, соответствующий вашему первому replace/4 Предложение предиката, оно заменит на этом уровне, но больше не будет углубляться.

Вам нужно будет заменить свое первое предложение чем-то более сложным, которое будет рекурсивно заменять внутренние термины, когда внешний термин совпадает.