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

Question

到目前为止，我一直都在踏实在 Prolog 程序中表示:

If, for a query Q, there is a subterm S, such that there is a term T that makes ?- S=T, Q. succeed although ?- Q, S=T. fails, then one of the predicates invoked by Q is not steadfast.

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

特别是，至少对我来说， logical-purity总是暗示着坚定。

示例 .为了更好地理解坚定性的概念，请考虑使用 向高级学生介绍 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。
假的。

不错 解决方案 这个问题要靠 纯描述关系的方法，例如:

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

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

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

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

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



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

5.1 Predicates must be steadfast.

Any decent predicate must be “steadfast,” i.e., must work correctly if its output variable already happens to be instantiated to the output value (O’Keefe 1990).

That is,

?- foo(X), X = x.

and

?- foo(x).

must succeed under exactly the same conditions and have the same side effects. Failure to do so is only tolerable for auxiliary predicates whose call patterns are strongly constrained by the main predicates.

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

例如，考虑 纯序言程序:

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

现在我们处于以下情况:

?- nat(0)。
真的。

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

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

因此我的问题是:我们应该称上述程序不坚定吗？请 证明 您的回答并解释了坚定不移的意图及其 定义 在现有文献中，它与 logical-purity 的关系以及相关的终止概念。

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.最初会成功.. 但你仍然会遇到其他问题..