prolog - `setup_call_cleanup/3` 是否可移植地检测确定性？

Question

有很详细的Draft proposal for setup_call_cleanup/3 .

让我引用我的问题的相关部分:

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(S=1,G=2,write(S+G)).
   Succeeds, unifying S = 1, G = 2.
   Either: outputs '1+2'
   Or: outputs on backtracking '1+_' prior to failure.
   Or (?): outputs on backtracking '1+2' prior to failure.

根据我的理解，这基本上是因为统一是可回溯的目标；它只是在重新执行时失败。因此它是由实现来决定是否调用清理第一次执行后(因为将不再有可观察到的目标的影响)，或推迟到第二次执行目标现在失败了。

所以在我看来这不能用来检测决定论可移植。只有一些内置结构，例如 true、fail、!等等确实是不可回溯的。

是否有其他方法可以在不执行目标两次的情况下检查确定性？我目前正在使用 SWI-prolog 的 deterministic/1，但我当然会重视可移植性。

Answer 1

没有。 setup_call_cleanup/3 无法以可移植的方式检测确定性。因为这会限制实现的自由。系统有不同的方式来实现索引。他们有不同的权衡。有些只有第一个参数索引，有些则不止于此。但提供“更好”索引的系统的行为通常相当随机。有些系统仅对非变量术语进行索引，其他系统也允许在头部仅具有变量的子句 - 前提是它是最后一个子句。有些人可能会使用 safe tests prior to cuts 进行“手动”选择点回避。而其他人则忽略了这一点。简而言之，这确实是一个非功能性问题，在这方面坚持可移植性就等于减慢系统速度。

但是，仍然成立的是:如果 setup_call_cleanup/3 检测到确定性，那么就不再需要使用第二个目标来确定确定性!因此它可以用来更有效地实现确定性检测。然而，在一般情况下，您必须执行一个目标两次。

current definition setup_call_cleanup/3 的设计还允许实现动态删除不必要的选择点。

可以想象(我没有见过这样的实现)，在Call成功并且内部存在选择点时，实现可以检查当前选择点并删除它们(如果确定性可以)检测到。另一种可能性可能是在两者之间执行一些异步垃圾收集。当前规范不排除所有这些选项。目前尚不清楚它们是否会被实现，但一旦某些应用程序依赖于此类功能，就有可能实现。这种情况在 Prolog 中已经发生过几次，所以重复并不完全是幻想。事实上，我正在考虑help DCGs的特殊情况。变得更加坚定。谁知道呢，也许你会走那条路!

以下是 SWI 中的索引如何取决于先前查询的历史记录的示例:

?- [user].
p(_,a). p(_,b). end_of_file.

true.

?- p(1,a).
true ;
false.

?- p(_,a).
true.

?- p(1,a).
true.       % now, it's determinate!

下面是一个示例，说明第二个参数的索引如何严格弱于第一个参数的索引:

?- [user].
q(_,_). q(0,0). end_of_file.

true.

?- q(X,1).
true ;           % weak
false.

?- q(1,X).
true.