Стойкость: определение и его связь с логической чистотой и окончанием

Question

До сих пор я всегда принимал постоянство в программах Prolog:

Если для запроса Q есть подзадача S такой, что есть термин T что делает ?- S=T, Q. преуспеть хотя ?- Q, S=T. терпит неудачу, то один из предикатов, вызываемых Q не стойкий

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

В частности, по крайней мере для меня логическая чистота всегда подразумевала стойкость.

---

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

integer_integer_maximum (X, Y, Y): -
        Y> = X,!.
integer_integer_maximum (X, _, X).

Очевидная ошибка в этом - скажем, " колебание " - определение состоит в том, что следующий запрос некорректно выполняется:

? - M = 0, integer_integer_maximum (0, 1, M).
М = 0. % неправильно!

тогда как обмен целями дает правильный ответ:

? - integer_integer_maximum (0, 1, M), M = 0.
ложный.

Хорошее решение этой проблемы - полагаться на чистые методы описания отношения, используя, например:

integer_integer_maximum (X, Y, M): -
        M # = max (X, Y).

Это работает правильно в обоих случаях и может даже использоваться в других ситуациях:

? - integer_integer_maximum (0, 1, M), M = 0.
ложный.
? - M = 0, integer_integer_maximum (0, 1, M).
ложный.

|? - X в 0..2, Y в 3..4, integer_integer_maximum(X, Y, M).
Х в 0..2,
Y в 3..4,
М в 3..4?;
нет

---

В настоящее время в статье " Рекомендации по кодированию для Пролога " Ковингтона и др., Написанной в соавторстве с самим изобретателем понятия Ричардом О'Кифом, содержится следующий раздел:

5.1 Предикаты должны быть стойкими.

Любой достойный предикат должен быть "устойчивым", т. Е. Должен работать правильно, если его выходная переменная уже создана для выходного значения (O'Keefe 1990).

То есть,

?- foo(X), X = x.

а также

?- foo(x).

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

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

Например, рассмотрим чистую программу Prolog:

nat (s (X)): - nat (X).
физ (0).

Сейчас мы находимся в следующей ситуации:

? - nat (0).
правда.
? - nat (X), X = 0.
nontermination

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

Отсюда мой вопрос: должны ли мы называть вышеупомянутую программу непостоянной? Пожалуйста, обоснуйте свой ответ объяснением намерения за стойкость и его определением в доступной литературе, его отношением к логической чистоте, а также соответствующими терминами терминации.

Answer 1

В "Ремесле пролога" на странице 96 Ричард О'Киф говорит, что "мы называем свойство отказа давать неправильные ответы, даже когда запрос имеет неожиданную форму (обычно предоставляя значения для того, что мы обычно считаем входными данными *), стойкость"

* Я не уверен, должны ли это быть результаты. т.е. в вашем запросе ?- M = 0, integer_integer_maximum(0, 1, M). M = 0. % wrong! M используется в качестве входных данных, но предложение было разработано для его вывода.

В nat(X), X = 0. мы используем X в качестве выходной переменной, а не входной переменной, но она не дала неправильного ответа, так как не дает никакого ответа. Так что я думаю, что под этим определением это может быть непоколебимо.

Эмпирическое правило, которое он дает, - это "отложить объединение вывода до окончания разреза". Здесь мы не получили сокращение, но мы все еще хотим отложить объединение.

Однако я бы подумал, что было бы разумно иметь сначала базовый случай, а не рекурсивный, чтобы nat(X), X = 0. изначально удастся.. но у вас все равно будут другие проблемы..