Устойчивость: определение и его связь с логической чистотой и прекращением
До сих пор я всегда придерживался устойчивости в программах Prolog:
Если для запроса Q существует подтерм S, так что существует термин T, который делает ?- S=T, Q. успешным, хотя ?- Q, S=T. не работает, тогда один из предикатов, вызываемый Q, будет не стойким.
Интуитивно я утверждал, что мы не можем использовать экземпляры, чтобы "обмануть" предикат, чтобы дать решения, которые иначе не только не даны, но отклонено. Обратите внимание на разницу для неисчерпающих программ!
В частности, по крайней мере, для меня logical-purity всегда подразумевала стойкость.
Пример. Чтобы лучше понять понятие стойкости, рассмотрите почти классический контрпример этого свойства, который часто цитируется при введении продвинутых студентов к операционным аспектам Prolog, используя определение неправильное отношения между двумя целыми числами и их максимальным
integer_integer_maximum(X, Y, Y) :-
Y >= X,
!.
integer_integer_maximum(X, _, X).
Вопиющая ошибка в этом вопросе: скажем, определение "колебания" означает, что следующий запрос неправильно преуспевает:
?- M = 0, integer_integer_maximum(0, 1, M).
M = 0. % wrong!
тогда как обмен целями дает правильный ответ:
?- integer_integer_maximum(0, 1, M), M = 0.
false.
Хорошим решением этой проблемы является полагаться на чистые методы для описания отношения, используя, например:
integer_integer_maximum(X, Y, M) :-
M #= max(X, Y).
Это корректно работает в обоих случаях и может использоваться даже в следующих ситуациях:
?- integer_integer_maximum(0, 1, M), M = 0.
false.
?- M = 0, integer_integer_maximum(0, 1, M).
false.
| ?- X in 0..2, Y in 3..4, integer_integer_maximum(X, Y, M).
X in 0..2,
Y in 3..4,
M in 3..4 ? ;
no
Теперь документ Руководства по кодированию для Prolog Ковингтона и др., в соавторстве с самим изобретателем понятия Ричард О "Keefe" содержит следующий раздел:
5.1 Предикаты должны быть стойкими.
Любой достойный предикат должен быть "стойким", то есть должен работать правильно, если его выходная переменная уже используется для создания выходного значения (OKeefe 1990).
То есть
?- foo(X), X = x.
и
?- foo(x).
должен преуспеть при одинаковых условиях и иметь одинаковые побочные эффекты. Несоблюдение этого допускается только для вспомогательных предикатов, чьи шаблоны вызовов сильно ограниченные основными предикатами.
Таким образом, определение, приведенное в цитированной статье, значительно более строгое, чем указано выше.
Например, рассмотрите программу pure Prolog:
nat(s(X)) :- nat(X).
nat(0).
Теперь мы находимся в следующей ситуации:
?- nat(0).
true.
?- nat(X), X = 0.
nontermination
Это явно нарушает свойство следующего в точно таких же условиях, потому что один из запросов больше не выполняется вообще.
Отсюда мой вопрос: нельзя ли назвать вышеупомянутую программу непоколебимой? Пожалуйста, оправдайте ваш ответ с объяснением намерения за стойкостью и его определение в доступной литературе, его отношение к logical-purity, а также соответствующие понятия терминации.
Ответы
Ответ 1
В "The craft of prolog" стр. 96 Ричард О'Киф говорит: "Мы называем свойство отказываться давать неправильные ответы, даже если запрос имеет неожиданную форму (обычно поставляя значения для того, что мы обычно считаем в качестве входов *) стойкость"
* Я не уверен, что это должны быть выходы. т.е. в вашем запросе ?- M = 0, integer_integer_maximum(0, 1, M). M = 0. % wrong! M используется как вход, но предложение было разработано для него как выход.
В nat(X), X = 0. мы используем X как выходную переменную, а не входную переменную, но она не дала неправильного ответа, так как она не дает ответа. Поэтому я считаю, что под этим определением он может быть стойким.
Правило большого пальца, которое он дает, это "отложить выходную унификацию до окончания разреза". Здесь у нас нет сокращения, но мы все же хотим отложить объединение.
Однако я бы подумал, что было бы разумно иметь базовый случай сначала, а не рекурсивный случай, так что nat(X), X = 0. изначально преуспел бы... но у вас все еще были бы другие проблемы.
