0

回想一下这个证明元循环

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

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

请帮我 ！发送

4

1 回答 1

1

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

在这个元解释器中，您正在具体化（〜实现）连词。你用 Prolog 的连词来实现它。现在你有两个不同的版本来解释连词。一旦你说先证明 A，然后证明 B。然后你说相反。

考虑到

p :- p, false.

和

p :- false, p.

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

另请参阅此答案，这可能会稍微澄清这些概念。

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

最后评论一下您的元解释器的风格：您正在混合列表和其他术语。事实上[true|true]会是真的。一定要避免这样的表示。要么坚持传统的“香草”表示，它在 Prolog 规则的语法树上运行。也就是说，连词表示为(',')/2。或者坚持列表。但不要混合列表和其他表示。

于 2014-06-21T17:55:47.753 回答