取得“确定性成功"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) 中:?- dif(Det, true), call_cleanup(true, Det=true).dif(Det, true).?- call_cleanup(true, Det=true), dif(Det, true).假.而 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/inequalityIntersection and union of 2 listsRemove 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: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.:In other words: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 ? ;noIn 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:In the SICStus documentation of call_cleanup/2, we see:And in the SWI variant, we see:Thus, for portability, we should actually write labeling_nondet/1 as:labeling_nondet(Vs) :- call_cleanup(labeling(Vs), Det=true), dif(Det, true). 这篇关于取得“确定性成功"Prolog 目标明确的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！