when/2 和 ground/1 的逻辑纯度 [英] Logical purity of when/2 and ground/1

问题描述

问题

我有一个关于逻辑纯度的问题.

I have a question related to logical purity.

这个程序是纯的吗?

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

关于上下文的一些[ir]相关细节

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

I'm trying to write pure predicates with good termination properties. For instance, I want to write a predicate list_length/2 that describes the relation between a list and its length. I want to achieve the same termination behaviour as the built-in predicate length/2.

我的问题试图找出以下谓词是否纯:

My question seeks to find if the following predicate is pure:

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，然后是 很难证明谓词是纯的.

... or I can use var/1, nonvar/1 and !/0, but then is hard to prove that the predicate is pure.

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.

推荐答案

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

Logical purity of when/2 and ground/1

注意有 ISO 内置 ground/1 和 nonvar/1 一样不纯.但您似乎更喜欢谈论 when/2 的条件.事实上，when/2 的任何可接受的条件都是尽可能纯的.所以这不仅适用于 ground/1.

Note that there is the ISO built-in ground/1 which is just as impure as nonvar/1. But it seems you are rather talking about the conditions for when/2. In fact, any accepted condition for when/2 is as pure as it can get. So this is not only true for ground/1.

这个程序是纯的吗?

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

是的，就目前的纯洁性而言.也就是说，在完全相同的意义上，将 library(clpfd) 视为纯的.在逻辑编程和 Prolog 的早期，比如说在 1970 年代，纯程序只会在它为真时成功，如果为假则失败.没有别的.

Yes, in the current sense of purity. That is, in the very same sense that considers library(clpfd) as pure. In the very early days of logic programming and Prolog, say in the 1970s, a pure program would have been only one that succeeds if it is true and fails if it is false. Nothing else.

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

However, today, we accept that ISO errors, like type errors are issued in place of silent failure. In fact, this makes much more sense from a practical point of view. Think of X = non_number, when(ground(X), X > 2 ). Note that this error system was introduced relatively late into Prolog.

虽然 Prolog 我明确报告了内置错误¹随后的 DEC10-Prolog(例如 1978、1982)和 C-Prolog 都没有包含可靠的错误报告系统.相反，打印了一条消息并且谓词失败，从而将错误与逻辑错误混淆.从此时起，仍然存在 Prolog 标志 unknown(ISO/IEC 13211-1:1995 中的 7.11.2.4)的值 warning 导致尝试执行未定义的谓词打印警告并失败.

While Prolog I reported errors of built-ins explicitly¹ the subsequent DEC10-Prolog (as of, e.g. 1978, 1982) nor C-Prolog did not contain a reliable error reporting system. Instead, a message was printed and the predicate failed thus confusing errors with logical falsity. From this time, there is still the value warning of the Prolog flag unknown (7.11.2.4 in ISO/IEC 13211-1:1995) which causes the attempt to execute an undefined predicate to print a warning and fail.

那么问题在哪里?考虑

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

这些 when/2 虽然完全正确，但现在对产生不一致的答案有很大贡献.毕竟，上面写着:

These when/2s, while perfectly correct, now contribute a lot to producing inconsistencies as answers. After all, above reads:

是的，查询是正确的，提供完全相同的查询是正确的.

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

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

Contrast this to SICStus' or SWI's library(clpfd):

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

所以 library(clpfd) 能够检测到这种不一致，而 when/2 必须等到它的参数成立.

So library(clpfd) is capable of detecting this inconsistency, whereas when/2 has to wait until its argument is ground.

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

Getting such conditional answers is often very confusing. In fact, many prefer in many situations a more mundane instantiation error to the somewhat cleaner when.

对此没有明显的通用答案.毕竟，许多有趣的约束理论都是不可判定的.是的，看起来非常无害的 library(clpfd) 已经允许您制定无法确定的问题！因此，我们将不得不接受这些不包含解决方案的有条件的答案.

There is no obvious general answer to this. After all, many interesting theories for constraints are undecidable. Yes, the very harmless-looking library(clpfd) permits you to formulate undecidable problems already! So we will have to live with such conditional answers that do not contain solutions.

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

However, once you get a pure unconditional solution or once you get real failure you do know that this will hold.

您使用 library(clpfd) 的定义实际上稍微好一些 w.r.t.终止于序言序言同意.考虑:

Your definition using library(clpfd) is actually slightly better w.r.t. termination than what has been agreed upon for the Prolog prologue. Consider:

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

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

Also, the goal length(L,L) produces a type error in a very natural fashion. That is, without any explicit tests.

您使用 when/2 的版本有一些自然"的不规则性，例如 length(L,0+0) 失败但 length(L,1+0) 成功.否则它似乎没问题—仅靠施工.

Your version using when/2 has some "natural" irregularities, like length(L,0+0) fails but length(L,1+0) succeeds. Otherwise it seems to be fine — by construction alone.

1) 最早的记录是 G. Battani, H. Meloni 的第 9 页.Interpréteur du langage de programmation Prolog.报告 D.E.A.d'informatique appliquée，1973 年.在那里，一个内置的错误被一个从未解决的目标所取代.在当前条款中，II-3-6 a 的 plus/3，p.13 将在当前系统中使用 freeze/2:

1) The earliest account is on p.9 of G. Battani, H. Meloni. Interpréteur du langage de programmation Prolog. Rapport de D.E.A. d'informatique appliquée, 1973. There, a built-in in error was replaced by a goal that was never resolved. In current terms plus/3 of II-3-6 a, p.13 would be in current systems with 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 不是多向".

这篇关于when/2 和 ground/1 的逻辑纯度的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！