Вычислительная модель логических программ Рекурсивно-логическое программирование Григорьева И.В.

Унификация Основу вычислительной модели логических программ составляет алгоритм унификации. Унификация является основой автоматической дедукции и логического вывода в задачах искусственного интеллекта. Вспомним, что терм t есть общий пример двух термов t1 и t2, если существуют такие подстановки 1 и 2, что t равно t1 1 и t2 2. Терм s называется более общим, чем терм t, если t-пример s, но s не является примером t.

Терм s называется алфавитным вариантом терма t, если t-пример s и s-пример t. Алфавитные варианты совпадают с точностью до переименования переменных, входящих в термы. Например, термы member(X,tree(Left,X,Right)) и member(Y,tree (left,Y,Z)) являются алфавитными вариантами.

Унификатором двух термов называется подстановка, которая делает термы одинаковыми. Если существует унификатор двух термов, то термы называются унифицируемыми. Существует тесная взаимосвязь между унификаторами и общими примерами. Любой унификатор определяет общий пример и обратно, любой общий пример определяет унификатор.

Например, конк([1,2,3],[3,4],List) и конк([X/Xs],Ys,[X/Zs]) унифицируемы. Унифицирующая подстановка {X = 1, Xs = [2,3],Ys = [3,4], List = [1,Zs]}. Общий пример, задаваемый этой подстановкой - это конк ([1,2,3],[3,4],[1 /Z]).

Наибольшим общим унификатором, или н. о. у, двух термов называется унификатор, соответствующий наиболее общему примеру. Если два терма унифицируемы, то существует единственный наибольший общий унификатор. Единственность определена с точностью до переименования переменных. Это эквивалентно тому, что два терма имеют единственный, с точностью до изоморфизма, наибольший общий пример.

Алгоритм унификации находит наибольший общий унификатор двух термов, если такой существует. Если термы не унифицируемы, алгоритм сообщает об отказе. Описываемый алгоритм унификации основан на решении системы равенств. Входом алгоритма являются два терма – Т1 и Т2. Результатом работы алгоритма является н. о. у. двух термов, если термы унифицируемы, или отказ, если термы не унифицируемы.

Алгоритм использует стек для хранения равенств, подлежащих решению, и ячейку памяти для построения выходной подстановки. В начале работы ячейка пуста, в стек помещается равенство Т1 = Т2. Алгоритм состоит из цикла, в теле которого из стека считывается и обрабатывается одно равенство. Цикл завершается, если в процессе работы появляется сообщение об отказе или стек оказывается пустым.

Рассмотрим возможные действия при считывании равенства S = Т. Простейший случай, когда S и Т - одинаковые константы или переменные. Тогда равенство корректно, и ничего делать не надо. Вычисление продолжается, из стека считывается следующее равенство. Простейший случай, когда S и Т - одинаковые константы или переменные. Тогда равенство корректно, и ничего делать не надо. Вычисление продолжается, из стека считывается следующее равенство.

Если S - переменная, а Т-терм, не содержащий вхождений S, то происходит следующее. В стеке отыскиваются все вхождения переменной S и каждое из них заменяется на Т. Аналогично все вхождения S в заменяются на Т. Затем подстановка S = Т добавляется к. Существенно, что S не входит в Т. Проверка, соответствующая словам «не содержит вхождений», известна как проверка на вхождение. Если S - переменная, а Т-терм, не содержащий вхождений S, то происходит следующее. В стеке отыскиваются все вхождения переменной S и каждое из них заменяется на Т. Аналогично все вхождения S в заменяются на Т. Затем подстановка S = Т добавляется к. Существенно, что S не входит в Т. Проверка, соответствующая словам «не содержит вхождений», известна как проверка на вхождение.

Если T-переменная, S-терм, не содержащий Т, т. е. Т удовлетворяет проверке на вхождение относительно S, то выполняется аналогичная последовательность действий. Если T-переменная, S-терм, не содержащий Т, т. е. Т удовлетворяет проверке на вхождение относительно S, то выполняется аналогичная последовательность действий.

Равенства добавляются в стек, если S и T- составные термы с одним и тем же главным функтором одной и той же арности, например: f(S1,...,Sn) к f(T1,...,Tn). Для унификации термов следует совместно унифицировать каждую пару аргументов, что достигается помещением в стек n равенств вида Si = Ti. Во всех остальных случаях выдается сообщение об отказе, и работа алгоритма завершается. Если стек пуст, то термы унифицируемы и.унификатор содержится в 0.

