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

Question

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

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.

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

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

Answer 1

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

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

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

immortal(X) -> immortal(X)

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

Answer 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

Answer 3

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

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) ).

Answer 4

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

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

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