5

问题

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

这个程序是纯的吗？

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).

我可以用实现我的目标......

:- 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/1and !/0, 但是很难证明谓词是纯的。

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.
4

1 回答 1

4

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

请注意，内置的 ISOground/1与nonvar/1. 但是您似乎是在谈论when/2. 事实上，任何可接受的条件when/2都是尽可能纯粹的。所以这不仅适用于ground/1.

这个程序是纯的吗？

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

是的，就目前的纯洁感而言。也就是说，在同样的意义上被认为library(clpfd)是纯粹的。在逻辑编程和 Prolog 的早期，比如在 1970 年代，纯程序只有在其为真时成功，在其为假时失败。没有其他的。

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

虽然 Prolog I 明确报告了内置错误1，但随后的 DEC10-Prolog（例如 1978、1982 年）和 C-Prolog 都没有包含可靠的错误报告系统。相反，打印了一条消息并且谓词失败，从而将错误与逻辑错误混淆。从此时起，仍有warningProlog 标志的值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/2s 虽然完全正确，但现在对产生不一致的答案有很大贡献。毕竟上面写着：

是的，查询是真的，只要同样的查询是真的。

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

| ?- X #> 2, X #< 2.
no

Solibrary(clpfd)能够检测到这种不一致，而when/2必须等到它的论点成立。

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

对此没有明显的一般性答案。毕竟，许多有趣的约束理论是不可判定的。是的，非常无害的外观library(clpfd)允许您已经制定无法确定的问题！因此，我们将不得不忍受这种不包含解决方案的条件答案。

然而，一旦你得到一个纯粹的无条件解决方案，或者一旦你遇到真正的失败，你就知道这将成立。

list_length/2

您使用library(clpfd)的定义实际上比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 页。Interpréteur du langage de programmation Prolog。Rapport de DEA d'informatique appliquée，1973 年。在那里，一个内置的错误被一个从未解决的目标所取代。按照 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不是“多向”。

于 2015-01-17T17:29:21.870 回答