prolog - SICStus Prolog 中的验证属性

Question

属性变量允许扩展统一。以下是关于界面的神秘细节。让我们直奔主题吧!

在 sicstus-prolog
library(atts) 提供了使用属性变量的谓词。
我想我明白了SICStus Prolog User's Manual page for library(atts)说，除了关于 verify_attributes(-Var, +Value, -Goals) 的一个细节:

[...] verify_attributes/3 is called before Var has actually been bound to Value. If it fails, the unification is deemed to have failed. It may succeed nondeterminately, in which case the unification might backtrack to give another answer. It is expected to return, in Goals, a list of goals to be called after Var has been bound to Value. Finally, after calling Goals, any goals blocked on Var are called.

上面的句子(由我突出显示)让我很困惑——也很困惑:)

我一直认为统一是一个程序，可以:

成功使用最通用的统一器(模变量重命名)

或失败。

却无缘无故的成功？!

约束求解器的实现者何时使用过该“功能”？

我想不出一个用例……请帮忙!

编辑

实际上，我认为(我的)求解器代码中的不确定性是一个错误，而不是一个特性。对于任何不确定性，都可以通过在 Goals 中返回一些析取来轻松模拟。 .

Answer 1

您会在 XSB 中发现相同的行为:

verify_attributes(-Var, +Value)
This predicate is called whenever an attributed variable Var (which has at least one attribute) is about to be bound to Value (a non-variable term or another attributed variable). When Var is to be bound to Value, a special interrupt called attributed variable interrupt is triggered, and then XSB's interrupt handler (written in Prolog) calls verify_attributes/2. If it fails, the unification is deemed to have failed. It may succeed non-deterministically, in which case the unification might backtrack to give another answer.
http://xsb.sourceforge.net/shadow_site/manual2/node4.html

它与返回目标的第三个参数无关，
稍后执行。这第三个参数甚至在
XSB，这个回调中没有这样的第三个参数。我猜谜语的解决方案是这样的，verify_attributes/2 钩子(Hook)可能会留下一个选择点，而随后的统一是这个选择点的延续。

这样在回溯期间，再次尝试选择点。和
这意味着随后的统一被撤消，然后
再试一次，以防选择点提供进一步的解决方案。通过巧妙地组织如何调用回调，我想每个 Prolog 系统都可以实现这一点，因为 Prolog 系统应该支持选择点。

但是由于缺乏用例也可能没有它。 freeze/2 和 when/2 都不需要它，因为它们使用实例化变量。典型的 CLP(X) 也不需要它，因为选择点是不需要的。但它可能存在于 XSB 中，因为缺少第三个参数。如果您在验证 Hook 中不允许非确定性，则需要提供替代方案。

总结替代方案以弥补禁止非确定性:

验证属性/3:
verify_attributes/2 的 SICStus 变体中的第三个参数，它
是 verify_attributes/3。那里的目标可能是不确定的。这
目标将看到实例化的变量。

attr_unify_hook/2:
这是 SWI-Prolog 钩子(Hook)。它将看到实例化的变量
也是。但是一个小测试表明它允许不确定性:

    Welcome to SWI-Prolog (threaded, 64 bits, version 8.1.4)

    ?- [user].
    |: foo:attr_unify_hook(_,_) :- write('a'), nl.
    |: foo:attr_unify_hook(_,_) :- write('b'), nl.
    |: 
    % user://1 compiled 0.01 sec, 2 clauses
    true.

    ?- put_attr(X, foo, 1), X=2.
    a
    X = 2 ;
    b
    X = 2.

sys_assume_cont/1 :
这是内置的 Jekejeke Prolog。它具有相同的效果
SICStus 中的第三个参数，但可以手动调用
执行 verify_attributes/2。