Error in replacing arguments in math formula

I have some problems with recursion in replacing arguments in math formula.

I use the predicate which replacing arguments in math formula.

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

In 1 case it's work correctly, when:

% Initial formula: (xy/5-z)+xy*w
% Find: x*y
% Replace: x-a*y+1
% prepared formula in prefix view: +/*xy -5z **xyw
% Find in prefix view: *xy
% Replace in prefix view: *-xa+y1

%Correctly work example

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

% Result after replacing:

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

In 2 case it's doesn't work and I can't solve the problem, already few days...

% Initial formula: ((x->z)->((y->z)->(x/y->z))->(x/y->z))
% Find: A->B
% Replace: not(A/B)
% Comment: Logical De Morgan rule. Implication theorem.
%prepared formula in prefix view: ( ->->->xz ->->yz->/xyz ->/xyz )
% Find in prefix view: ->(A, B)
% Replace in prefix view: not(/(A, B))

%Don't work example 1):

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

% Result after replacing:

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

%Tried another way, but not successful reach the goal:

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

% Result after replacing:

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

But if insert manually previous result to new call then will one more replacing.

%manual insert of previous result from replace3 to replace4

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

% Result after replacing:

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

Could someone give me advice what do wrong? I tried to explain as completely as I can. Thanks very much for your help!

Solution

This predicate clause is your issue I think:

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

If the entire expression matches the find expression, it will be replaced at the top level and then the entire replacement process will stop. In your specific case:

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

Your input expression is already of the form f3(->(A,B)) so your final result is f3(not(\/(A,B))) and the design of the first predicate clause for replace/4 ensures that neither A nor B will be further examined:

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

This problem can actually happen at any level within the recursion. As soon as your predicate sees a subterm that matches your first replace/4 predicate clause, it will replace at that level but no longer go deeper.

You'll need to replace your first clause with something more elaborate which will recursively replace the inner terms when the outer term matches.