在 SICStus Prolog 中验证_属性

Question

属性变量允许扩展统一。以下是关于该界面的晦涩细节。 让我们切入正题吧！

在 sicstus-prolog 中 库（atts）提供使用属性变量的谓词。 我想我明白了 SICStus Prolog 用户手册页面（atts） 所说的内容，除了关于

verify_attributes(-Var, +Value, -Goals)

的一个细节：

[...] verify_attributes/3 在 Var 实际绑定到 Value 之前被调用。如果失败，则视为统一失败。 它可能会不确定地成功，在这种情况下，统一可能会回溯以给出另一个答案。预计会在目标中返回在 Var 绑定到 Value 后要调用的目标列表。最后，在调用进球后，所有在 Var 上被阻挡的进球都会被调用。

上面这句话（由我突出显示）让我很困惑——而且也很困惑:)

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

• 成功使用最通用的统一器（模变量重命名）

• 或失败。

但是不确定会成功吗？！

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

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

---

编辑

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

Goals

中返回一些析取来轻松模拟。

Answer 1

您在 XSB 中发现了相同的行为：

验证属性（-Var，+值）
每当 属性变量 Var（至少有一个属性）即将 绑定到值（非变量项或另一个属性 多变的）。当Var要绑定到Value时，一个特殊的中断 调用属性变量中断被触发，然后XSB的 中断处理程序（用 Prolog 编写）调用 verify_attributes/2。如果它 失败，则视为统一失败。可能会成功 不确定性，在这种情况下，统一可能会倒退 给出另一个答案。
http://xsb.sourceforge.net/shadow_site/manual2/node4.html

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

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

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

总结一下弥补非确定性的替代方案：

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

• attr_unify_hook/2：
  这是 SWI-Prolog 挂钩。它将看到变量被实例化 以及。但一个小测试表明它允许非确定性：

    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.