Prolog程序设计语言与证明树

Question

回想一下这个证明元循环

solve(true, true).
solve([], []). 
solve([A|B],[ProofA|ProofB]) :-
   solve(A,ProofA),
   solve(B, ProofB).
solve(A, node(A,Proof)) :-
   rule(A,B),
   solve(B,Proof).

假设解释器的第三个规则被改变，而解释器的其他规则保持不变，如下所示：

% Signature: solve(Exp, Proof)/2 solve(true, true). 
solve([], []).                                      
solve([A|B], [ProofA|ProofB]) :-
   solve(B, ProofB),   %3
   solve(A, ProofA). 
solve(A, node(A, Proof)) :-
   rule(A, B),
   solve(B, Proof). 

考虑将在两个版本中为某些查询创建的证明树。变量替换只能在一个版本中实现吗？解释一下。任何真正的叶子可以移动到最左边的无限分支的另一边吗？解释一下。在这两个问题中，如果答案是肯定的，请举例说明。这将对证据产生怎样的影响？

请帮帮我！发送

Answer 1

(我对你的元解释器有很多保留意见。但首先我会回答你的问题)

在这个元解释器中，你正在具体化(~实现)合取。你可以用Prolog的合取来实现它。现在，您有两个不同的版本来解释连接词。一旦你说先证明A，然后证明B，然后你说相反的。

想想

p :- p, false.

和

p :- false, p.

第二个版本将产生一个有限故障分支，而第一个版本将产生一个无限故障分支。所以这就是使用一个或另一个元解释器的效果。请注意，这个“错误”可以通过解释元解释器本身来减轻！

另请参阅this answer，它可能会稍微澄清一些概念。

还有其他方法来实现合取(通过二值化)；这样下一级元解释器将不再能够进行补偿。

最后，关于你的元解释器的风格:你混合了列表和其他术语。事实上，[true|true]将会是真的。一定要避免这样的表示。要么坚持传统的“香草”表示法，它在Prolog规则的语法树上操作。也就是说，合取被表示为(',')/2。或者坚持使用列表。但不要混用列表和其他表示法。