无法通过缓存/记忆来停止 Prolog 节点的创建答案

【问题标题】：Can't stop Prolog nodes creation by caching / memorizing无法通过缓存/记忆来停止 Prolog 节点的创建
【发布时间】：2023-03-10 17:55:01
【问题描述】：

如何在 Prolog 中记住树上的术语？

我认为我的推理很好，但是像 commutation 这样的节点不断添加创建更多具有相同先前值的节点，程序可以运行，但我想停止创建这些节点。

name(Term,X) :- Term=..[X|_].
prop(eq,commutative).
prop(and,commutative).
prop(and,associative).
prop(Op,P):-compound(Op),name(Op,Opname),prop(Opname,P).

identity(A,A). %checks if both are the same, or returns the same in any parameter
commute(A,B):- A=..[N,X,Y], B=..[N,Y,X]. %true if B is commutation of A, or B outputs commutation of A
associate(X,Y):- X=..[N,A,B],B=..[N,BA,BB], Y=..[N,C,BB],C=..[N,A,BA].

:- dynamic proofcache/1.
proof(_,Steps) :- Steps<1, !, false.
proof(eq(A,B),Steps) :- identity(A,B),writeln(["id",A,"=",B,Steps]),!,true.
proof(eq(A,B),Steps) :-  prop(A,commutative),  (proofcache(eq(A,B));asserta(proofcache(eq(A,B))),  commute(A,R),writeln(["comm",A,"=",R,Steps]), proof(eq(R,B),Steps-1)).
proof(eq(A,B),Steps) :-  prop(A,associative),  (proofcache(eq(A,B));asserta(proofcache(eq(A,B))),  associate(A,R),writeln(["assoc",A,"=",R,Steps]), proof(eq(R,B),Steps-1)).

示例查询：

proof(  eq( and(t,and(t,f)), and(and(t,t),f) )  ,6).

【问题讨论】：

这更像是一种猜测，或者如果这是我的问题评论，我个人会看哪里，但总比没有好。这闻起来是 Abstract rewriting system 类型的问题，而不是 Prolog 问题。我想说这是一个confluence 问题，但实际上并没有深入研究这个问题，这与您所描述的不符。
如果您可以访问 Baader 和 Nipkow 的书 Term rewriting and all that，它应该会填补空白。您也可以尝试将其移至CS 网站，
搜索term rewriting prolog 发现this 有可下载的Prolog 代码。与您使用的方式不同，因此您必须学习它才能使用它，但可能会对您有所帮助。
如果你不能得到Term rewriting and all that然后看看A Taste of Rewrite Systems
我很想为此设置 500 分赏金，但不要认为任何经常使用该标签的人都会回答这个问题，我会放弃 500 分。分数的答案必须在 Prolog 中实现一个术语重写系统来解决这个问题。

标签： tree prolog memcached proof

【解决方案1】：

显然问题是我假设分号在 C++ 代码中像 || 一样被短路，因此即使前面的命题被评估为假，; 之后的术语也会被评估，所以在前面加上一个剪切运算符解决了这个问题。

由于我是语言新手，可能会出现更多错误，这是解决方案的示例，writeln 消息有助于发现问题，trace 也可以提供帮助。

proof(eq(A,B),Steps) :- prop(A,commutative),
    (proofcache(eq(A,B),comm), writeln(["comm was cached",eq(A,B),Steps]), !;
    asserta(proofcache(eq(A,B),comm)), writeln(["comm was not cached",eq(A,B),Steps]), 
    commute(A,R), writeln(["comm",A,"=",R,Steps]),
    proof(eq(R,B),Steps-1)).

【讨论】：