Как Пролог может получать бессмысленные результаты, такие как 3 <2?

Question

В статье, которую я читаю, говорится следующее:

Плейстед [3] показал, что можно писать формально правильные программы PROLOG, используя семантику исчисления предикатов первого порядка, и при этом получать бессмысленные результаты, такие как 3 <2.

Это относится к тому факту, что Прологи тогда (1980-е годы) не использовали проверку происходящего .

К сожалению, статья, на которую он ссылается, находится за платным доступом. Я все же хотел бы увидеть такой пример. Интуитивно кажется, что отсутствие проверки происходит просто расширяет вселенную структур, включая круговые (но эта интуиция, по мнению автора, должна быть ошибочной).

---

Надеюсь, этот пример не

      smaller(3, 2) :- X = f(X).

Это было бы досадно.

Answer 1

Вот пример из статьи в современном синтаксисе:

      three_less_than_two :-
    less_than(s(X), X).

less_than(X, s(X)).

Действительно, мы получаем:

      ?- three_less_than_two.
true.

Потому что:

      ?- less_than(s(X), X).
X = s(s(X)).

В частности, это объясняет выбор 3 и 2 в запросе: Учитывая X = s(s(X)) значение s(X) является "трехцветным" (содержит три вхождения s если не раскрыть внутреннее), а X сам по себе "двоякий".

Включение проверки событий возвращает нас к логическому поведению:

      ?- set_prolog_flag(occurs_check, true).
true.

?- three_less_than_two.
false.

?- less_than(s(X), X).
false.

Так что это действительно похоже на

      arbitrary_statement :-
    arbitrary_unification_without_occurs_check.

Answer 2

Я считаю, что это соответствующая часть статьи, которую вы не можете увидеть сами (отсутствие платного доступа не ограничивало меня просматривать ее при использовании Google Scholar, вы должны попробовать получить к ней доступ таким образом):

Answer 3

Хорошо, как работает данный пример?

Если я это запишу:

      sm(s(s(s(z))),s(s(z))) :- sm(s(X),X).  % 3 < 2 :- s(X) < X
sm(X,s(X)).                            % forall X: X < s(X)

Запрос:

      ?- sm(s(s(s(z))),s(s(z)))

Это бесконечный цикл!

Поверни это другой стороной

      sm(X,s(X)).                            % forall X: X < s(X)
sm(s(s(s(z))),s(s(z))) :- sm(s(X),X).  % 3 < 2 :- s(X) < X

      ?- sm(s(s(s(z))),s(s(z))).
true ;
true ;
true ;
true ;
true ;
true 

Глубокая проблема в том, что Xдолжно быть число Пеано. Как только это будет циклично, человек больше не будет в арифметике Пеано. Надо добавить \+cyclic_term(X)срок там. (может позже, мой разум сейчас занят)