Отладка рекурсии в Прологе - PullRequest
Новая
       27

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

0 голосов
/ 25 октября 2018

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

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)).Я понимаю, что это правильный ответ, но я не уверен, как Пролог искал его.

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

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

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

PS Это взято из следующей ссылки

1 Ответ

0 голосов
/ 25 октября 2018

Пролог ищет через бактрекинг.Есть два способа, которыми 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)).

...