Verify_attributes в SICStus Prolog

Переменные атрибутов позволяют расширить унификацию. Далее мы поговорим о загадочных деталях интерфейса. Давайте перейдем к делу!

В библиотеке sicstus-prolog (atts ) предоставляет предикаты для использования переменных с атрибутами. Думаю, я понял то, что SICStus Prolog User's Manual на странице библиотеки (atts) говорится, за исключением одной детали о verify_attributes(-Var, +Value, -Goals):

[...] verify_attributes / 3 вызывается до того, как Var будет фактически привязан к Value. В случае неудачи объединение считается неудачным. Успех может быть неопределенным, и в этом случае объединение может вернуться назад, чтобы дать другой ответ. Ожидается, что в Goals он вернет список целей, которые будут вызываться после того, как Var будет привязан к Value. Наконец, после вызова Goals вызываются все голы, заблокированные на Var.

Вышеупомянутое предложение (выделенное мной) смутило меня и многое тоже :)

Я всегда думал, что объединение - это процедура, которая может либо:

  • добиться успеха с самым общим объединителем (переименование переменной по модулю)

  • или потерпеть неудачу.

Но добиться успеха неопределенно ?!

Когда эта "функция" когда-либо была использована разработчиками решателей ограничений?

Я не могу придумать ни одного варианта использования ... помогите, пожалуйста!

РЕДАКТИРОВАТЬ

На самом деле, я считаю неопределенность в (моем) коде решателя ошибкой, а не особенностью. Ибо любую неопределенность можно легко смоделировать, вернув некоторую дизъюнкцию в Goals.


clp prolog sicstus-prolog
person repeat    schedule 25.06.2019    source источник
comment
... нет! freeze(X, ( Y = 1 ; Y = 2 ) )   -  person false    schedule 25.06.2019
comment
@ложный. Что ты имеешь в виду? Есть Goals аргумент в пользу незамороженных голов ...   -  person repeat    schedule 25.06.2019
comment
@ложный. Да, ваш второй пример верен: по мануалу Y может быть унифицирован при размораживании X. Но это легко сделать с помощью Goals = [(Y = 1 ; Y = 2)].   -  person repeat    schedule 25.06.2019
comment
@ложный. Может быть, clpq, clpr или clpb он понадобится, а я не получаю его в своих clpfd очках :)   -  person repeat    schedule 25.06.2019

Ответы (1)


arrow_upward
2
arrow_downward

Вы обнаружите такое же поведение в 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, вам нужно предоставить альтернативы.

Подытоживая альтернативы для компенсации запрета недетерминизма:

  • 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.
person Mostowski Collapse    schedule 28.06.2019