Tud*_*riu 5 prolog logical-purity
这个问题
我有一个与逻辑纯度有关的问题.
这个节目是纯粹的吗？
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,后来是很难证明谓词是纯粹的.
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.
\n\nwhen/2 和 ground/1 的逻辑纯度
\n
请注意，内置的 ISO 与 一样ground/1不纯nonvar/1。\n但似乎您正在谈论 的条件when/2。事实上，任何可接受的条件when/2都是尽可能纯粹的。所以这不仅适用于ground/1.
\n\n这个程序纯粹吗？
\nRun Code Online (Sandbox Code Playgroud)\nwhen(ground(X), X > 2).\n
是的，就目前意义上的纯粹而言。library(clpfd)也就是说，与认为纯粹的含义完全相同。在逻辑编程和 Prolog 的早期阶段，比如 20 世纪 70 年代，纯粹的程序只能是如果为真则成功，为假则失败的程序。没有其他的。
然而，今天，我们接受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），这会导致尝试执行未定义的谓词以打印警告并失败。
那么问题在哪里呢？考虑
\n?- when(ground(X), X> 2), when(ground(X), X < 2).\n when(ground(X), X>2), when(ground(X), X<2).\n这些when/2虽然完全正确，但现在在很大程度上导致了答案的不一致。毕竟，上面写着：
\n\n是的，只要同样的查询为真，该查询就是真的。
\n
将此与 SICStus 或 SWI 进行对比library(clpfd)：
?- X #> 2, X #< 2.\n false.\n因此library(clpfd)能够发现这种不一致，而when/2必须等到其论点得到证实。
获得这样的条件答案通常非常令人困惑。事实上，在许多情况下，许多人更喜欢更普通的实例化错误，而不是更干净的错误。
\n对此没有明显的一般答案。毕竟，许多有趣的约束理论都是不可判定的。是的，看起来无害的东西library(clpfd)已经可以让你提出无法解决的问题了！因此，我们将不得不忍受这种不包含解决方案的条件答案。
然而，一旦你得到了一个纯粹的无条件解决方案，或者一旦你遇到了真正的失败，你就知道这将会成立。
\nlist_length/2您使用的定义实际上比Prolog 序言所商定的library(clpfd)终止稍微好一些。考虑：
?- N in 1..3, list_length(L, N).\n此外，目标length(L,L)会以非常自然的方式产生类型错误。也就是说，没有任何明确的测试。
您使用的版本when/2有一些“自然”的不规则之处，例如length(L,0+0)失败但length(L,1+0)成功。否则，仅通过构造 \xe2\x80\x94 似乎就可以了。
freeze/2：plus(X, Y, Z) :-\n ( integer(X), integer(Y), ( var(Z) ; integer(Z) )\n -> Z is X+Y\n ; freeze(_,erreur(plus(X,Y,Z)))\n ).\n所以plus/3不是“多向”。