Содержание к диссертации
Введение
1. Формальная теория 13
1.1. Основные определения 13
1.2. Нерекурсивные и рекурсивные детерминированные С-модели 16
1.3. Постановка задачи 19
Выводы к главе 1 19
2. Алгоритмы планирования и синтеза программ 21
2.1. Проблема эффективности и общие принципы построения машины вывода для устойчивых баз знаний 21
2.2. Планирование и синтез в классе НДС-моделей 24
2.2.1. Правила вывода 24
2.2.2. Трансформация вариантной части 25
2.2.3. Компиляция НДС-модели 26
2.2.4. Постановка задачи и схемы алгоритмов вывода 31
2.2.5. Извлечение программы из доказательства 38
2.3. Планирование и синтез в классе РДС-моделей 41
2.3.1. Формальная модель доказательства 41
2.3.2. Подготовка данных и алгоритм вывода на РДС-модели 44
2.4. Программная реализация 50
Выводы к главе 2 60
3. Оценка эффективности 61
3.1. Расчет вычислительных затрат на осуществление вывода в классе С-моделей 61
3.2. Получение вида зависимости вычислительных затрат от объема спецификации РДС-модели 64
3.3. Экспериментальные результаты 65
Выводы к главе 3 68
4. Интерпретация с-модели для ряда логических исчислений 69
4.1. Трансформация спецификаций языка Пролог в конструкции теории С-моделей 70
4.2. Упрощенный метод интерпретации для ряда логических исчислений 75
4.3. Реализация методов преобразования и экспериментальные результаты 78
Выводы к главе 4 83
Заключение 84
Список литературных источников 86
Список сокращений 92
Приложения 93
Приложение 1. Полная модель данных компиляции и доказательства 93
Приложение 2. XML-схема описания С-модели 94
Приложение 3. Исходный код алгоритма планирования 96
Приложение 4. Исходный код процедуры очистки результатов вывода 103
Приложение 5. Пример исходной спецификации РДС-модели для проведения тестов 105
Приложение 6. Пример спецификации в формате CNF 108
Приложение 7. Пример спецификации в формате ТМЕ 109
Приложение 8. Пример спецификации в формате TPTP-FOF ПО
Приложение 9. Пример спецификации для дескриптивной логики на языке OWL Ill
- Основные определения
- Проблема эффективности и общие принципы построения машины вывода для устойчивых баз знаний
- Расчет вычислительных затрат на осуществление вывода в классе С-моделей
- Трансформация спецификаций языка Пролог в конструкции теории С-моделей
Введение к работе
В современном мире информационных технологий наблюдается постоянный рост интереса к методам интеллектуальной обработки информации. Эти тенденции определяются, с одной стороны, растущими объемами и интеграцией хранилищ данных, а с другой - постоянным ростом спроса на информационные услуги, связанные с обработкой этих данных. Указанные факторы проявляются как на уровне корпоративных информационных систем в области медицины, экономики, прогнозирования и др., так и на глобальном уровне, где одним из следствий возросших потребностей в «интеллектуализации» всемирной сети стало возникновение парадигмы Semantic Web. Основой многих современных систем интеллектуального поиска и обработки информации являются машины логического вывода, реализующие те или иные методы доказательства логических теорем. Примерами таких систем являются экспертные системы, системы поддержки принятия^решений, интеллектуального поиска и др. Одной'" из основных проблем построения машин вывода является скорость получения доказательства, которая обычно определяется как количество вычислительных операций, требуемых для обработки базы знаний заданного объема. Следует отметить, что эффективность генерации вывода также зависит от степени выразительности языка описания предметной области. Некоторые современные реализации машин вывода для логики высказываний (построенные, например, на базе табличного (tableaux) метода) в ряде случаев позволяют добиться линейных вычислительных затрат на осуществление вывода относительно объема базы знаний [33]. В то же время вывод на более выразительных моделях, описанных на языке логики предикатов, зачастую приводит к полиномиальному или даже экспоненциальному росту вычислительных затрат. Другой важной проблемой теории искусственного интеллекта является автоматический синтез программ. По отношению к общей проблеме логического вывода, задача синтеза программ в традиционной постановке
4 является более узкой. Алгоритмы синтеза применяются в основном в CASE-системах, а также в научно-практических разработках, связанных со сложными математическими вычислениями и необходимостью построения сложных алгоритмов. Примерами последних являются математические расчеты в астрономии, авиационно-космической промышленности, численной механике, проектирование аппаратного обеспечения, разработка промышленных систем управления и др. Однако, задача синтеза может быть интерпретирована как извлечение (трассировка) последовательности шагов доказательства, приводящих к заданному следствию. В диссертации показано, как предлагаемый подход может быть применен к некоторому подмножеству задач, выраженных на распространенных логических языках — логике высказываний, логике первого порядка и дескриптивной логике, что значительно расширяет возможности практического применения предлагаемых алгоритмов.
Диссертация посвящена исследованию алгоритмов логического вывода в специальных исчислениях и синтеза линейных программ, программ с-подпрограммами и рекурсией. Область исследования диссертационной работы ограничена дедуктивным подходом, где программа извлекается из доказательства соответствующей теоремы.
Появление первых работ в области автоматического синтеза программ на основе дедуктивного подхода приходится на 60-е гг. прошлого столетия. В работах Р. Уолдингера, Ц. Ченя, Р. Ли, 3. Манны [46^48, 62] при доказательстве теоремы использовался метод резолюций Робинсона и различные его вариации, направленные на повышение вычислительной эффективности [27, 31].
В 70-ее годы появился язык логического программирования Пролог, который в последующие два десятилетия получил широкое распространение и был использован при решении множества практических задач, в частности при построении экспертных систем. На базе Пролога появилось множество реализаций, решающих задачу синтеза программ, например AutoBayes, NuPrl, Oyster и др. [6, 39, 41]. Однако, несмотря на большие функциональные
5 возможности, использование в Прологе стратегии вывода от целей к посылкам приводит к издержкам, связанным с необходимостью возврата при установлении недостижимости очередной подцели (так называемый «бэктрекинг») [26, 28, 40, 44]. В результате, решение сложных задач вывода и синтеза может привести к экспоненциальному росту вычислительных затрат, что значительно ограничивает использование Пролога для построения эффективных систем интеллектуальной обработки данных.
В последние десятилетия направление исследований в области автоматического синтеза программ сместилось от идеи полной замены человека к задаче помощи программисту при разработке алгоритмов, выполнении верификации программ и т.п. Основная критика традиционного подхода заключается в низкой производительности алгоритмов и наличии проблемы полноты вывода, а также несовместимости конструкций логических языков и языков программирования.
Важный теоретический и практический вклад в развитие данного1 направления и преодоление перечисленных проблем- внесли работы отечественных исследователей. В частности, идея альтернативного метода вывода от аксиом к целям, впервые высказанная Г. Генценым [40], получила развитие в исследованиях С. Ю. Маслова и Г. Е. Минца [7-9], где приобрела название «обратного метода». В конце 70-х гг. прошлого столетия Н. Н. Непейвода предложил формальную теорию, устанавливающую соответствие между предложениями доказательства теорем и терминами структурного программирования [12-14]. Э. X. Тыугу предложил аппарат вычислительных моделей, использование которого для синтеза ветвящихся программ и программ с подпрограммами обосновано в публикациях [10, 11, 30]. В работах А. Я. Диковского на основе теории вычислительных моделей исследованы возможности синтеза программ с рекурсией [1, 2]. Теория структурных функциональных моделей (С-моделей) В. Б. Новосельцева [17] является развитием теории вычислительных моделей и обладает теоретически
доказанным свойством полноты вывода и возможностью построения алгоритмов решающих задачу вывода за полиномиальное время за счет использования внешней памяти.
В настоящей работе предлагается вариант реализации алгоритма автоматического логического вывода и синтеза программ с использованием теории структурных функциональных моделей в качестве базового аппарата для формализации знаний о предметной области. Для ограничения пространства вывода и снижения вычислительных затрат разработаны специальные структуры данных внутреннего представлении исходной спецификации. Особое место в диссертации отводится планированию программ с подпрограммами и рекурсивными конструкциями, где предлагается реализация оригинального метода «динамической развертки», позволяющего избежать дополнительных затрат на хранение информации о вложенности' подпрограмм и решить проблему их поиска без снижения производительности алгоритма.
Следует также отметить, что большинство современных алгоритмов логического вывода ориентированы на «оперативную» обработку базы знаний, исходя из предположения, что содержимое базы знаний постоянно меняется. В то же время существует ряд предметных областей, где база знаний меняется достаточно редко, что позволяет получить дополнительный прирост производительности при осуществлении логического вывода и синтеза путем использования внешней памяти. Предлагаемый в работе подход специальной подготовки базы знаний предназначен для применения на устойчивых моделях и показывает значительный прирост скорости вывода по сравнению с существующими аналогами. Отметим, что возможность динамического внесения изменений в подготовленные структуры данных не исключается, однако не входит в рамки настоящего диссертационного исследования.
Цель работы и задачи исследования. Целью исследования является разработка высокопроизводительных алгоритмов логического вывода и синтеза
7 программ на структурных функциональных моделях, а также адаптация этих алгоритмов для решения задач, выраженных в языках традиционных логических исчислений.
Для достижения указанной цели в работе решаются следующие задачи:
Формальное определение элементов модели исходных данных и формулировка задачи логического вывода и синтеза программ на базе теории структурных функциональных моделей.
Определение общих принципов, требований и архитектуры машины вывода.
Формулировка правил вывода и разработка структур данных компиляции исходной спецификации с целью снижения вычислительных затрат при выполнении задачи планирования.
Разработка и программная реализация алгоритмов планирования и синтеза. программ.
Расчет вычислительных затрат и экспериментальная оценка скорости разработанного алгоритма с использованием тестовых выборок данных.
Сопоставление выразительных возможностей и определение правил трансформации элементов спецификации языка Пролог в конструкции теории структурных функциональных моделей.
Адаптация разработанной машины вывода для решения задач, выраженных в языках ряда логических исчислений: логики высказываний, логики первого порядка, дескриптивной логики.
Экспериментальное сравнение производительности разработанной машины вывода с существующими аналогами.
Объектом исследования является область теории искусственного интеллекта, связанная с проблемами автоматического доказательства логических теорем и синтеза программ.
Предметом исследования являются вычислительные модели и алгоритмы логического вывода и синтеза программ.
Методы исследований. В работе использованы элементы теории
структурных функциональных моделей, теории множеств, логики
высказываний, первого порядка и дескриптивной логики, методы структурного
программирования.
Научная новизна работы заключается в следующем:
На базе теории структурных функциональных моделей разработаны алгоритмы логического вывода и синтеза программ, обладающие высокими показателями скорости вычислений за счет представления исходной спецификации в виде специальных структур данных и использования метода динамической развертки, позволяющего сократить пространство вывода при помощи организации стека подпрограмм и рекурсивного планирования на иерархии подсхем.
На основании анализа элементов спецификации языка Пролог и сопоставления их с конструкциями теории структурных функциональных моделей введены новые формальные правила и ограничения трансформации задач вывода на логике первого порядка в задачи планирования на структурных функциональных моделях.
Произведена адаптация разработанной машины вывода для ряда задач, выраженных в языках традиционных логических исчислений (логики высказываний, логики первого порядка и дескриптивной логики) и экспериментально подтверждена более высокая скорость вычислений по сравнению с существующими аналогами.
Практическая ценность и реализация результатов работы. Предлагаемые структуры данных и алгоритмы планирования реализованы в виде прикладного программного пакета. Разработанное программное обеспечение может быть использовано для решения широкого круга задач, связанных как непосредственно с исследованиями в области синтеза программ, так и с решением проблем прикладного характера в различных областях, таких как прогнозирование, интеллектуальный поиск (data mining), построение
9 экспертных систем, систем поддержки принятия решений и т.д. Предлагаемый подход хорошо масштабируется и особенно эффективен при обработке баз знаний большого объема.
Предложенные модели данных компиляции и алгоритмы вывода были внедрены в ООО «ФлексСофт» при разработке медицинской информационной системы для обработки экспертной базы знаний ExpertDoc. Применение предлагаемых подходов позволило многократно повысить скорость поиска противопоказаний лекарственных препаратов и реализовать дополнительные возможности трассировки найденного решения.
Результаты работы также были использованы в проекте построения единой информационной среды Томского политехнического университета для решения задачи определения прав доступа пользователей (сотрудников университета) к информации о студентах. Применение предложенной стратегии вывода позволило реализовать эффективный алгоритм вычисления путем обхода дерева решений.
Предложенный подход логического вывода и синтеза программ используется в учебном курсе теории языков программирования и методов трансляции, который преподается студентам Томского политехнического университета.
Основные положения, выносимые на защиту:
1. Разработанный алгоритм вывода и синтеза программ, использующий
метод динамической развертки и стратегию предварительной подготовки
данных, характеризуется следующими показателями количества затрачиваемых
операций относительно длины описания модели предметной области:
а) линейная зависимость для программ с условиями и подпрограммами;
б) полиномиальная зависимость не выше третьей степени для программ с
рекурсией.
2. Предложенный метод сопоставления элементов спецификации языка
Пролог и конструкций теории структурных функциональных моделей
10 определяет принципиальную возможность, правила и ограничения трансформации задач вывода, выраженных на языке логики первого порядка в задачи планирования на структурных функциональных моделях.
Разработанный алгоритм вывода на структурных функциональных моделях может быть использован для доказательства ряда логических теорем,, сформулированных на языках логики высказываний, логики первого порядка и дескриптивной логики.
Результаты экспериментов подтверждают высокие показатели производительности разработанной машины вывода по сравнению с существующими аналогами.
Достоверность полученных результатов подтверждается полнотой и корректностью теоретических обоснований и результатами экспериментов, проведенных с помощью разработанной программной реализации.
Апробация работы.
Основные результаты работы представлены в виде:
3-х статей в журнале «Известия ТПУ» Томский политехнический университет, г.Томск,
а также докладов на ряде научных форумов, среди которых можно отметить следующие:
«IX Всероссийская конференция молодых ученых по математическому моделированию и информационным технологиям (YM-2008)» (г. Кемерово, 28-30 октября 2008 г.);
Международная конференция «Программные системы: теория и приложения (PSTA-2009)» (г. Переславль-Залесский, ИПС РАН, 13-15 мая 2009г.);
Международная конференция «Теоретические и прикладные вопросы
современных информационных технологий (ТиПВСИТ'2009)»
(г. Улан-Удэ, 20-26 июля 2009 г.)
Всего по теме диссертации опубликовано 6 работ, из них 3 статьи в
журнале, входящем в перечень ВАК, 2 статьи опубликованы по материалам
конференций и 1 работа опубликована в качестве тезисов доклада на
конференции.
Личный вклад:
Формальное описание модели данных и постановки задачи построены автором на основе теории структурных функциональных моделей В. Б. Новосельцева.
Модели данных и алгоритмы синтеза программ, включая оригинальный алгоритм динамической развертки, разработаны автором и являются реализацией задач, поставленных научным руководителем аспирантского исследования.
Формальное обоснование применения разработанной машины вывода для решения задач, сформулированных на языках логики высказываний, логики первого порядка и дескриптивной логики, предложено лично автором.
Реализация машины вывода и экспериментальные оценки производительности выполнены лично автором.
Объём и структура работы. Диссертация состоит из введения, четырёх глав, заключения, списка источников из 62 наименований и 9 приложений. Содержит 21 рисунок и 1 таблицу.
В первой главе вводятся основные определения и соглашения, предлагается формальная модель описания предметной области и постановки задачи планирования и синтеза на базе теории структурных функциональных моделей.
Во второй главе рассматривается общая архитектура машины вывода, предлагаются структуры данных для преобразования (компиляции) исходной модели, определяются формальные правила вывода и предлагается реализация алгоритмов планирования и синтеза программ.
12 В третьей главе дается теоретическая и экспериментальная оценка производительности разработанного алгоритма планирования.
В четвертой главе рассматривается подход к представлению структурных вычислительных моделей в виде спецификаций языка Пролог. Указаны ограничения и преимущества предлагаемого метода. Предложен упрощенный подход интерпретации конструкций структурных вычислительных моделей для ряда логических исчислений. Приведены результаты тестовых испытаний и сравнения с существующими аналогами.
Основные определения
Определение 1.1. Описание модели предметной области Е, называемое сигнатурой, состоит из четырех множеств {A, F, Р, D) и представляет собой множество атрибутов, функциональных связей, селекторов (предикатов) и схем отношений соответственно. Считается также, что выделено некоторое непустое подмножество первичных или примитивных схем EdD.
Атрибуты, составляющие множество А, фиксируют некоторые характеристики объекта предметной области. Каждый атрибут связан со схемой из множества D. Если TeD\E, то связь атрибута а со схемой Г выражается записью а: Г и атрибут называется непервичным. В противном случае, если ТєЕ, то атрибут является первичным или примитивным (например, целое число, строка) и запись а: Г может быть заменена просто на а, если ссылка на схему не имеет значения. Определение 1.2. Выражение вида: /:аи...,ап- ао, (1.1) где at, і = 0...П — имена атрибутов, называется функциональной связью (ФС). В записи (1.1)/- имя ФС, at - аргументы (/=1.. .ті), а0 - результат ФС. Неформально функциональная связь трактуется как возможность вычисления атрибута «о по значениям атрибутов а і,..., а„ с помощью отображения/ При описании модели предметной области на языке структурных функциональных моделей важнейшим является понятие схемы. Определение 1.3. Схема Г атрибута t определяется выражением вида: t:T=(aoQ.Soo, аоь оь &on -Son ifpl(...)zDaio:S]0,an:Sn...\f_set[ (1.2) ... ;? (...)= аы .Бы, akx:Skl... f_setkendif \f_set\ где tsA — имя атрибута схемы, TsD\E обозначает имя схемы. Для всех возможных значений индексов i, j символы SyEiD обозначают собственные подсхемы, ауєА — собственные атрибуты схемы Т.
Обозначение f_set в заключительной части определения схемы скрывает множество собственных ФС схемы Т.
Часть выражения (1.2) находящаяся между обозначениями if...endif является опциональной и определяет вариантную или условную часть схемы. Вариантная часть состоит из условных ветвещ разделенных символом , которые соответствуют традиционной программной конструкции if..elseif..else или ветвям оператора case. В условных ветвях символы ріЄР, i=\...k называются выбирающими селекторами и представляют собой логическую функцию вида pi(ano,...), где ап0)... — набор атрибутов заголовка схемы Т. Следом за описанием селектора pt указываются условные атрибуты al0:Sio, an .Sn... Выражение f_sett, следующее за описанием условных атрибутов, скрывает множество условных ФС. Условная ФС может включать в качестве аргументов и результатов атрибуты заголовка схемы и условные атрибуты соответствующей ей ветви. Условие pi определяет допустимость атрибутов и ФС, входящих в /-ю ветвь. Иными словами, условные атрибуты и ФС имеют смысл только в соответствующей им ветви вариантной части схемы.
Далее, определим, какие имена атрибутов порождаются в описании схемы. Определение 1.4. Пусть t — имя непервичного атрибута, связанного со схемой Г, т.е. t:T. Пусть ао,...,ап — имена собственных атрибутов, определенных в схеме Т. Тогда, t.ao, ..., t.an — также являются именами атрибутов. Набор атрибутов ао,...,ап, будем называть суб-атрибутами по отношению к атрибуту t.
Теперь определим некоторые правила, ограничивающие ФС, входящие в множества/ е описания схемы.
Определение 1.5. Функциональная связь /І ai,...,a„— ао, входящая в описание схемы Т, является допустимой если ао,...,ап — примитивные атрибуты схемы Т, либо примитивные суб-атрибуты непервичного атрибута, принадлежащего схеме Т. Схема называется синтаксически замкнутой, если fjset содержит только допустимые ФС. Предметом исследования в настоящей работе являются только синтаксически замкнутые схемы.
Кроме этого ФС, входящие в определение схемы, должны отвечать следующим требованиям: S ФС содержит по крайней мере один собственный атрибут схемы; S в наборе f_set нет ФС, в которые вовлечены атрибуты из разных вариантных ветвей схемы или атрибуты из вариантных частей ее подсхемы; S длина любого атрибута, связанного ФС, не превышает двух. Для пояснения введенных обозначений приведем пример модели, описывающей простейшую систему уравнений: { л;;.х 0 ., х + п; х = О Основная схема: Т=(х,у ifpi(x) = /п: х-»у ... /?2(Х) = г:і? /2ь x- r.m;f22: r.n, х- у endif) Схема для вычисления квадрата числа: R = (in, п \fsq: m —» п). 1.2. Нерекурсивные и рекурсивные детерминированные С-модели Определим понятие структурной функциональной модели. Определение 1.6. Конечная совокупность схем M=(T\,...,TS) называется структурной (С-) функциональной моделью. Каждая схема Г„ i=\...s должна являться примитивной или удовлетворять определению 1.3. Определение 1.7. С-модель M=(Ti,...,Ts) является синтаксически замкнутой, если подсхемы, встречающиеся в определении каждой схемы 7}еМ, являются элементарными либо входят в состав модели М. Далее, введем понятие детерминированной схемы. Определение 1.8. Схема является детерминированной, если она не содержит вариантной части либо ее вариантная часть содержит две взаимоисключающие условные ветви и определяется записью ifp(...) з яоо оо, ЯоьЯоі \f-JetQ О а\о \ ь an:Sn... \f_setx endif Данное определение означает, что «оо оо? Яоь оі I fjseto имеют смысл при истинности р, a a\o:Sw, аи ц... \ f_set\ — в обратном случае. Наличие у некоторого атрибута а условия р может быть выражено записью alp, а обратное условие (соответствующее else в двухальтернативной вариантной части) обозначается я/ р. Определение 1.9. С-модель M=(T\,...,TS) является нерекурсивной детерминированной (НД-) С-моделыо, если она удовлетворяет следующим условиям: S модель Мявляется синтаксически замкнутой (см. Определение 1.7); S схемы T\,...,TS являются детерминированными; S любая схема 7} модели М определяется через элементарные атрибуты, либо через схемы, предшествующие ТІ в модели М. Введение рекурсивных выражений порождает в описаниях схем конструкции следующего вида: 7\ = (..., t2:T2, ...), Т2 = (-.-, Н\Т$, ...), ... , Tk = (..., t\.T\, ...), где 7\, Т2, Тъ, ..., Tk- схемы С-модели. Определение 1.10. Будем называть рекурсию явной, если для рекурсивного вхождения Ті = (..., t2\T2, ...), ... , Tk (..., h .Ti, ...), значение k=\, т.е. T\ = (..., t\\T\, ...), и неявной или опосредованной, если & 1. Соответственно, вхождение атрибута ti .T\B схему Tk при Аг=1, будем называть явным, а при k l неявным или опосредованным вхождением рекурсивной подсхемы. Определение 1.11. С-модель A4=(Ti,...,Ts) является рекурсивной детерминированной (РД-) С-моделъю, если она удовлетворяет следующим! ограничениям: S модель Мявляется синтаксически замкнутой (см. Определение 1.7); S схемы Ti,...,Ts являются детерминированными; S для каждой Т:еМ явные или опосредованные вхождения подсхем вида Ґ.ТІ, могут появляться только в одной из двух альтернативных ветвей схемы ТІ.
Отметим, что введенное здесь определение РДС-модели идентично по смыслу с определением, приведенным в [17, 18], однако избегает использования понятия полной развертки схемы.
Проблема эффективности и общие принципы построения машины вывода для устойчивых баз знаний
В [18] показано, что полная развертка НДС-модели соответствует некоторой детерминированной (Д-) модели Диковского [1]. При этом, А. Я. Диковским доказано, что при решении задачи синтеза на Д-моделях без использования внешней памяти, задача является TVP-полной. Класс РДС-моделей включает в себя класс НДС-моделей. В [18] также показано, что на развертке РДС-модели теоретически возможно построение алгоритмов вывода и синтеза, которые решают задачу за полиномиальное время, а также определен принцип динамической развертки, позволяющий значительно сократить издержки. В связи с этим перспективной задачей представляется построение машины вывода, использующей внешнюю память, избегающей построения-статической развертки на подсхемах и обладающей полиномиальными характеристиками отношения вычислительных затрат к объему исходной модели.
Кратко поясним основные составляющие предлагаемой архитектуры машины вывода. Чтение файла описания С-модели. Исходная С-модель поставляется в виде спецификации, описанной на языке XML. Отметим, что формат описания исходных данных не имеет принципиального значения, так как при чтении модели данные преобразуются к единому внутреннему представлению. Язык XML был выбран лишь потому, что он является наиболее универсальным и распространенным языком описания данных. Внутреннее представление С-модели представляет собой результаты синтаксического анализа и разбора (парсинга) файла описания, представленные в виде простых программных структур.
Для проведения экспериментов машина вывода дополняется модулем генерации С-модели. Этот модуль выполняет автоматическое создание модели требуемого объема исходя из заданного количества элементов и набора исходных и целевых атрибутов. Более подробное описание процесса генерации моделей для тестов приводится в главе 3, посвященной экспериментальной оценке производительности машины вывода.
Проверка и подготовка структур данных (компиляция). При реализации машины вывода многие проблемы можно преодолеть за счет подбора оптимальных с точки зрения эффективности информационных структур данных, используемых при осуществлении планирования и синтеза. Основная идея, позволяющая добиться высокой скорости алгоритма планирования, заключается в компиляции исходных данных (схем отношений, ФС, атрибутов, условий и т.д.) в специальные структуры данных, оптимизированные для решения задач вывода на данной выборке. Результаты компиляции не должны зависеть от постановки задачи, что позволяет использовать ее результаты многократно для различных задач вывода. Благодаря модулю загрузки/выгрузки результатов компиляции, структуры», данных могут быть выгружены во внешнюю память для повторного использования в дальнейшем.
Формулировка логической теоремы. Постановка задачи, построенная согласно определению 1.12, представляет собой файл, содержащий список исходных и целевых атрибутов, а также имя головной схемы в которой определены эти атрибуты. Модуль формулировки теоремы читает файл постановки задачи и выполняет поиск перечисленных элементов описания постановки задачи среди элементов откомпилированной модели. Исходные и искомые атрибуты в совокупности с головной схемой, представленные-в виде структур данных компиляции и являются входными данными для процедуры планирования.
Модули логического вывода (планирования) и извлечения (синтеза) программы не используют каких-либо дополнительных структур данных, помимо элементов модели данных компиляции. Результатом вывода является набор элементов данных, являющихся шагами доказательства достижимости целевых атрибутов на основе набора исходных атрибутов. При этом результаты планирования могут оказаться избыточными с точки зрения построения конечной программы. Задачей алгоритма синтеза является формирование минимально необходимой последовательности шагов доказательства, и интерпретации ее в заданном формате, соответствующем потребностям пользователя (например, файл с текстом программы).
Из приведенного описания видно, что ядро приложения составляют модули компиляции, формулировки теоремы и логического вывода. В последующих разделах главы рассматриваются формальные правила вывода, предлагаются модели данных компиляции, постановки задачи и доказательства и приводится описание алгоритмов планирования и синтеза, реализующих применение правил вывода на предлагаемых структурах данных.
Данное правило определяет условие допустимости р атрибута х при наличии условия допустимости р функциональной связи f, т.е. при достижимости условных аргументов А условной ФС f, утверждается достижимость результата ФС в соответствующей ветви условия.
Условие xlp8c p определяет достижимость атрибута при всех альтернативных ветвях и тождественно записи х без указания условий допустимости.
Расчет вычислительных затрат на осуществление вывода в классе С-моделей
Прежде всего, отметим, что приведенные в этом разделе расчеты позволяют получить лишь приблизительные значения времени работы алгоритма, так как учитываются далеко не все типы временных затрат. Основной целью здесь является математическое обоснование линейных показателей скорости работы алгоритма вывода на НДС-моделях, описанного в гл. 2, относительно объема исходной спецификации. Операции, затраты на которые были взяты в расчет при оценке производительности, содержат следующие действия: создание/изменение сложных объектов (например, шагов доказательства); помещение или получение очередного объекта из списка.
Игнорируются следующие типы операций: S сравнения примитивных значений и проверки истинностного значения логических переменных; S установки значений примитивных переменных. Также игнорируется операция проверки достижимости конечных целей на каждом шаге доказательства, затраты на которую являются линейными. Кроме того, для ряда задач, эта операция может быть исключена без ущерба для функциональных возможностей алгоритма.
Пусть s обозначает общее количество ФС схемы, a aj - количество аргументов у-й ФС. Тогда, для случая линейной программы без условий и подпрограмм время работы алгоритма вывода определяется формулой:
При осуществлении вывода на схеме с подпрограммами для каждой доставляющей ФС в расчет затрат включаются затраты fpz п/п - на добавление аргумента вызова подпрограммы; fmeK " - на добавление/получение вызова подпрограммы из стека.
Пусть также г обозначает количество схем в исходной спецификации, и, — количество непервичных атрибутов (т. е. количество вызовов подпрограмм) в і-и схеме, a bik - количество ФС, доставляющих вложенные атрибуты /с-го непервичного атрибута в г -й схеме (т. е. количество аргументов вызовов подпрограммы).
Дополнительные затраты при работе в классе РДС-моделей приходятся на поиск потенциальных рекурсивных вхождений и построение замыкания. В остальном введение рекурсивных конструкций не ухудшает общей оценки скорости работы алгоритма, т. к. вывод на подзадачах {t:T\, А0, XQlp) и {t\.T\, t]JC0 , XQI P) (2 и 3 этапы на рис. 2.5) проводится тем же способом, что и основной алгоритм поиска решения и полностью в него включается. Целью приведенных ниже расчетов не является вывод формулы расчета скорости, а получение вида зависимости скорости вычисления от объема исходных данных. В п. 3.1 приведена оценка времени работы алгоритма на схемах с условиями и подпрограммами, которая выражается полиномом первой степени T(r, s, а, и, Ь), где г - количество схем в модели; s — количество не доставляющих ФС каждой подсхемы; а — количество аргументов каждой ФС; и — количество непервичных атрибутов в каждой схеме; Ъ - количество доставляющих ФС каждой схемы.
Рассмотрим предельно сложный случай РДС-модели. Для. начала введем переменную п, обозначающую количество атрибутов (как заголовка, так и вариантной части) каждой схемы. Предположим, что п для всех схем одинаково. Так как s n, примем s=n. Предположим, что.каждая схема включает в себя вызовы всех подсхем модели. Тогда и=г и г п. Примем г=п, следовательно и=п.
С учетом принятых допущений оценка сложности алгоритма поиска рекурсивного вхождения определяется Тпоискрекурс1Ш 0(п2).
Предположим теперь, что рекурсивное вхождение встречается в каждой схеме и опосредовано всеми подсхемами модели и затрагивает все ФС этих схем (входные ФС нерекурсивной ветви условия и ФС выхода из рекурсивной подсхемы не исключаем). При допущении, что построение замыкания требует максимального количества итераций, равного количеству доставляющих ФС каждой подсхемы (равное Ь), сложность алгоритма построения всех замыканий определяется Тзалшкант 0(Ь-пъ).
Из приведенных результатов, видно, что скорость вычислений на РДС-модели не выходит за рамки зависимости от объема исходных данных модели в виде полиномиальной функции третьей степени. Отметим, также, что предельный случай, используемый для расчетов, имеет мало общего с реальными практическими задачами, где оценки сложности алгоритмов поиска рекурсии и построения замыкания обычно не превышают 0(п2) и Оф-п2) соответственно.
Экспериментальная оценка производительности разработанной машины вывода производилась для пяти типов задач: линейные программы, программы с вариантной частью без подпрограмм, программы с подпрограммами, и, наконец, рекурсивные программы с необходимость и без необходимости построения замыкания. Результаты экспериментов показаны на рис. 3.1.
На вход машины вывода подавались сгенерированные схемы с возрастающим количеством ФС от 10 до 250, связанных таким образом, чтобы обеспечить необходимость обработки всех ПВ при осуществлении планирования. Каждой сгенерированной ФС назначалось одинаковое количество аргументов и одинаковое количество целей, что позволило оценивать скорость относительно количества ФС, без учета количества аргументов. Пример исходной спецификации для проведения тестов представлен в Приложении 5.
Генерация данных и осуществление вывода для каждой модели проводилось многократно для сглаживания побочных эффектов. При генерации схем с вариантной частью, при участии в схеме п ФС, в каждую вариантную часть помещалось (п-6)/2 условных ФС, чтобы обеспечить близкие к максимальным суммарные затраты на обработку условных конструкций согласно формуле (3.2). Генерация схем с условиями и подпрограммами производилась с таким расчетом, чтобы обеспечить максимальное количество подсхем с максимальной степенью вложенности этих подсхем. Каждая пара ФС была представлена в виде схемы, включающей в себя вызовы других подсхем. Оценка производительности при построении программ с рекурсией проводилась на моделях, содержащих один рекурсивный вызов, опосредованный всеми подсхемами модели, и требующий двукратного прохождения этих подсхем для построения замыкания.
Трансформация спецификаций языка Пролог в конструкции теории С-моделей
Представленный ниже метод трансформации конструкций языка Пролог использует результаты, приведенные в работах [15, 20], однако дополняет последние более полным описанием метода преобразования переменных, многоместных предикатов и функций.
Согласно стандарту, базовая спецификация языка Пролог включает в себя: 1. Описание фактов в виде предикатов с параметрами. 2. Хорновские. правила — импликативные выражения связывающие набор предикатов-посылок с предикатом-следствием. Предикаты, входящие в правило, могут включать в себя переменные. 3. Целевое утверждение - предикат, определяющий задачу логического вывода. При описании конструкций языка Пролог будем придерживаться традиционных правил: S Предикаты обозначаются заглавными латинскими буквами: Р, Q, R, S; S Константы объявляются с помощью строчных символов, стоящих в начале латинского алфавита: а, Ь, с; S Переменные с помощью строчных символов, стоящих в конце латинского алфавита: х, у, z; В соответствии с введенными обозначениями, формализованная спецификация на языке
Отметим, что способ эффективной реализации предикатов в виде ФС является отдельной задачей и требует независимого исследования как на предмет полноты так и на предмет эффективности. В данной работе 1 Здесь и далее символ « - » интерпретируется как «взаимно-однозначное соответствие» предлагается лишь теоретическая база для некоторого вычислительного аппарата, реализующего нахождение фактов путем подстановки индивидных значений. Одним из вариантов реализации может служить язык запросов к базе данных фактов, подобный SQL в реляционных базах данных, однако этот вопрос выходит за рамки настоящего исследования. 4. Предикаты, отражающие факты, отражают множество кортежей, удовлетворяющих соответствующей схеме и формируют некоторую интерпретацию (реализацию) ФС, объявленных в предыдущем пункте. 5. Каждое вхождение предиката-посылки в правую часть правила Н, определяет вхождение атрибута соответствующего непервичного типа в заголовок схемы, соответствующей предикату-следствию этого правила: 6. Переменные, входящие в предикаты-посылки правой части правила К преобразуются в атрибуты заголовка схемы, соответствующей предикату следствию. Эти атрибуты служат доставляющими атрибутами подсхем, соответствующих предикатам правой части правила. Р0:-..., РД/о,...,гД... «- Т0 = (..., г0)..., rh..., tt:Ti /ю: ro- ti.ro,...,frf: r,-» . ,...,/ : fc/ -»r0,...,/V. Urj- rj,...) 7. Функции, входящие в исходную спецификацию (если таковые допускаются) преобразуются в ФС соответствующих предикатов без изменений.
С-моделей несколько сужает общую процедуру вывода и круг задач для исчисления первого порядка, решаемых в Прологе. Однако подобные ограничения являются достаточно обоснованными, так как снимают некоторые известные проблемы, например, использование спецификаций, приводящих к «зацикливанию» и необходимости искусственного торможения вывода.
Таким образом, предложенный метод трансформации практически полностью покрывает формальную модель спецификаций Пролога, что в свою очередь, определяет множество задач логики первого порядка, которые могут быть решены в рамках теории С-моделей. В следующем разделе определяется класс задач ряда логических языков, которые могут быть решены с помощью разработанной реализации машины вывода.
Приведенные в п. 4.1 методы трансформации позволяют использовать разработанные алгоритмы вывода на С-модели для автоматического доказательства весьма широкого множества задач логики первого порядка, где-в выражения вовлекаются многоместные предикаты, функциональные символы, индивидные значения (константы), кванторы и т.д. Однако, реализация представленного подхода, и в особенности пункта 3 правил трансформации, представляет большие трудности. В связи с этим, предлагается упрощенный вариант трансформации конструкций С-модели в Хорновские выражения на различных логических исчислениях, который позволяет выполнять вывод с помощью уже реализованных программных алгоритмов, описанных в гл. 2. Далее, в п. 4.3. эти методы используются для. сравнения производительности разработанной машины вывода с существующими, аналогами.
Одной из важнейших возможностей ДЛ является возможность построения иерархий на концептах, связанных отношением принадлежности-(категоризации). Напомним, что концепт является логической комбинацией ранее определенных концептов и ролей. В ряде источников, например [32, 35],, приводится сопоставление логики первого порядка и дескриптивной логики (ДЛ). Известно, что выражения ДЛ могут быть приведены к высказываниям ЛПП, если они не вовлекают в предикаты более двух переменных.
