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

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

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.

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

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


infinite-loop recursion circular-reference prolog
person Peter Olson    schedule 13.11.2011    source источник
comment
Вы хотите сказать, что определение бессмертного состоит в том, что он бессмертен?   -  person Lasse V. Karlsen    schedule 13.11.2011
comment
Вы ищете таблицу, хотя только несколько реализаций пролога поддерживают ее (например, XSB или YAP).   -  person salva    schedule 13.11.2011

Ответы (4)


arrow_upward
6
arrow_downward

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

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

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

immortal(X) -> immortal(X)

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

person Fred Foo    schedule 13.11.2011

arrow_upward
3
arrow_downward

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

:- table foo/1.

foo(X) :- foo(X).

bar(X) :- bar(X).

а потом:

| ?- [tabled].
[tabled loaded]

yes
| ?- foo(1).

no
| ?- bar(1).    % does not finish
person salva    schedule 13.11.2011

arrow_upward
2
arrow_downward

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

man(socrates).

Сократ — человек.

mortal(X) :- man(X).

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

immortal(X) :- immortal(X).

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

Ваши определения - и как их интерпретирует Пролог:

man(socrates).

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

mortal(X) :- man(X).

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

immortal(X) :- immortal(X).

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

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

immortal(X) :- not( mortal(X) ).
person ypercubeᵀᴹ    schedule 13.11.2011
comment
Я понимаю, почему это может быть бесконечный цикл, но я предполагал, что логический язык сможет сделать вывод, что immortal всегда будет ложным. Например, предположим, что на Stack Overflow есть значок рекурсии, и единственный способ получить значок рекурсии — это получить значок рекурсии, получить его было бы невозможно. - person Peter Olson; 13.11.2011
comment
Если вы хотите, чтобы бессмертие всегда было ложным, вы можете объявить это явно immortal(X) :- False. или с immortal(X) :- !. (я могу ошибаться в этом, много лет я не использовал Пролог). Для этого простого случая они эквивалентны, но у вас могут быть и другие, более сложные случаи, где рекурсия очень полезна (и может быть остановлена ​​с помощью !) - person ypercubeᵀᴹ; 13.11.2011
comment
immortal(X) :- !. неверно, будет сказано, что каждый X бессмертен. - person Joe Lehmann; 13.11.2011
comment
@PeterOlson, Исправление: если вы хотите, чтобы бессмертие всегда было ложным, вы можете явно объявить это immortal(X) :- False., что означает, что все не бессмертны. (а не с immortal(X) :- !. что, как указал Джо Леманн, означает обратное, что каждый бессмертен. - person ypercubeᵀᴹ; 13.11.2011
comment
@ypercube Было бы проще полностью исключить определение immortal, и это означало бы, по сути, то же самое. - person Peter Olson; 13.11.2011
comment
@Peter Olson: Это совсем другое. Вызов неопределенного на основе ISO-Prolog не завершается ошибкой, а вызывает ошибку. - person salva; 13.11.2011

arrow_upward
0
arrow_downward

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

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

Ваш г-н Пролог сделал бы вывод, что цикл loopy(Y) уже был вызван и потерпит неудачу.

person Joe Lehmann    schedule 13.11.2011