取得“确定性成功"Prolog 目标明确 [英] Making "deterministic success" of Prolog goals explicit
问题描述
某些 Prolog 目标的确定性成功问题在—至少—以下问题中一再出现:
使用了不同的方法(例如，引发某些资源错误，或仔细查看 Prolog 顶层给出的确切答案)，但在我看来，它们都有些过时.
我正在寻找一种通用的、可移植的且符合 ISO 的方法来确定某些 Prolog 目标(成功)的执行是否留下了一些选择点.也许是一些元谓词?
你能告诉我正确的方向吗?提前致谢！
大家好消息:setup_call_cleanup/3(目前是 草案提案 ISO)让您以一种非常便携和美观的方式做到这一点.
参见示例:
setup_call_cleanup(true, (X=1;X=2), Det=yes)
当没有更多选择点时，使用 Det == yes 成功.
编辑:让我用一个简单的例子来说明这个结构的神奇之处，或者更确切地说是非常密切相关的谓词call_cleanup/2:
在优秀的CLP(B) SICStus Prolog 的文档，我们在 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?因为它让我可以方便地描述(子集)所有特定深度的布尔表达式，从而公平地枚举它们.例如:
<预>?- 长度(Ls, _), 短语(sat(Sat), Ls).ls = [] ;ls = [],星期六 = a ;ls = [],周六 = ~_G475 ;Ls = [_G475],周六 = _G478+_G479.因此，我使用 DCG 仅表示在生成表达式时已经消耗了多少可用的令牌"，从而限制了结果表达式的总深度.
下一个，我们需要一个小辅助谓词 labeling_nondet/1 ，它完全作为标签/1 ，但如果仍然是一个选择点残留.这就是 call_cleanup/2 的用武之地:
labeling_nondet(Vs) :-差异(Det，真)，call_cleanup(标签(Vs)，Det=true).我们的测试用例(实际上，我们的意思是无限序列的小测试用例，我们可以很方便地用 Prolog 来描述)现在旨在验证上述属性，即:<块引用>
如果有一个选择点，那么还有一个进一步的解决方案.
换句话说:
<块引用>labeling_nondet/1的解集是labeling/1解集的真子集.
让我们描述一下上述性质的反例是什么样的:
<预>反例(周六):-长度(Ls，_)，短语(sat(Sat), Ls),term_variables(Sat, Vs),星期六(星期六)，setof(Vs, labeling_nondet(Vs), Sols),setof(Vs, labeling(Vs), Sols).现在我们使用这个可执行规范来找到这样一个反例.如果求解器按照文档工作，那么我们将永远找不到反例.但在这种情况下，我们立即得到:
<预>|?- 反例(周六).周六 = a+ ~_A,sat(_A=:=_B*a) ?;所以实际上该属性不成立.分解到本质，虽然下面的查询中没有更多的解决方案，但Det与true并不统一:
<代码>|?- sat(a + ~X), call_cleanup(labeling([X]), Det=true).X = 0 ?;不
在 SWI-Prolog 中，多余的选择点很明显:
<预>?- sat(a + ~X), 标签([X]).X = 0 ;假.我不是举这个例子来批评 SICStus Prolog 或 SWI 的行为:没有人真正关心是否在 labeling/1，尤其是在涉及通用量化变量的人工示例中(这对于使用 labeling/1 的任务来说是不典型的).
我我举这个例子是为了展示可以用如此强大的检查谓词测试记录和预期的保证是多么好和方便......
... 假设实现者有兴趣标准化他们的工作，以便这些谓词在不同的实现中实际上以相同的方式工作！细心的读者会注意到，在 SWI-Prolog 中使用反例搜索会产生完全不同的结果.
出乎意料的是，上述测试用例发现 SWI-Prolog 和 SICStus 的 call_cleanup/2 实现存在差异.在 SWI-Prolog (7.3.11) 中:
而 SICStus Prolog (4.3.2) 中的两个查询都失败.
这是一个非常典型的案例:一旦您对测试特定属性感兴趣，您会发现测试实际属性的过程中存在许多障碍.
在 ISO 草案提案中，我们看到:
<块引用>[清理目标]的失败被忽略.
在 call="nofollow 的 SICStus 文档中，我们看到:
<块引用>在执行一些副作用后，清理肯定会成功；否则，可能会导致意外行为.
在 SWI 变体中，我们看到:
<块引用>清理的成功或失败被忽略
因此，为了可移植性，我们实际上应该将 labeling_nondet/1 写成:
labeling_nondet(Vs) :-call_cleanup(labeling(Vs), Det=true),差异(Det，真).The matter of deterministic success of some Prolog goal has turned up time and again in—at least—the following questions:
- Reification of term equality/inequality
- Intersection and union of 2 lists
- Remove duplicates in list (Prolog)
- Prolog: How can I implement the sum of squares of two largest numbers out of three?
- Ordering lists with constraint logic programming)
Different methods were used (e.g., provoking certain resource errors, or looking closely at the exact answers given by the Prolog toplevel), but they all appear somewhat ad-hack to me.
I'm looking for a generic, portable, and ISO-conformant way to find out if the execution of some Prolog goal (which succeeded) left some choice-point(s) behind. Some meta predicate, maybe?
Could you please hint me in the right direction? Thank you in advance!
Good news everyone: setup_call_cleanup/3 (currently a draft proposal for ISO) lets you do that in a quite portable and beautiful way.
See the example:
setup_call_cleanup(true, (X=1;X=2), Det=yes)
succeeds with Det == yes when there are no more choice points left.
EDIT: Let me illustrate the awesomeness of this construct, or rather of the very closely related predicate call_cleanup/2, with a simple example:
In the excellent CLP(B) documentation of SICStus Prolog, we find in the description of labeling/1 a very strong guarantee:
Enumerates all solutions by backtracking, but creates choicepoints only if necessary.
This is really a strong guarantee, and at first it may be hard to believe that it always holds. Luckily for us, it is extremely easy to formulate and generate systematic test cases in Prolog to verify such properties, in essence using the Prolog system to test itself.
We start with systematically describing what a Boolean expression looks like in 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).
There are in fact many more cases, but let us restrict ourselves to the above subset of CLP(B) expressions for now.
Why am I using a DCG for this? Because it lets me conveniently describe (a subset of) all Boolean expressions of specific depth, and thus fairly enumerate them all. For example:
?- length(Ls, _), phrase(sat(Sat), Ls). Ls = [] ; Ls = [], Sat = a ; Ls = [], Sat = ~_G475 ; Ls = [_G475], Sat = _G478+_G479 .
Thus, I am using the DCG only to denote how many available "tokens" have already been consumed when generating expressions, limiting the total depth of the resulting expressions.
Next, we need a small auxiliary predicate labeling_nondet/1, which acts exactly as labeling/1, but is only true if a choice-point still remains. This is where call_cleanup/2 comes in:
labeling_nondet(Vs) :-
dif(Det, true),
call_cleanup(labeling(Vs), Det=true).
Our test case (and by this, we actually mean an infinite sequence of small test cases, which we can very conveniently describe with Prolog) now aims to verify the above property, i.e.:
If there is a choice-point, then there is a further solution.
In other words:
The set of solutions of
labeling_nondet/1is a proper subset of that oflabeling/1.
Let us thus describe what a counterexample of the above property looks like:
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).
And now we use this executable specification in order to find such a counterexample. If the solver works as documented, then we will never find a counterexample. But in this case, we immediately get:
| ?- counterexample(Sat). Sat = a+ ~_A, sat(_A=:=_B*a) ? ;
So in fact the property does not hold. Broken down to the essence, although no more solutions remain in the following query, Det is not unified with true:
| ?- sat(a + ~X), call_cleanup(labeling([X]), Det=true).
X = 0 ? ;
no
In SWI-Prolog, the superfluous choice-point is obvious:
?- sat(a + ~X), labeling([X]). X = 0 ; false.
I am not giving this example to criticize the behaviour of either SICStus Prolog or SWI: Nobody really cares whether or not a superfluous choice-point is left in labeling/1, least of all in an artificial example that involves universally quantified variables (which is atypical for tasks in which one uses labeling/1).
I am giving this example to show how nicely and conveniently guarantees that are documented and intended can be tested with such powerful inspection predicates...
... assuming that implementors are interested to standardize their efforts, so that these predicates actually work the same way across different implementations! The attentive reader will have noticed that the search for counterexamples produces quite different results when used in SWI-Prolog.
In an unexpected turn of events, the above test case has found a discrepancy in the call_cleanup/2 implementations of SWI-Prolog and SICStus. In 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.
whereas both queries fail in SICStus Prolog (4.3.2).
This is the quite typical case: Once you are interested in testing a specific property, you find many obstacles that are in the way of testing the actual property.
In the ISO draft proposal, we see:
Failure of [the cleanup goal] is ignored.
In the SICStus documentation of call_cleanup/2, we see:
Cleanup succeeds determinately after performing some side-effect; otherwise, unexpected behavior may result.
And in the SWI variant, we see:
Success or failure of Cleanup is ignored
Thus, for portability, we should actually write labeling_nondet/1 as:
labeling_nondet(Vs) :-
call_cleanup(labeling(Vs), Det=true),
dif(Det, true).
这篇关于取得“确定性成功"Prolog 目标明确的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
