在数学公式中替换参数的错误

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个情况下，它的工作正常，

• ％初始公式：（x y/5-z） x y*w
• ％查找：x*y
• ％替换：x-a*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）） z）
• ％查找：a-> b
• ％替换：不（a/b）
• ％评论：逻辑de Morgan规则。暗示定理。
• ％在前缀视图中准备的公式：（ -> -> -> -> -> 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))).

但是，如果手动以先前的结果插入新调用，则会再替换一个。

％的手动插入以前的替换3替换4的结果

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))的形式，因此您的 final 结果是 f3(not(/(A,B)))，并且replace/4的第一个谓词子句的设计可确保A和B都不会进一步检查：

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

这个问题实际上可以在递归中的任何级别上发生。一旦您的谓词看到一个与您的第一个replace/4谓词子句匹配的子术语，它将在该级别上替换，但不再更深。

您需要用更精细的内容替换第一个子句，这些条款将在外术语匹配时递归替换内部条款。