问题标签 [steadfastness]

到目前为止，我在 Prolog 程序中始终坚持的意思是：

如果对于 query Q，有一个 subterm S，这样有一个T使?- S=T, Q. success虽然?- Q, S=T. failed的术语，那么调用的谓词之一Q不是坚定的。

直觉上，我因此将坚定性理解为我们不能使用实例化来“欺骗”谓词来给出解决方案，否则这些解决方案不仅从未给出，而且被拒绝。注意非终止程序的区别！

特别是，至少对我来说，逻辑上的纯粹总是意味着坚定不移。

例子。为了更好地理解稳定的概念，考虑一个几乎经典的反例，在向高级学生介绍 Prolog 的操作方面时经常引用该属性，使用了两个整数与其最大值之间关系的错误定义：

一个明显的错误——我们是否应该说“摇摆不定”——定义当然是以下查询错误地成功：

而交换目标会产生正确的答案：

这个问题的一个很好的解决方案是依靠纯方法来描述关系，例如：

这在两种情况下都可以正常工作，甚至可以在更多情况下使用：

现在 Covington 等人的论文Coding Guidelines for Prolog由该概念的发明者Richard O'Keefe 合着，包含以下部分：

5.1 谓词必须坚定。

任何体面的谓词都必须是“坚定不移的”，即，如果它的输出变量恰好被实例化为输出值，则必须正确工作（O'Keefe 1990）。

那是，

和

必须在完全相同的条件下成功并且具有相同的副作用。只有辅助谓词的调用模式受到主谓词的强烈约束，否则只能容忍这种情况。

因此，引用论文中给出的定义比我上面所说的要严格得多。

例如，考虑纯Prolog 程序：

现在我们处于以下情况：

这显然违反了在完全相同的条件下成功的属性，因为其中一个查询根本不再成功。

因此我的问题是：我们是否应该称上述程序不坚定？请解释坚定性背后的意图及其在现有文献中的定义、其与逻辑纯度的关系以及相关的终止概念，以证明您的回答是正确的。