一些Prolog目标确定性成功的问题一次又一次地出现 - 至少 - 以下问题:
使用了不同的方法(例如,引发某些资源错误,或仔细查看Prolog toplevel给出的确切答案),但它们对我来说都有点不合适.
我正在寻找一种通用的,可移植的,符合ISO的方式来查明某些Prolog目标(成功)的执行是否会留下一些选择点.有些元谓词,也许？
你能否向我提示正确的方向？先感谢您!
mat*_*mat 13
每个人都好消息:( setup_call_cleanup/3目前是ISO的提案草案)让你以一种非常便携和美观的方式做到这一点.
看例子:
setup_call_cleanup(true, (X=1;X=2), Det=yes)
Det == yes当没有剩余选择点时成功.
编辑:让我call_cleanup/2用一个简单的例子来说明这个构造的强大之处,或者更确切地说是非常密切相关的谓词:
在SICStus Prolog的优秀CLP(B)文档中,我们在描述中找到了labeling/1一个非常有力的保证:
通过回溯枚举所有解决方案,但仅在必要时创建选择点.
这确实是一个强有力的保证,起初可能很难相信它始终存在.对我们来说幸运的是,在Prolog中制定和生成系统测试用例非常容易,以验证这些属性,实质上是使用Prolog系统来测试自身.
我们首先系统地描述CLP(B)中的布尔表达式:
:- use_module(library(clpb)).
:- use_module(library(lists)).
sat(_) --> [].
sat(a) --> [].
sat(~_) --> [].
sat(X+Y) --> [_], sat(X), sat(Y).
sat(X#Y) --> [_], sat(X), sat(Y).
实际上还有更多的情况,但是现在让我们将自己局限于CLP(B)表达式的上述子集.
为什么我要使用DCG呢？因为它可以方便地描述特定深度的所有布尔表达式(的一个子集),因此可以相当地枚举它们.例如:
?- length(Ls, _), phrase(sat(Sat), Ls). Ls = [] ; Ls = [], Sat = a ; Ls = [], Sat = ~_G475 ; Ls = [_G475], Sat = _G478+_G479 .
因此,我仅使用DCG来表示在生成表达式时已经消耗了多少可用的"标记",从而限制了结果表达式的总深度.
接下来,我们需要一个小的辅助谓词labeling_nondet/1,它的作用完全如此labeling/1,但只有当选择点仍然存在时才会出现.这是call_cleanup/2进来的地方:
labeling_nondet(Vs) :-
dif(Det, true),
call_cleanup(labeling(Vs), Det=true).
我们的测试用例(通过这个,我们实际上意味着无限的小测试用例序列,我们可以非常方便地用Prolog描述)现在旨在验证上述属性,即:
如果有一个选择点,那么还有一个解决方案.
换一种说法:
这组解决方案
labeling_nondet/1是其中的一个适当的子集labeling/1.
因此,让我们描述一下上述属性的反例:
counterexample(Sat) :-
length(Ls, _),
phrase(sat(Sat), Ls),
term_variables(Sat, Vs),
sat(Sat),
setof(Vs, labeling_nondet(Vs), Sols),
setof(Vs, labeling(Vs), Sols).
现在我们使用这个可执行规范来找到这样一个反例.如果解算器按照记录的方式工作,那么我们永远不会找到反例.但在这种情况下,我们立即得到:
| ?- counterexample(Sat). Sat = a+ ~_A, sat(_A=:=_B*a) ? ;
所以其实属性并不能成立.虽然在以下查询中没有更多解决方案,但细分为本质,Det并不统一true:
| ?- sat(a + ~X), call_cleanup(labeling([X]), Det=true).
X = 0 ? ;
no
在SWI-Prolog中,多余的选择点是显而易见的:
?- sat(a + ~X), labeling([X]). X = 0 ; false.
我没有举出这个例子来批评SICStus Prolog或SWI的行为:没有人真正关心是否留下了多余的选择点labeling/1,尤其是涉及普遍量化变量的人为例子(这对任务来说是非典型的)在哪一个使用labeling/1).
我正在给这个例子来说明如何精美,方便地被记录在案,并打算保证能与这样强大的检测谓词来测试...
...假设实现者有兴趣标准化他们的工作,以便这些谓词在不同的实现中实际上以相同的方式工作!细心的读者会注意到,当在SWI-Prolog中使用时,搜索反例会产生完全不同的结果.
在意外的事件转变中,上述测试用例发现call_cleanup/2SWI-Prolog和SICStus 的实现存在差异.在SWI-Prolog(7.3.11)中:
?- dif(Det, true), call_cleanup(true, Det=true). dif(Det, true). ?- call_cleanup(true, Det=true), dif(Det, true). false.
而两个查询在SICStus Prolog(4.3.2)中都失败了.
这是一个非常典型的案例:一旦您对测试特定属性感兴趣,您就会发现许多阻碍测试实际属性的障碍.
在ISO 草案提案中,我们看到:
[清理目标]的失败被忽略.
在call_cleanup/2的SICStus文档中,我们看到:
在执行一些副作用后,清理成功; 否则,可能会导致意外行为.
在SWI变体中,我们看到:
清除成功或失败将被忽略
因此,为了便携性,我们应该写labeling_nondet/1为:
labeling_nondet(Vs) :-
call_cleanup(labeling(Vs), Det=true),
dif(Det, true).