Erreur lors du remplacement des arguments dans la formule mathématique

Question

J'ai quelques problèmes avec la récursivité pour remplacer les arguments dans la formule mathématique.

J'utilise le prédicat qui remplace les arguments dans la formule mathématique.

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

Dans 1 cas, il est correctement travail, lorsque:

• % formule initiale: (x y/5-z) + x y * w
• % Rechercher: x * y
• % Remplacer: xa * y + 1
• % formule préparée en vue du préfixe: +/* xy -5Z ** XYW
• % Rechercher dans une vue préfixe: * xy
• % Remplacer en mode préfixe: * -xa + y1

% fonctionnent correctement par exemple

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

% Résultat après le remplacement:

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

Dans deux cas, il est ne le fait pas travail et je ne peux pas résoudre le problème, déjà quelques jours ...

• % Formule initiale: ((x-> z) -> ((y-> z) -> (x/y-> z)) -> (x/y-> z))
• % Trouver: A -> B
• % Remplacer: non (A/B)
• % Commentaire: Règle logique de Morgan. Théorème d'implication
• % formule préparée en vue de préfixe: (-> -> -> xz -> -> yz ->/xyz ->/xyz)
• % Recherche en vue de préfixe: -> (A, B)
• % remplacer en mode préfixe: non (/ (A, B))

% ne pas travailler par exemple 1):

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

% Résultat après le remplacement:

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

% Essayé une autre façon, mais pas réussi à atteindre l'objectif:

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

% Résultat après le remplacement:

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

Mais si l'insertion résultat manuellement avant nouvel appel alors sera un plus remplaçant.

% insert manuel de résultat précédent de replace3 à replace4

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

% Résultat après le remplacement:

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

Quelqu'un pourrait-il me donner des conseils ce mal? J'ai essayé d'expliquer aussi complètement que possible. Merci beaucoup pour votre aide!

Answer 1

Cette clause sous-jacente est votre problème, je pense:

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

Si l'expression entière correspond à l'expression trouver, il sera remplacé au niveau supérieur, puis l'ensemble du processus de remplacement s'arrête. Dans votre cas:

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

Votre expression d'entrée est déjà la forme f3(->(A,B)) afin que votre résultat final est f3(not(\/(A,B))) et la conception de la première clause de prédicats pour replace/4 assure que ni A ni B sera examinée plus avant:

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

Ce problème peut effectivement se produire à tous les niveaux dans le récursivité. Dès que votre prédicat voit un sous-terme qui correspond à votre première clause de prédicat replace/4, il sera remplacé à ce niveau mais ne sera plus approfondi.

Vous devrez remplacer votre première clause par quelque chose de plus élaboré qui remplacera récursivement les termes internes lorsque le terme extérieur correspond.