prolog - 明确 Prolog 目标的 "deterministic success"

Question

某些 Prolog 目标的确定性成功问题已经一次又一次地出现在 - 至少 - 以下问题:

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 )

使用了不同的方法(例如，引发某些资源错误，或仔细查看 Prolog 顶层给出的确切答案)，但在我看来，它们都有些过时。

我正在寻找一种通用的、可移植的、符合 ISO 的方法来确定某些 Prolog 目标(成功)的执行是否留下了一些选择点。一些元谓词，也许？

你能提示我正确的方向吗？先感谢您!

Answer 1

大家好消息:setup_call_cleanup/3 (目前 ISO 的 draft proposal)让您以一种非常便携和美观的方式做到这一点。

见 example :
setup_call_cleanup(true, (X=1;X=2), Det=yes)
成功 Det == yes当没有更多选择点时。

编辑 :让我来说明这个结构的惊人之处，或者更确切地说是非常密切相关的谓词 call_cleanup/2 ，举个简单的例子:

中优CLP(B) documentation of SICStus Prolog , 我们在 labeling/1 的描述中找到一个非常强大的保证:

Enumerates all solutions by backtracking, but creates choicepoints only if necessary.

这确实是一个强有力的保证，一开始可能很难相信它总是成立。对我们来说幸运的是，在 Prolog 中制定和生成系统的测试用例来验证这些属性非常容易，本质上是使用 Prolog 系统来测试自己。

我们首先系统地描述 CLP(B) 中 bool 表达式的样子:

:- 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？因为它让我可以方便地描述特定深度的所有 bool 表达式(的一个子集)，从而公平地枚举它们。例如:

?- 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).

我们的 测试用例 (通过这个，我们实际上是指无限序列的小测试用例，我们可以很方便地用 Prolog 描述)现在旨在验证上述属性，即:

If there is a choice-point, then there is a further solution.

换句话说:

The set of solutions of labeling_nondet/1 is a proper subset of that of 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).

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

在 SWI-Prolog 中，多余的选择点很明显:

?- 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).