Абстрактный интерпретатор логических программ

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

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

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

Для более формального описания вычислений введем несколько полезных понятий. Вычислением цели Q = Qпрограммой Р называется, возможно бесконечная последовательность троек <Q, G, C> здесь Q, –конъюнктивная цель, G– цель, входящая в Q, C– предложение A¬B…B, с таким переименованием, что новые символы переменных не встречаются в Q, 0£j£1. Для всех i > 0 цель Qявляется или результатом замены G, на тело С, в Q, и применения подстановки Q, наибольшего общего унификатора термов G, и А, (Азаголовок С), или константой true, если G– единственная цель в Q, и телоС, пусто,или константой отказ если С, и заголовок С, не унифицируемы.

Цели BΘназываются производными от цели Gи правила С. Цель G_j = B, где Bвходит в тело предложения С, называется порожденной G, и С. Цель Gназывается предшественником любой порожденной ею цели. Две цели с общим предшественником называются родственными целями.

Протоколом вычисления (Q, G, C) логической программы называется последовательность пар <G,Θ>, где Θ– подмножество н.о.у. Θ, полученного на i-й редукции и ограниченного переменными из G.

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

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

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

Вход: Логическая программа Р

цель G

Результат:GΘ, если это пример G, выводимый из Р, или отказ, если возник отказ

Алгоритм:Начальная резольвента равна входной цели G

Пока резольвента непуста, выполнить

Выбрать такую цель А из резольвенты и такое (переименованное) предложение

А'¬В, В,..., B, п³0 из Р, что А и А' унифицируемы с н.о.у. Θ

(если нет таких цели и правила, то выйти из цикла).

Удалить А и добавить В,В,... ,B, к резольвенте.

Применить Θ к резольвенте и к G.

Если резольвента пуста, то результат – G,

иначе результат – отказ.

Рис. 4.2. Абстрактный интерпретатор логических программ.

Пример вопроса, для которого найдено доказательство, называется решением вопроса.

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

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

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

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

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