Почему циклические ссылки и рекурсия приводят к сбою моей программы?

#recursion #prolog #infinite-loop #circular-reference

#рекурсия #пролог #бесконечный цикл #циклическая ссылка

Вопрос:

Я написал эту простую программу Prolog.

 man(socrates).
mortal(X) :- man(X).
immortal(X) :- immortal(X).
  

Я задал ему обычные вопросы, такие как, является ли Сократ человеком или Сократ смертный.

 ?- man(socrates).
true.                    //we know for a fact that Socrates is a man
?- mortal(socrates).
true.                    //and it can logically be inferred that Socrates is mortal
?- immortal(socrates).
                         //but we can't seem to figure out if he's immortal
  

Произошел сбой из-за рекурсивного определения immortal . Циклические ссылки также приводят к сбою или ошибке с Out of stack space.

Мне кажется, что, по крайней мере, в этом случае, для мистера Пролога было бы довольно тривиально заключить, что из правил в программе нельзя сделать вывод, что Сократ бессмертен. Как? Я полагаю, что он мог бы изучить стек и посмотреть, проходит ли он по правилу, которое уже было пройдено.

Есть ли причина, по которой это еще не реализовано? Будет ли какая-то проблема с этим, которую я упускаю из виду, или существуют реализации Prolog, которые уже выполняют такой анализ?

Комментарии:

1. Вы хотите сказать, что определение бессмертного заключается в том, что он бессмертен?

2. Вы ищете «табулирование», хотя только несколько реализаций prolog поддерживают его (например, XSB или YAP).

Ответ №1:

Мне кажется, что, по крайней мере, в этом случае, для мистера Пролога было бы довольно тривиально заключить, что из правил в программе нельзя сделать вывод, что Сократ бессмертен.

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

Что касается логического значения вашего предиката immortal , это

 immortal(X) -> immortal(X)
  

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

Ответ №2:

Использование таблиц с XSB:

 :- table foo/1.

foo(X) :- foo(X).

bar(X) :- bar(X).
  

и затем:

 | ?- [tabled].
[tabled loaded]

yes
| ?- foo(1).

no
| ?- bar(1).    % does not finish
  

Ответ №3:

Ваши определения — и как вы их интерпретируете:

 man(socrates).
  

Сократ — мужчина.

 mortal(X) :- man(X).
  

Каждый человек смертен.

 immortal(X) :- immortal(X).
  

Каждый бессмертный бессмертен.


Ваши определения — и как Prolog их интерпретирует:

 man(socrates).
  

Если вы спрашиваете о мужественности Сократа, я знаю, что это правда.

 mortal(X) :- man(X).
  

Если вы спросите меня о смертности кого-либо, я проверю его мужественность (и если это правда, то и смертность тоже).

 immortal(X) :- immortal(X).
  

Если вы спросите меня о бессмертии кого-то, я проверю его бессмертие.
(Вам все еще интересно, как это приводит к бесконечному циклу?)


Если вы хотите заявить, что кто-то бессмертен, если нельзя доказать, что он смертен, то вы можете использовать:

 immortal(X) :- not( mortal(X) ).
  

Комментарии:

1. Я понимаю, почему это может быть бесконечный цикл, но я предположил, что логический язык a сможет сделать вывод, что immortal всегда будет false . Например, предположим, что в Stack Overflow есть значок «рекурсия», и единственный способ получить значок рекурсии — это получить значок рекурсии, его было бы невозможно получить.

2. Если вы хотите, чтобы значение immortal всегда было false , вы можете объявить это явно immortal(X) :- False. или с помощью immortal(X) :- !. (я могу ошибаться в этом, много лет я не использовал Prolog). Для этого простого случая они эквивалентны, но у вас могут быть другие, более сложные случаи, где рекурсия очень полезна (и может быть остановлена ! )

3. immortal(X) :- !. неверно, это скажет, что каждый X бессмертен.

4. @PeterOlson, поправка : Если вы хотите, чтобы значение immortal всегда было false , вы можете объявить это явно immortal(X) :- False. , что означает, что все они не бессмертны. ( и не с immortal(X) :- !. , что, как указал Джо Леманн, означает обратное, что каждый бессмертен .

5. @Peter Olson: Это совсем другое. Вызов undefined, основанный на ISO-Prolog, не завершается сбоем, но выдает ошибку.

Ответ №4:

Как насчет этой маленькой программы:

  loopy(Y) :- read(X), Z is X Y, print(Z), nl, loopy(Y).
  

Ваш Mr. Prolog сделал бы вывод, что loopy (Y) уже был вызван и завершится неудачей.