4

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

在 库（atts）中提供了使用属性变量的谓词。我想我得到了SICStus Prolog User's Manual page for library(atts)所说的内容，除了关于以下内容的一个细节verify_attributes(-Var, +Value, -Goals)：

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

上面的句子（由我突出显示）让我很困惑——也很困惑：）

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

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

  • 或失败。

却无缘无故的成功？！

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

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

编辑

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

4

1 回答 1

2

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

verify_attributes(-Var, +Value)
每当属性变量 Var（具有至少一个属性）即将绑定到 Value（非变量项或另一个属性变量）时，都会调用此谓词。当 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 中，因为缺少第三个参数。如果您在验证挂钩中不允许非确定性，则需要提供替代方案。

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

  • verify_attributes/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.
  • sys_assume_cont/1：
    这是内置的 Jekejeke Prolog。它与 SICStus 中的第三个参数具有相同的效果，但可以在执行 verify_attributes/2 时手动调用。
于 2019-06-28T22:56:38.953 回答