Вот моя база знаний:
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. Это взято из следующего ссылка
Prolog выполняет поиск через бактрекинг. Есть два способа, которыми Prolog может стремиться удовлетворить вызов numeral(X)
:
numeral(0)
, и в этом случае он объединяет X
с 0
; а такжеnumeral(succ(Y)) :- numeral(Y)
, и в этом случае он объединяет X
с succ(Y)
и выполняет рекурсивный вызов.Я здесь использовал Y
, поскольку это также создает путаницу: переменные в предложении - это с локальным охватом в том смысле, что X
в предложении не является той же переменной, что и X
в вызове.
Теперь, если Prolog откатывает назад и стремится удовлетворить предикат с предложением, это означает, что X = succ(Y)
с Y
переменной, но ему необходимо сделать дополнительный вызов с numeral(Y)
, как указано в теле.
Опять же, есть два варианта:
numeral(0)
, и в этом случае он объединяет Y
с 0
; а также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))
.