坚定性:定义及其与逻辑纯度和终止的关系

Question

到目前为止,我一直坚持 Prolog程序意味着:

如果对于一个查询Q,有一个subterm S,使得存在一个术语T,使?- S=T, Q. 成功虽然?- Q, S=T. 失败,然后通过调用一个谓词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. % wrong!

而交换目标产生了正确的答案:

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

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

integer_integer_maximum(X, Y, M) :-
        M #= max(X, Y).

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

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

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

| ?- X in 0..2, Y in 3..4, integer_integer_maximum(X, Y, M).
X in 0..2,
Y in 3..4,
M in 3..4 ? ;
no

---

现在由Covington等人撰写的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).
true.

?- nat(X), X = 0.
nontermination

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

因此我的问题是:我们是否应该称上述计划不坚定？请证明你的答案,并在现有文献中解释坚定性及其定义背后的意图,与逻辑纯度的关系以及相关的终止概念.

Answer 1

在《序言的技巧》第 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.最初会成功..但你仍然会遇到其他问题..