Делая "детерминированный успех" целей Пролога явным

Вопрос о детерминированном успехе некоторой цели Пролога снова и снова поднимался, по крайней мере, в следующих вопросах:

Использовались разные методы (например, провоцирование определенных ошибок в ресурсах или тщательное изучение точных ответов, данных на уровне Пролога), но все они кажутся мне рекламными.

Я ищу общий, переносимый и совместимый со стандартом ISO способ выяснить, не выполнило ли выполнение какой-либо цели Пролога (которая была успешной) некоторую точку выбора. Может быть, какой-то мета-предикат?

Не могли бы вы намекнуть мне в правильном направлении? Заранее спасибо!

2 ответа

Решение

Хорошие новости всем: setup_call_cleanup/3 (в настоящее время проект предложения для ISO) позволяет сделать это довольно портативным и красивым способом.

Смотрите пример:

setup_call_cleanup(true, (X=1;X=2), Det=yes)

успешно с Det == yes когда больше нет точек выбора.


РЕДАКТИРОВАТЬ: Позвольте мне проиллюстрировать удивительность этой конструкции, или, скорее, очень тесно связанных предикатов call_cleanup/2, с простым примером:

В превосходной документации CLP(B) SICStus Prolog мы находим в описании labeling/1 очень сильная гарантия:

Перечисляет все решения в обратном порядке, но создает точки выбора только при необходимости.

Это действительно сильная гарантия, и поначалу трудно поверить, что это всегда так. К счастью для нас, в Prolog чрезвычайно легко составлять и генерировать систематические тестовые примеры для проверки таких свойств, по сути, используя систему Prolog для самопроверки.

Мы начнем с систематического описания того, как выглядит логическое выражение в CLP(B):

:- use_module(library(clpb)).
:- use_module(library(lists)).

sat(_) --> [].
sat(a) --> [].
sat(~_) --> [].
sat(X+Y) --> [_], sat(X), sat(Y).
sat(X#Y) --> [_], sat(X), sat(Y).

На самом деле есть еще много случаев, но давайте пока ограничимся вышеупомянутым подмножеством выражений CLP(B).

Почему я использую DCG для этого? Потому что это позволяет мне удобно описывать (подмножество) все логические выражения определенной глубины и, таким образом, справедливо перечислять их все. Например:

? - длина (Ls, _), фраза (sat(сб), Ls).
Ls = [];
Ls = [],
Сб = а;
Ls = [],
Сб = ~ _G475;
Ls = [_G475],
Сб = _G478 + _G479.

Таким образом, я использую DCG только для обозначения того, сколько доступных "токенов" уже было использовано при генерации выражений, ограничивая общую глубину результирующих выражений.

Далее нам нужен небольшой вспомогательный предикат labeling_nondet/1, который действует именно так, как labeling/1, но верно только в том случае, если точка выбора все еще остается. Это где call_cleanup/2 приходит в:

labeling_nondet(Vs) :-
        dif(Det, true),
        call_cleanup(labeling(Vs), Det=true).

Наш тестовый пример (и под этим мы фактически имеем в виду бесконечную последовательность небольших тестовых случаев, которые мы можем очень удобно описать с помощью Пролога) теперь нацелен на проверку вышеуказанного свойства, а именно:

Если есть точка выбора, то есть дальнейшее решение.

Другими словами:

Множество решений labeling_nondet/1 является правильным подмножеством этого из labeling/1,

Итак, опишем, как выглядит контрпример вышеупомянутого свойства:

контрпример (сб):-
        длина (Ls, _),
        фраза (сб (сб), Ls),
        term_variables(сб, вс),
        СБ (СБ),
        setof(Vs, labeling_nondet(Vs), Sols),
        setof(Vs, маркировка (Vs), Sols).

И теперь мы используем эту исполняемую спецификацию, чтобы найти такой контрпример. Если решатель работает так, как задокументировано, то мы никогда не найдем контрпример. Но в этом случае мы сразу получаем:

|? - контрпример (сб).
Сб = а + ~_А,
сел (_A=:=_B*a)?;

Так что на самом деле собственность не держит. Разобраться в сути, хотя в следующем запросе больше не осталось решений, Det не объединяется с true:

| ?- sat(a + ~X), call_cleanup(labeling([X]), Det=true).
X = 0 ? ;
no

В SWI-Prolog избыточная точка выбора очевидна:

? - сат (a + ~X), маркировка ([X]).
Х = 0;
ложь

Я не привожу этот пример, чтобы критиковать поведение SICStus Prolog или SWI: никого на самом деле не волнует, оставлена ​​ли лишняя точка выбора в labeling/1 менее всего в искусственном примере, который включает универсально количественные переменные (что нетипично для задач, в которых используются labeling/1).

Я приведу этот пример, чтобы показать, как красиво и удобно гарантии, которые задокументированы и предназначены, могут быть проверены с такими мощными проверочными предикатами...

... при условии, что разработчики заинтересованы в стандартизации своих усилий, чтобы эти предикаты фактически работали одинаково в разных реализациях! Внимательный читатель заметит, что поиск контрпримеров дает совершенно разные результаты при использовании в SWI-Prolog.

В неожиданном повороте событий вышеупомянутый контрольный пример обнаружил расхождение в call_cleanup/2 реализации SWI-Prolog и SICStus. В SWI-Прологе (7.3.11):

? - dif (Det, true), call_cleanup (true, Det = true).
диф (дет, правда).? - call_cleanup (true, Det = true), dif (Det, true).
ложь

в то время как оба запроса не выполняются в SICStus Prolog (4.3.2).

Это довольно типичный случай: если вы заинтересованы в тестировании определенного свойства, вы обнаружите много препятствий на пути тестирования реального свойства.

В проекте предложения ИСО мы видим:

Отказ [цели очистки] игнорируется.

В документации SICStus call_cleanup/2 мы видим:

Очистка завершается успешно после выполнения некоторого побочного эффекта; в противном случае возможно непредвиденное поведение.

И в варианте SWI мы видим:

Успех или неудача Очистки игнорируется

Таким образом, для переносимости, мы должны написать labeling_nondet/1 как:

labeling_nondet(Vs) :-
        call_cleanup(labeling(Vs), Det=true),
        dif(Det, true).

В setup_call_cleanup/3 нет гарантии, что он обнаружит детерминизм, то есть пропущенные точки выбора в достижении цели. В черновом предложении 7.8.11.1 описывается только:

в) Обработчик очистки вызывается ровно один раз; не позже чем
при неудаче Г. Ранние моменты:
Если G истинно или ложно, C вызывается при реализации
зависимый момент после последнего решения и после последнего
Наблюдаемый эффект Г.

Таким образом, в настоящее время нет требования, чтобы:

setup_call_cleanup(true, true, Det=true)

Возвращает Det=true в первую очередь. Это также отражено в контрольных примерах 7.8.11.4. В примерах, приведенных в предложении проекта, мы находим один контрольный пример, в котором говорится:

setup_call_cleanup(true, true, X = 2).
Either: Succeeds, unifying X = 2.
Or: Succeeds.

Так что это и правильная реализация, чтобы обнаружить детерминизм и не обнаружить детерминизм.

Другие вопросы по тегам