Verify_attributes 在 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.

上面的句子（由我突出显示）让我很困惑——而且还有很多:)

我一直认为统一是一个可以：

成功最通用的统一器（模变量重命名）
或失败。

但不确定是否成功？！

"feature"什么时候对约束求解器的实现者有用？

我想不出一个用例...请帮忙！

编辑

实际上，我认为（我的）求解器代码中的不确定性是一个错误，而不是一个功能。对于任何不确定性，都可以通过在 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

与第三个参数无关，returns一个目标，稍后执行。这第三个参数甚至在 XSB，这个回调没有第三个参数。我猜谜题的解法是这样的，verify_attributes/2钩子可能会留下一个选择点，后面的统一就是在这个选择点的延续上。

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

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

总结替代方案以补偿限制non-determinism：

verify_attributes/3:
verify_attributes/2 的 SICStus 变体中的第三个参数，它是 verify_attributes/3。那里的目标可以是 non-deterministic。这目标将看到实例化的变量。
attr_unify_hook/2:
这是 SWI-Prolog 挂钩。它将看到实例化的变量以及。但是一个小测试表明它允许 non-determinism:

    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 built-in。它具有相同的效果 SICStus 中的第三个参数，但可以同时手动调用执行 verify_attributes/2。

Verify_attributes 在 SICStus Prolog 中

Verify_attributes in SICStus Prolog

prolog

sicstus-prolog

clp

编辑