Verify_attributes в Прологе SICStus - PullRequest
Новая
       80

Verify_attributes в Прологе SICStus

5 голосов
/ 25 июня 2019

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

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

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

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

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

  • успешно с наиболее общим унификатором (переименование переменной по модулю)

  • или сбой.

Но преуспеть не определенно ?!

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

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

EDIT

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

1 Ответ

2 голосов
/ 29 июня 2019

Вы найдете то же поведение в XSB:

verify_attributes (-Var, + Value)
Этот предикат вызывается всякий раз, когда атрибутируемая переменная Var (которая имеет хотя бы один атрибут) составляет околобыть привязанным к Value (не переменный термин или другая приписанная переменная).Когда Var должен быть привязан к Value, запускается специальное прерывание, называемое атрибутивной переменной, и затем обработчик прерываний XSB (написанный на прологе) вызывает verify_attributes / 2.Если это не удается, объединение считается потерпевшим неудачу.Он может завершиться недетерминированным образом, и в этом случае объединение может вернуться назад, чтобы дать другой ответ.
http://xsb.sourceforge.net/shadow_site/manual2/node4.html

Это не имеет ничего общего с третьим параметром, который возвращает цель, которая будетказнен позже.Этот третий параметр даже отсутствует в XSB, такого третьего параметра в этом обратном вызове нет.Я полагаю, что решение загадок таково, что хук verify_attributes / 2 может оставить точку выбора, и что последующее объединение находится в продолжении этой точки выбора.

Так что во время обратного отслеживания точка выбора пробуетсяснова.А это означает, что последующие объединения отменяются, а затем пробуются еще раз, если точка выбора обеспечивает дальнейшее решение.С умной организацией того, как вызывается обратный вызов, я думаю, что каждая система Prolog могла бы реализовать это, поскольку системы Prolog должны отстаивать точки выбора.Ни freeze / 2, ни когда / 2 не требуют этого, поскольку они работают с созданной переменной.И при этом типичный CLP (X) не требует этого, так как точки выбора нежелательны.Но он может существовать в XSB, поскольку третий аргумент отсутствует.Если вы запрещаете недетерминизм в хуке проверки, вам нужно предоставить альтернативы.

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

  • verify_attributes /3:
    Третий аргумент в варианте SICStus для verify_attributes / 2, который является 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в.Он имеет тот же эффект, что и третий аргумент в SICStus, но может быть вызван вручную при выполнении verify_attributes / 2.
...