Вход:Два терма Т1 и T2, которые надо унифицировать. Результат: Подстановка - н. о. у. термов Т1, и Т2 или отказ. Алгоритм: Начальное значение подстановки пусто, стек содержит равенство Т1 = Т2, failure := false, пока стек не пуст и не failure, выполнить, считать X = Y из стека ветвление Х-переменная, не входящая в Y: заменить все вхождения X в стеке и в на Y добавить X = Y к. Y-переменная, не входящая в X: заменить все вхождения У в стеке и в на X добавить Y= X к. добавить Y= X к. X и Y-одинаковые константы или переменные: продолжать X есть f(Х1,..., Хn) и Y есть f(Y1,..., Yn) для некоторого функтора f и n > 1: поместить X =Y, для всех i = 1,...,n в стек в остальных случаях: failure := true если failure, то результат-отказ; иначе результат.

Рассмотрим попытку унификации термов конк([a,b],[c,d],Ls) и конк([X| Xs],Ys,[X|Zs]). Начальное состояние стека: конк([a,b],[c,d],Ls) = конк([X| Xs],Ys,[X|Zs]) Эти два терма имеют один и тот же функтор - конк одной арности 3, поэтому в стек добавляются три равенства, соответствующие подтермам двух термов: [a,b]= [X| Xs], [c,d]=Ys, Ls=[ X|Zs].

Проверка на вхождение необходима, чтобы предотвратить попытку унифицировать такие термы, как s(X) и X. Эти термы не имеют конечного общего примера.

Абстрактный интерпретатор логических программ Неформально процесс вычисления логической программы может быть описан следующим образом. Он начинается с некоторого исходного (возможно, конъюнктивного) вопроса G и завершается одним из двух результатов: успешное завершение или отказ. В случае успешного завершения результатом должен быть доказанный пример G.

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

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

Для более формального описания вычислений введем несколько полезных понятий. Вычислением цели Q = Q0 программой Р называется, возможно бесконечная, последовательность троек (Qi,Gi,Ci); здесь Qi - конъюнктивная цель, Gi-цель, входящая в Qi, Сi - предложение A:- В1,...,Bk в Р c таким переименованием, что новые символы переменных не встречаются в Qj, 0

Для всех i > 0 цель Qi+1, является или результатом замены Gi на тело Сi в Qi, и применения подстановки Qi наибольшего общего унификатора термов Gi и Аi, (Ai -заголовок Сi), или константой true, если Gi-единственная цель в Qi и тело Сi пусто, или константой отказ, если Gi и заголовок Сi - не унифицируемы.

Цели BiQi называются производными от цели Gj и правила Cj. Цель Gj = Bik, где Bik входит в тело предложения Сi, называется порожденной Gi и Ci. Цель Gi, называется предшественником любой порожденной ею цели. Две цели с общим предшественником называются родственными целями.

Протоколом вычисления (Qi,Gi,Ci) логической программы называется последовательность пар (Gj i), где i- подмножество н. о. у. i полученного на i-й редукции и ограниченного переменными из G.

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

Интерпретатор решает вопрос G с помощью программы Р. Результатом работы интерпретатора будет пример G, если найдено доказательство такого примера, или отказ, если в процессе вычисления возник отказ. Заметим, что интерпретатор может и отказаться закончить вычисления.

Вход:Логическая программа Р цель G Результат: G, если это пример G, выводимый из Р. или отказ, если возник отказ Алгоритм: Начальная резольвента равна входной цели G Пока резольвента непуста, выполнить Выбрать такую цель А из резольвенты и такое (переименованное) предложение А:- В1, В2,..., Вn, n > 0 из Р, что А и А унифицируемы с и.о.у. (если нет таких цели и правила, то выйти из цикла). Удалить А и добавить В1, В2,..., Вn к резольвенте. Применить к резольвенте и к G. Если резольвента пуста, то результат-G, иначе - отказ.

Пример вопроса, для которого найдено доказательство, называется решением вопроса. Пример вопроса, для которого найдено доказательство, называется решением вопроса. Метод, в соответствии с которым добавляются и удаляются цели в резольвентах, называется методом расписания интерпретатора. В абстрактном интерпретаторе метод расписания не уточнен. Метод, в соответствии с которым добавляются и удаляются цели в резольвентах, называется методом расписания интерпретатора. В абстрактном интерпретаторе метод расписания не уточнен.

Рассмотрим решение вопроса конк([a,b],[c,d],Ls) с использованием приведенного интерпретатора. Начальная резольвента - конк([a,b],[c,d],Ls). Поскольку имеется единственная цель, то она и выбирается для редукции. Выбранным правилом будет конк([X|Xs], Ys, [X|Zs]):- конк(Xs, Ys, Zs). Унификатор цели и заголовка- {X=a, Xs=[b], Ys=[c,d], Ls=[a,Zs] }. Новой резольвентой будет пример терма конк(Xs, Ys, Zs) при применении унификатора, т. е конк([b], [c,d], Zs)

