12

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

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

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

特别是，至少对我来说，总是意味着坚定不移。

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

integer_integer_maximum(X, Y, Y) :-
        Y >= X,
        !.
integer_integer_maximum(X, _, X)。

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

?- M = 0, integer_integer_maximum(0, 1, M)。
M = 0. % 错误！

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

?- integer_integer_maximum(0, 1, M), M = 0.
 false。

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

integer_integer_maximum(X, Y, M) :-
        M #= 最大值（X，Y）。

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

?- integer_integer_maximum(0, 1, M), M = 0.
 false。

?- M = 0, integer_integer_maximum(0, 1, M)。
错误的。

| ?- X 在 0..2，Y 在 3..4，integer_integer_maximum(X, Y, M)。
X 在 0..2 中，
Y 在 3..4 中，
M 在 3..4 中？;
不

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

5.1 谓词必须坚定。

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

那是，

?- foo(X), X = x.

和

?- foo(x).

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

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

例如，考虑纯Prolog 程序：

nat(s(X)) :- nat(X)。
nat(0)。

现在我们处于以下情况：

?- nat(0)。
真的。

?- nat(X), X = 0。
不终止

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

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

4

1 回答 1

3

在“序言的工艺”第 96 页中，Richard O'Keef 说“即使查询具有意外的形式（通常为我们通常认为的输入提供值*），我们也将拒绝给出错误答案的属性称为稳定”

*我不确定这是否应该是输出。即在您的查询中，?- M = 0, integer_integer_maximum(0, 1, M). M = 0. % wrong!M 用作输入，但该子句已被设计为输出。

在nat(X), X = 0. 我们使用 X 作为输出变量而不是输入变量，但它没有给出错误的答案，因为它没有给出任何答案。所以我认为根据这个定义，它可能是坚定的。

他给出的一条经验法则是“将输出统一推迟到削减之后”。在这里我们没有削减，但我们仍然想推迟统一。

但是，我认为首先使用基本情况而不是递归情况是明智的，因此nat(X), X = 0.最初会成功..但您仍然会遇到其他问题..

于 2016-08-28T19:47:59.093 回答