明确 "deterministic success" 的 Prolog 目标

Question

某些 Prolog 目标的确定性成功问题已经反复出现，至少出现在以下问题中：

Reification of term equality/inequality
Intersection and union of 2 lists
Remove duplicates in list (Prolog)
Ordering lists with constraint logic programming)

使用了不同的方法（例如，引发某些资源错误，或仔细查看 Prolog 顶层给出的确切答案），但它们对我来说都显得有点 ad-hack。

我正在寻找一种通用的、可移植的和符合 ISO 标准的方法来查明某些 Prolog 目标（已成功）的执行是否留下了一些选择点。也许是一些元谓词？

你能给我指明正确的方向吗？提前致谢！

Answer 1

大家好消息：setup_call_cleanup/3（目前是 draft proposal ISO）让你以一种非常便携和漂亮的方式做到这一点。

参见 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) 中的样子开始：

:- 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 仅表示在生成表达式时已经消耗了多少可用 "tokens"，限制了生成表达式的总深度。

接下来，我们需要一个小的辅助谓词 labeling_nondet/1，它的作用与 labeling/1 完全相同，但只有在选择点 仍然存在时才为真 .这是 call_cleanup/2 的用武之地：

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

现在我们使用这个可执行规范来找到这样一个反例。如果求解器按照记录工作，那么我们将永远找不到反例。但是在这种情况下，我们立即得到：

| ?- 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的行为：没有人真正关心[=18=中是否留下了多余的选择点]，至少在涉及普遍量化变量的人工示例中（这对于使用 labeling/1 的任务来说是非典型的）。

我 am 给出这个例子是为了展示如何用如此强大的检查谓词来测试记录和预期的保证是多么的好和方便...

...假设实现者有兴趣标准化他们的工作，以便这些谓词实际上在不同的实现中以相同的方式工作！细心的reader会注意到在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).
false.

而 SICStus Prolog (4.3.2) 中的两个查询 都失败了 。

这是一个非常典型的案例：一旦您对测试特定的属性感兴趣，您就会发现测试实际属性.

的过程中存在许多障碍。

在 ISO draft proposal 中，我们看到：

Failure of [the cleanup goal] is ignored.

在 call_cleanup/2 的 SICStus 文档中，我们看到：

Cleanup succeeds determinately after performing some side-effect; otherwise, unexpected behavior may result.

而在 SWI variant 中，我们看到：

Success or failure of Cleanup is ignored

因此，为了便于移植，我们实际上应该将 labeling_nondet/1 写成：

labeling_nondet(Vs) :-
        call_cleanup(labeling(Vs), Det=true),
        dif(Det, true).

Answer 2

setup_call_cleanup/3 不能保证它检测到确定性，即目标成功时缺少选择点。 7.8.11.1 描述 draft proposal 只说：

c) The cleanup handler is called exactly once; no later than
upon failure of G. Earlier moments are:
If G is true or false, C is called at an implementation
dependent moment after the last solution and after the last
observable effect of G.

所以目前没有要求：

setup_call_cleanup(true, true, Det=true)

Returns 首先是 Det=true。这也反映在 draf proposal 给出的测试用例 7.8.11.4 示例中，我们发现一个测试用例说：

setup_call_cleanup(true, true, X = 2).
Either: Succeeds, unifying X = 2.
Or: Succeeds.

因此，它既是检测确定性又不检测确定性的有效实现。

明确 "deterministic success" 的 Prolog 目标

Making "deterministic success" of Prolog goals explicit

prolog