坚定性:定义及其与逻辑纯度和终止的关系 [英] Steadfastness: Definition and its relation to logical purity and termination

问题描述

到目前为止，我一直认为 Prolog 程序中的坚定意味着:

<块引用>

如果，对于查询Q，有一个子项S，使得有一个项T 使得?- S=T, Q. succeed 尽管 ?- Q, S=T. fails，然后调用谓词之一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.错误.

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

<预>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，M 在 3..4 中?;不

<小时>

现在是 Covington 的论文 Prolog 编码指南等人由该概念的发明者合着，Richard O'Keefe 包含以下部分:

<块引用>

5.1 谓词必须坚定不移.

任何体面的谓词都必须是坚定的"，即，如果其输出变量已经被实例化为输出值，则必须正确工作(O'Keefe 1990).

也就是说，

?- foo(X), X = x.

和

?- foo(x).

必须在完全相同的条件下成功并具有相同的副作用.不这样做只对调用模式为的辅助谓词是可容忍的受主谓词的强烈约束.

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

例如，考虑 pure Prolog 程序:

<预>nat(s(X)) :- nat(X).自然(0).

现在我们处于以下情况:

<预>?- nat(0).真的.?- nat(X), X = 0.不终止

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

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

解决方案

在序言的工艺"第 96 页中，Richard O'Keef 说即使查询具有意外形式，我们也称其为拒绝给出错误答案的属性(通常为我们通常认为的输入提供值*)坚定不移'

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

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

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

但是我认为首先使用基本情况而不是递归情况是明智的，这样 nat(X), X = 0. 最初会成功......但你会还有其他问题..

So far, I have always taken steadfastness in Prolog programs to mean:

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.

Intuitively, I thus took steadfastness to mean that we cannot use instantiations to "trick" a predicate into giving solutions that are otherwise not only never given, but rejected. Note the difference for nonterminating programs!

In particular, at least to me, logical-purity always implied steadfastness.

---

Example. To better understand the notion of steadfastness, consider an almost classical counterexample of this property that is frequently cited when introducing advanced students to operational aspects of Prolog, using a wrong definition of a relation between two integers and their maximum:

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

A glaring mistake in this—shall we say "wavering"—definition is, of course, that the following query incorrectly succeeds:

?- M = 0, integer_integer_maximum(0, 1, M).
M = 0. % wrong!

whereas exchanging the goals yields the correct answer:

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

A good solution of this problem is to rely on pure methods to describe the relation, using for example:

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

This works correctly in both cases, and can even be used in more situations:

?- 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

---

Now the paper Coding Guidelines for Prolog by Covington et al., co-authored by the very inventor of the notion, Richard O'Keefe, contains the following section:

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.

Thus, the definition given in the cited paper is considerably stricter than what I stated above.

For example, consider the pure Prolog program:

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

Now we are in the following situation:

?- nat(0).
true.

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

This clearly violates the property of succeeding under exactly the same conditions, because one of the queries no longer succeeds at all.

Hence my question: Should we call the above program not steadfast? Please justify your answer with an explanation of the intention behind steadfastness and its definition in the available literature, its relation to logical-purity as well as relevant termination notions.

解决方案

In 'The craft of prolog' page 96 Richard O'Keef says 'we call the property of refusing to give wrong answers even when the query has an unexpected form (typically supplying values for what we normally think of as inputs*) steadfastness'

*I am not sure if this should be outputs. i.e. in your query ?- M = 0, integer_integer_maximum(0, 1, M). M = 0. % wrong! M is used as an input but the clause has been designed for it to be an output.

In nat(X), X = 0. we are using X as an output variable not an input variable, but it has not given a wrong answer, as it does not give any answer. So I think under that definition it could be steadfast.

A rule of thumb he gives is 'postpone output unification until after the cut.' Here we have not got a cut, but we still want to postpone the unification.

However I would of thought it would be sensible to have the base case first rather than the recursive case, so that nat(X), X = 0. would initially succeed .. but you would still have other problems..

这篇关于坚定性:定义及其与逻辑纯度和终止的关系的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！