Создание "детерминированного успеха" целей Prolog

Ответ 1

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

См. пример:

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

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

EDIT. Позвольте мне проиллюстрировать удивительность этой конструкции, а точнее, очень близкого предиката 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 для этого? Потому что это позволяет мне удобно описать (подмножество) все булевы выражения определенной глубины и, таким образом, достаточно рассчитать их все. Например:

?- length(Ls, _), phrase(sat(Sat), Ls).
Ls = [] ;
Ls = [],
Sat = a ;
Ls = [],
Sat = ~_G475 ;
Ls = [_G475],
Sat = _G478+_G479 .

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

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

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

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

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

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

Множество решений labeling_nondet/1 является собственным подмножеством множества labeling/1.

Опишем, что выглядит counterexample указанного свойства:

counterexample(Sat) :-
        length(Ls, _),
        phrase(sat(Sat), Ls),
        term_variables(Sat, Vs),
        sat(Sat),
        setof(Vs, labeling_nondet(Vs), Sols),
        setof(Vs, labeling(Vs), Sols).

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

| ?- counterexample(Sat).
Sat = a+ ~_A,
sat(_A=:=_B*a) ? ;

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

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

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

?- sat(a + ~X), labeling([X]).
X = 0 ;
false.

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

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

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

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

?- dif(Det, true), call_cleanup(true, Det=true).
dif(Det, true).

?- call_cleanup(true, Det=true), dif(Det, true).
false.

в то время как оба запроса терпят неудачу в SICStus Prolog (4.3.2).

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

В проекте ISO мы видим:

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

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

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

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

Успех или сбой очистки - игнорируется

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

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

Ответ 2

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

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

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

setup_call_cleanup(true, true, Det=true)

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

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

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