标签: steadfastness

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

到目前为止,我一直坚持 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.

这个问题的一个很好的解决方案是依靠 …

prolog non-termination logical-purity steadfastness

12
推荐指数
1
解决办法
296
查看次数