is_list/1 и свободные переменные

Question

Вот первое наблюдение:

?- is_list([]), is_list([_,_,_]).
true.

Вот еще одно наблюдение:

?- [] = _, [_,_,_] = _.
true.

Поэтому с чего бы is_list/1 быть реализован таким образом, чтобы

?- is_list(_).
false.

или же

?- is_list([_|_]).
false.

когда _ может быть четко объединен со списком? Разве это не было бы логически более разумным, чем это true?

В документации SWI-Пролога дляis_list/1В записке говорится:

В версиях до 5.0.1, is_list/1 только что проверил [] или же [_|_] а также proper_list/1 имел роль нынешнего is_list/1, Текущее определение соответствует стандарту де-факто.

Почему это стандарт де-факто?

Answer 1

Как вы правильно заметили, is_list/1 является неправильным или, скорее, неполным, потому что неправильно говорит, что нет никаких решений, когда задается самый общий запрос.

? - is_list (Ls).
ложный.

Список не существует? Давай!

Эта прискорбная черта характерна для всех наследственных предикатов проверки типа, таких как atom/1, integer/1 и т. д., чья некорректность была очевидна уже тогда, когда эти предикаты были задуманы, но протолкнуты после того, как они назвали тех, кто правильно выступал против предложенной им семантики, как "пуристов" (которым в то время не хватало комплиментарного характера, который слово приобрело с тех пор).

Случаи как:

? - is_list (Ls), Ls = [].
ложный.? - Ls = [], is_list (Ls).
Ls = [].

ясно продемонстрируйте, что с такими немонотонными тестами что-то принципиально нарушается с логической точки зрения. "Пролог (,)/2 не является логическим соединением ", да, если вы используете нелогичные предикаты на первом месте в вашем коде. В противном случае, (,)/2 всегда логическое сочетание целей.

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

library(error) и в частности must_be/2 идти в правильном направлении после того, как некорректность унаследованных нелогичных предикатов стала невыносимой даже для случайных пользователей пролога:

?- must_be(список, X).
Аргументы недостаточно проработаны?- must_be(список, [_|_]).
Аргументы недостаточно проработаны?- must_be(список, [a,b,c]).
правда.

must_be/2 прост в использовании и является хорошим первым шагом к более правильной логике программ. Другие конструкции также появляются на горизонте, и я надеюсь, что другие прокомментируют текущее состояние.

А теперь верная формулировка: оставляя в стороне фундаментальную проблему, изложенную выше, в документации SWI упоминается утверждение о том, достаточно ли проверки внешнего функтора, чтобы рассматривать термин как список, или же список должен фактически соответствовать индуктивному определению список, который:

• атом [] это список.
• если Ls это список, то '.'(_, Ls) это список.

Обратите внимание, что в последних версиях SWI, [] это даже не атом, поэтому он снова нарушает это понятие.