Как пролог выполняется через рекурсивные запросы с использованием succ?

Может ли кто-нибудь объяснить мне, почему этот запрос пролога работает так, как он работает. Определение таково: 



add(0,Y,Y). 

add(succ(X),Y,succ(Z)):- add(X,Y,Z).


Учитывая это: 



?-  add(succ(succ(succ(0))),  succ(succ(0)),  R).


Вот след запроса: 



Call:  (6)  add(succ(succ(succ(0))),  succ(succ(0)),  R) 



Call:  (7)  add(succ(succ(0)),  succ(succ(0)),  _G648) 



Call:  (8)  add(succ(0),  succ(succ(0)),  _G650) 



Call:  (9)  add(0,  succ(succ(0)),  _G652) 



Exit:  (9)  add(0,  succ(succ(0)),  succ(succ(0))) 



Exit:  (8)  add(succ(0),  succ(succ(0)),  succ(succ(succ(0)))) 



Exit:  (7)  add(succ(succ(0)),  succ(succ(0)), 

                                              succ(succ(succ(succ(0))))) 



Exit:  (6)  add(succ(succ(succ(0))),  succ(succ(0)), 

                                                succ(succ(succ(succ(succ(0))))))


Часть, которая смутила меня больше всего в этом учебнике, была тем фактом, что в первом аргументе succ разделен, и он рекурсирует. Хотя при рекурсии R получает succ... Но как?! Кроме того, откуда берется ноль на первом выходе (9)? Я новичок в прологе, и я пытаюсь понять язык для домашнего задания. Любая помощь очень ценится.



Примечание: для всех, кто заинтересован, ссылка на этот учебник http://www.learnprolognow.org/lpnpage.php?pagetype=html&pageid=lpn-htmlse9

346   3  

3 ответов:

"откуда берется ноль на первом выходе (9)?"

Вызов

Объединен с первым предложением, которое говорит, что если первый аргумент add равен нулю, то второй и третий являются одинаковыми. В этой конкретной ситуации переменная _G652 становится succ(succ(0)).

"хотя при рекурсии R получает succ... Но как?!"

Это является результатом применения второго пункта. В этом пункте говорится (грубо), что вы сначала отделите succ от первого аргумента, затем вызовите add рекурсивно и, наконец, добавьте еще один "слой" succ к третьему аргументу, возвращающемуся из этого рекурсивного вызова.

Предикат add есть не что иное, как прямая реализация сложения в арифметике Пеано: http://en.wikipedia.org/wiki/Peano_axioms#Addition

1  
2012-04-25 09:14:16

Вы видите, call и exit - это verbs действия, которые интерпретатор предпринимает, пытаясь решить поставленный Вами запрос. Затем след показывает детали фактически выполненной работы и позволяет вам просмотреть ее в исторической перспективе.

Когда Пролог должен выбрать правило (a call), он использует name, которое вы ему даете (так называемый functor), и пытается к unify каждому аргументу в голове правила. Тогда мы обычно говорим, что пролог рассматривает также arity, то есть число аргументов, для выбора.

Unification попытки "сделать равными" два члена, и заслуживающие внимания результаты так называемые bindings переменных. Вы уже знаете, что переменные-это имена, начинающиеся с Uppercase. Такие имена идентифицируют неопределенные значения в правилах, т. е. являются placeholders для Аргументов. Чтобы избежать путаницы, когда Пролог показывает трассировку, переменные переименовываются, чтобы мы могли их идентифицировать, потому что соответствующая деталь-это identities или привязки, установленные во время доказательства.

Тогда вы видите такие _G648 символы в следах. Они остаются дляеще не установленных аргументов названной цели, а именно R и Z. R уникален (встречается только в вызове верхнего уровня), поэтому этот пролог любезно сохраняет удобное для пользователя имя, но Z приходит из программы, потенциально встречается несколько раз, а затем переименовывается.

Чтобы ответить на этот запрос 

?-  add(succ(succ(succ(0))),  succ(succ(0)),  R).

Пролог Первые попытки соответствия 

add(0,Y,Y).

И потерпеть неудачу, потому что succ(succ(succ(0)) нельзя сделать равным 0. Затем попытки 

add(succ(X),Y,succ(Z)) :- add(X,Y,Z).

Таким образом должны быть решены следующие привязки (слева термины вызывающего): 

succ(succ(succ(0))) = succ(X)
succ(succ(0)) = Y
R = Z
Вы можете видеть, почему X становится succ(succ(0)), и у нас есть новая цель доказать, то есть тело правила add(X,Y,Z) С только что установленными связями:

Add (succ(succ(0)), succ(succ (0)), _G648)

И так далее... пока X не станет 0 и цель не совпадет

add(0,Y,Y).

Тогда Y становится succ(succ (0)), и следует также дать значение Z в вызове правило.

HTH

4  
2012-04-25 09:37:18

(Надеюсь) более разборчивый след с большим количеством аннотаций: 

 (6) Call:  add(succ(succ(succ(0))),  succ(succ(0)),  R)          % R     = succ(_G648)
      (7) Call:  add(succ(succ(0)),  succ(succ(0)),  _G648)       % _G648 = succ(_G650) 
           (8) Call:  add(succ(0),  succ(succ(0)),  _G650)        % _G650 = succ(_G652) 
                (9) Call:  add(0,  succ(succ(0)),  _G652)         % _G652 = succ(succ(0))
                (9) Exit:  add(0,  succ(succ(0)),  succ(succ(0)))       
           (8) Exit:  add(succ(0),  succ(succ(0)),  succ(succ(succ(0)))) 
      (7) Exit:  add(succ(succ(0)),  succ(succ(0)), succ(succ(succ(succ(0))))) 
 (6) Exit:  add(succ(succ(succ(0))),  succ(succ(0)), succ(succ(succ(succ(succ(0))))))
Как видите, четыре выхода избыточны, окончательный ответ уже известен в точке (9) Exit; в этой точке достаточно только одного выхода: 
     %     R = succ(_G648)
     %              _G648 = succ(_G650) 
     %                           _G650 = succ(_G652) 
     %                                        _G652 = succ(succ(0))
     % thus,
     %     R = succ(        succ(        succ(        succ(succ(0)) )))

Это действительно то, что происходит при оптимизации хвостового вызова, поскольку определение предиката является действительно хвостовым рекурсивным, а результат под R строится сверху вниз, причем" дыра " постепенно заполняется инстанциацией логических переменных. Таким образом, succ( _ ) не добавляется после рекурсивного вызова, но устанавливается перед им. В этом также заключается суть оптимизации хвостовой рекурсии по модулю cons.

0  
2018-05-31 16:19:48

Comments

    Ничего не найдено.
Click here to cancel reply.