#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) уже был вызван и завершится неудачей.