Отладка рекурсии в Прологе

Вот моя база знаний:

numeral(0). 
numeral(succ(X))  :-  numeral(X).

Вот мой запрос:

numeral(X).

Вот что SWI Prolog возвращает в режиме трассировки:

[trace]  ?- numeral(X).
   Call: (8) numeral(_3806) ? creep
   Exit: (8) numeral(0) ? creep
X = 0 ;
   Redo: (8) numeral(_3806) ? creep
   Call: (9) numeral(_4006) ? creep
   Exit: (9) numeral(0) ? creep
   Exit: (8) numeral(succ(0)) ? creep
X = succ(0) ;
   Redo: (9) numeral(_4006) ? creep
   Call: (10) numeral(_4010) ? creep
   Exit: (10) numeral(0) ? creep
   Exit: (9) numeral(succ(0)) ? creep
   Exit: (8) numeral(succ(succ(0))) ? creep
X = succ(succ(0))

Я понимаю, как он находит ответ X=0, я не совсем понимаю, как он получает: X = succ(succ(0)). Я понимаю, что это правильный ответ, но не знаю, как его искали в Prologs.

Вот мои мысли: Когда он печатает Call: (9) numeral(_4006) ? creep, он пробует следующее правило: numeral(succ(X)) :- numeral(X). И, в частности, он, вероятно, заменяет _4006 = succ(X) затем он проверяет, выполняется ли он только тогда, когда сохраняется numeral(X), который Prolog сверяет с numeral(0), поэтому результат - _4006 = succ(0).

Теперь, если мы попросим другое решение, он снова вернется к numeral(_4006), но что он догадывается, когда он вызывает numeral(_4010). Что здесь за ветвящийся процесс?

Есть ли способ получить более подробную информацию?

P.S. Это взято из следующего ссылка

Библиотека для работы с мороженым
Библиотека для работы с мороженым
Лично я попрощался с операторами print() в python. Без шуток.
0
0
84
1
Перейти к ответу Данный вопрос помечен как решенный

Ответы 1

Ответ принят как подходящий

Prolog выполняет поиск через бактрекинг. Есть два способа, которыми Prolog может стремиться удовлетворить вызов numeral(X):

  1. с numeral(0), и в этом случае он объединяет X с 0; а также
  2. с numeral(succ(Y)) :- numeral(Y), и в этом случае он объединяет X с succ(Y) и выполняет рекурсивный вызов.

Я здесь использовал Y, поскольку это также создает путаницу: переменные в предложении - это с локальным охватом в том смысле, что X в предложении не является той же переменной, что и X в вызове.

Теперь, если Prolog откатывает назад и стремится удовлетворить предикат с предложением, это означает, что X = succ(Y) с Y переменной, но ему необходимо сделать дополнительный вызов с numeral(Y), как указано в теле.

Опять же, есть два варианта:

  1. с numeral(0), и в этом случае он объединяет Y с 0; а также
  2. с numeral(succ(Z)) :- numeral(Z), и в этом случае он объединяет Y с succ(Z) и выполняет рекурсивный вызов.

В случае, если мы выберем первый, Y установлен на 0, и, следовательно, X = succ(Y), следовательно, X = succ(0). В последнем случае и X = succ(Y), и Y = succ(Z), и мы снова делаем рекурсивный вызов.

Теперь, если мы снова используем первую строку для numeral(0), это означает, что Z унифицирован с 0, следовательно, Z = 0, следовательно, Y = succ(0), следовательно, X = succ(succ(0)).

Другие вопросы по теме