SICStus Prolog 中的 Verify_attributes [英] Verify_attributes in SICStus Prolog

问题描述

属性变量允许扩展统一.以下是关于界面的神秘细节.让我们切入正题！

Attribute variables permit to extend unification. The following is about arcane details of the interface. Let's cut right to the chase!

在 sicstus-prologlibrary(atts) 提供使用属性变量的谓词.我想我明白了 SICStus Prolog 用户手册图书馆页面(atts) 说，除了关于 verify_attributes(-Var, +Value, -Goals) 的一个细节:

In sicstus-prolog library(atts) provides predicates for using attributed variables. I think I get what the SICStus Prolog User's Manual page for library(atts) says, except for one detail about verify_attributes(-Var, +Value, -Goals):

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

[...] 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.

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

The above sentence (highlighted by me) confused me—and a lot, too:)

我一直认为统一是一个程序:

I have always thought that unification is a procedure that could either:

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

• succeed with the most general unifier (modulo variable renaming)

或失败.

但不确定成功?！

约束求解器的实现者何时使用该功能"?

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

I can't think of a single use case... help please!

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

Actually, I regard non-determinacy in (my) solver code a bug—not a feature. For any non-determinacy can easily be emulated by returning some disjunction in Goals.

推荐答案

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

You find the same behaviour in XSB:

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

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钩子可能会留下一个选择点，后续的统一就在这个选择点的延续中.

It has nothing to do with the third parameter that returns a goal, to be executed later. This third parameter is even missing in XSB, there is no such third parameter in this call back. I guess the riddles solution is such, that the verify_attributes/2 hook might leave a choice point, and that the subsequent unification is in the continuation of this choice point.

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

So that during backtracking, the choice point is tried again. And this means that the subsequent unifications are undone, and then tried again as well in case the choice point provides a further solution. With a clever organization of how the call back is called, I guess every Prolog system could implement that, since Prolog systems should champion choice points.

但由于缺乏用例也可能没有它.freeze/2 和 when/2 都不需要它，因为它们与实例化的变量一起工作.典型的 CLP(X) 也不需要它，因为选择点是不需要的.但它可能存在于 XSB 中，因为缺少第三个参数.如果您在 verify 钩子中禁止非确定性，则需要提供替代方案.

But because of lack of use cases might also do without it. Neither freeze/2 nor when/2 require it, since they work with the instantiated variable. Nor do the typical CLP(X) require it, since choice points are unwanted. But it might exist in XSB, since the third argument is missing. If you disallow non-determinism in the verify hook, you need to provide alternatives.

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

To sum up the alternatives to compensate for barring non-determinism:

• verify_attributes/3:
  verify_attributes/2 的 SICStus 变体中的第三个参数，其中是 verify_attributes/3.那里的目标可能是不确定的.这目标将看到实例化的变量.

• verify_attributes/3:
  The third argument in SICStus variant of verify_attributes/2, which is verify_attributes/3. The goals there can be non-deterministic. The goals will see the variable instantiated.

attr_unify_hook/2:
这是 SWI-Prolog 钩子.它将看到实例化的变量以及.但是一个小测试表明它允许非确定性:

attr_unify_hook/2:
This is the SWI-Prolog hook. It will see the variable instantiated as well. But a small test shows that it allows 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.它具有相同的效果SICStus 中的第三个参数，但可以手动调用，而执行 verify_attributes/2.

这篇关于SICStus Prolog 中的 Verify_attributes的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！