Делая "детерминированный успех" целей Пролога явным
Вопрос о детерминированном успехе некоторой цели Пролога снова и снова поднимался, по крайней мере, в следующих вопросах:
- Уточнение термина равенство / неравенство
- Пересечение и объединение 2 списков
- Удалить дубликаты в списке (Пролог)
- Пролог: Как я могу реализовать сумму квадратов двух самых больших чисел из трех?
- Списки заказов с программированием логики ограничений)
Использовались разные методы (например, провоцирование определенных ошибок в ресурсах или тщательное изучение точных ответов, данных на уровне Пролога), но все они кажутся мне рекламными.
Я ищу общий, переносимый и совместимый со стандартом 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.
Так что это и правильная реализация, чтобы обнаружить детерминизм и не обнаружить детерминизм.