Эта цель выбирается на следующей итерации цикла. Выбирается то же предложение для отношения конк, но во избежание конфликта переменные должны быть переименованы. Выберем такой вариант: конк([Xl|Xsl], Ysl, [Xl|Zsl]):- конк(Xsl,Ysl,Zsl). Унификатор цели и заголовка- {Xl=a, Xsl=[b], Ysl=[c,d], Zs=[b| Zsl] }. Далее выбирается факт конк([ ],Zs2,Zs2); вновь производятся необходимые переименования переменных.

На этот раз унификатор– {Zs2=[c,d], Zs1=[c,d]}. Новая резольвента пуста, и вычисление заканчивается. Для получения результата вычислений применим соответствующую часть вычисленного н. о. у. Первая унификация привела к изменению Ls на [а|Zs]. Во второй унификации Zs превратилось в [b|Zsl]. Далее Zsl стало [c,d]. Объединяя, получим, что Li имеет значение [a|[b|[c,d]]], или, упрощенно, [a,b,c,d].

Вычисление может быть представлено протоколом. Для того чтобы протокол был понятнее, цели напечатаны с отступом относительно предшественника. Цель имеет глубину отступа d+1, если глубина отступа предшественника - d. конк([a,b],[c,d],Zs) Zs=[a|Zsl] конк([b],[c,d],Zsl)Zsl = [b| Zs2] конк([ ],[c,d], Zs2)Zs2 = [c,d] true Output: Zs = [a,b,c,d]

В качестве другого примера рассмотрим решение вопроса сын(S,аран). Вопрос редуцируется с использованием предложения сын(Х,Y) :- отец(Х,Y), мужчина (X). Наибольший общий унификатор - {X = S, Y = аран]. Применение подстановки дает новую резольвенту -отец(аран, S), мужчина (S). Это - конъюнктивная цель. В качестве очередной цели можно выбрать одну из двух целей. Выбор цели отец (аран,S) приводит к следующему вычислению.

Цель унифицируется с фактом отец (аран,лот), имеющимся в программе, и вычисление продолжается с заменой S на лот. Новая резольвента - мужчина (лот), она является фактом программы, и вычисление завершается. Протокол вычисления приведен в левой части рис. сын (S,apан) сын (S,apaн) omeu(apaн,S) S = лот мужчина(лот) S = лот мужчина(лот) отец (аран,лот) true true Рис. Различные протоколы, дающие одинаковое решение.

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

Решение вопроса, полученное с помощью абстрактного интерпретатора, может содержать переменные. Рассмотрим вопрос member (a,Xs) относительно программы, задающей отношение member. member(X,[X|Xs]).member(X,[Y|Xs]):-member(X,Ys). Его можно рассматривать как вопрос о том, какой список Xs содержит а в качестве элемента. Одно из решений, вычисленное абстрактным интерпретатором Хs =[a, Ys], т.е. список с головой а и произвольным хвостом. Решение, содержащее переменные, обозначает бесконечное множество решений - все их основные примеры.

В интерпретаторе имеются два выбора: выбор цели для редукции и выбор предложения для выполнения редукции. Оба выбора осуществляются в любой реализации вычислительной модели. Природа этих выборов принципиально различна. Выбор цели для редукции произволен; для успешного вычисления несущественно, какая цель выбрана. Если существует успешное вычисление при выборе данной цели, то существует успешное вычисление и при выборе любой другой цели. Два протокола описывают успешные вычисления (для задачи о сыне), различающиеся выбором цели на втором шаге вычисления.

Выбор предложения для выполнения редукции является недетерминированным. Не каждый выбор приводит к успешному вычислению. Например, в обоих протоколах мы могли совершить неверный выбор. Если бы мы редуцировали цель отец (аран,S) с помощью факта отец(аран,иска), то не смогли бы редуцировать появившуюся цель мужчина (иска). Во втором вычислении, если бы мы редуцировали цель мужчина(S) с помощью факта мужчина(исаак), то цель отец (аран,исаак) уже не могла быть редуцирована.

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

Альтернативные выборы, которые может сделать абстрактный интерпретатор при попытке доказать цель, неявно определяют дерево поиска. Если в дереве поиска существует путь, соответствующий доказательству цели, то интерпретатор «угадывает» этот путь. Однако могут быть построены и менее «умные», лишенные способности угадывать интерпретаторы, но обладающие теми же возможностями, что и абстрактный интерпретатор.

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

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