prolog - when/2 和 ground/1 的逻辑纯度

Question

问题

我有一个与逻辑纯度相关的问题。

这个程序是纯粹的吗？

when(ground(X), X > 2).

有关上下文的一些[ir]相关详细信息

我正在尝试编写具有良好终止属性的纯谓词。例如，我想编写一个谓词 list_length/2 来描述列表与其长度之间的关系。我想实现与内置谓词 length/2 相同的终止行为。

我的问题旨在找出以下谓词是否是纯的:

list_length([], 0).
list_length([_|Tail], N):-
    when(ground(N), (N > 0, N1 is N - 1)),
    when(ground(N1), N is N1 + 1),
    list_length(Tail, N1).

<小时/>

我可以通过 clpfd 实现我的目标...

:- use_module(library(clpfd)).
:- set_prolog_flag(clpfd_monotonic, true).

list_length([], 0).
list_length([_|Tail], N):-
    ?(N) #> 0,
    ?(N1) #= ?(N) - 1,
    list_length(Tail, N1).

...或者我可以使用 var/1、nonvar/1 和 !/0，但随后是 hard证明谓词是纯的。

list_length([],0).
list_length([_|Tail], N):-
    nonvar(N), !,
    N > 0,
    N1 is N - 1,
    list_length(Tail, N1).
list_length([_|Tail], N):-
    list_length(Tail, N1),
    N is N1 + 1.

Answer 1

Logical purity of when/2 and ground/1

请注意，有 ISO 内置 ground/1 这和 nonvar/1 一样不纯。 。但看来你更多的是在谈论 when/2 的条件。事实上，任何接受的条件 when/2尽可能纯净。所以这不仅适用于 ground/1 .

Is this program pure?

when(ground(X), X > 2).

是的，就目前的纯粹而言。也就是说，与考虑 library(clpfd) 的意义完全相同。一样纯粹。在逻辑编程和 Prolog 的早期阶段，比如 20 世纪 70 年代，纯粹的程序只能是如果为真则成功，为假则失败的程序。没有别的了。

但是，今天，我们接受 ISO errors ，就像发出类型错误来代替静默失败一样。事实上，从实际角度来看，这更有意义。想想X = non_number, when(ground(X), X > 2 ) 。请注意，这个错误系统是相对较晚引入 Prolog 的。

虽然 Prolog 我明确地报告了内置错误¹，但随后的 DEC10-Prolog(例如 1978 年、1982 年)或 C-Prolog 均不包含可靠的错误报告系统。相反，打印了一条消息，并且谓词失败，从而将错误与逻辑错误混淆。从这个时候开始，仍然有值warning Prolog 标志 unknown (ISO/IEC 13211-1:1995 中的 7.11.2.4)这会导致尝试执行未定义的谓词以打印警告并失败。

那么问题在哪里呢？考虑一下

?- when(ground(X), X> 2), when(ground(X), X < 2).
   when(ground(X), X>2), when(ground(X), X<2).

这些when/2虽然完全正确，但现在在很大程度上导致了答案的不一致。毕竟，上面写着:

Yes, the query is true, provided the very same query is true.

将此与 SICStus 或 SWI 的 library(clpfd) 进行对比:

?- X #> 2, X #< 2.
   false.

所以library(clpfd)能够检测到这种不一致，而when/2必须等到其论点得到证实。

获得这样的条件答案通常非常令人困惑。事实上，在许多情况下，许多人更喜欢更普通的实例化错误，而不是更干净的错误。

对此没有明显的一般答案。毕竟，许多有趣的约束理论都是不可判定的。是的，看起来非常无害的library(clpfd)已经允许你提出不可判定的问题了!因此，我们将不得不忍受这种不包含解决方案的条件答案。

但是，一旦您获得纯粹的无条件解决方案或一旦您遇到真正的失败，您就知道这将成立。

list_length/2

您的定义使用 library(clpfd)实际上稍微好一点。终止比什么已经agreed upon为 Prolog 序言。考虑:

?- N in 1..3, list_length(L, N).

另外，目标length(L,L)以非常自然的方式产生类型错误。也就是说，没有任何明确的测试。

您的版本使用 when/2有一些“自然”的不规则性，例如 length(L,0+0)失败但是length(L,1+0)成功了。除此之外，它似乎还不错——仅通过构造。

<小时/>

1. 最早的记载是 G. Battani、H. Meloni 的第 9 页。 Prolog 编程语言解释器。 D.E.A. 关系d'informatique appliquée，1973。在那里，一个内置的错误被一个从 Unresolved 目标所取代。按照当前的术语，II-3-6 a 的 plus/3，第 13 页将在当前系统中为 freeze/2 :

plus(X, Y, Z) :-
       (  integer(X), integer(Y), ( var(Z) ; integer(Z) )
       -> Z is X+Y
       ;  freeze(_,erreur(plus(X,Y,Z)))
       ).

所以plus/3不是“多向的”。