WWW.DISUS.RU

БЕСПЛАТНАЯ НАУЧНАЯ ЭЛЕКТРОННАЯ БИБЛИОТЕКА

 

Pages:     || 2 | 3 |
-- [ Страница 1 ] --

ТОМСКИЙ ПОЛИТЕХНИЧЕСКИЙ УНИВЕРСИТЕТ

На правах рукописи

Пинжин Алексей Евгеньевич

АЛГОРИТМЫ ИНТЕЛЛЕКТУАЛЬНОЙ ОБРАБОТКИ ИНФОРМАЦИИ И СТРУКТУРНОГО СИНТЕЗА ПРОГРАММ

Специальность 05.13.01 - Системный анализ, управление и обработка информации (в отраслях информатики, вычислительной техники и автоматизации)

Диссертация

на соискание ученой степени

кандидата технических наук

Научный руководитель:

доктор физико-математических наук, профессор

Новосельцев Виталий Борисович

Томск – 2009

СОДЕРЖАНИЕ

Введение 3

1. ФОРМАЛЬНАЯ ТЕОРИЯ 12

1.1. Основные определения 12

1.2. Нерекурсивные и рекурсивные детерминированные С-модели 15

1.3. Постановка задачи 18

Выводы к главе 1 18

2. АЛГОРИТМЫ ПЛАНИРОВАНИЯ И СИНТЕЗА ПРОГРАММ 20

2.1. Проблема эффективности и общие принципы построения машины вывода для устойчивых баз знаний 20

2.2. Планирование и синтез в классе НДС-моделей 23

2.2.1. Правила вывода 23

2.2.2 Трансформация вариантной части 24

2.2.3. Компиляция НДС-модели 25

2.2.4. Постановка задачи и алгоритм вывода 30

2.2.5. Извлечение программы из доказательства 37

2.3. Планирование и синтез в классе РДС-моделей 40

2.3.1. Формальная модель доказательства 40

2.3.2. Подготовка данных и алгоритм вывода на РДС-модели 43

2.4. Программная реализация 49

Выводы к главе 2 59

3. ОЦЕНКА ЭФФЕКТИВНОСТИ 60

3.1. Расчет вычислительных затрат на осуществление вывода в классе С-моделей 60

3.2. Получение вида зависимости вычислительных затрат от объема спецификации РДС-модели 63

3.3. Экспериментальные результаты 64

Выводы к главе 3 66

4. ИНТЕРПРЕТАЦИЯ С-МОДЕЛИ ДЛЯ РЯДА ЛОГИЧЕСКИХ ИСЧИСЛЕНИЙ 67

4.1. Трансформация спецификаций языка Пролог в конструкции теории С-моделей 68

4.2. Упрощенный метод интерпретации для ряда логических исчислений 73

4.3. Реализация методов преобразования и экспериментальные результаты 76

Выводы к главе 4 80

Заключение 82

СПИСОК ЛИТЕРАТУРНЫХ ИСТОЧНИКОВ 84

СПИСОК СОКРАЩЕНИЙ 90

ПРИЛОЖЕНИЯ 91

Приложение 1. Полная модель данных компиляции и доказательства 91

Приложение 2. XML-схема описания С-модели 92

Приложение 3. Исходный код алгоритма планирования 94

Приложение 4. Исходный код процедуры очистки результатов вывода 101

Приложение 5. Пример исходной спецификации РДС-модели для проведения тестов 103

Приложение 6. Пример спецификации в формате CNF 106

Приложение 7. Пример спецификации в формате TME 107

Приложение 8. Пример спецификации в формате TPTP-FOF 108

Приложение 9. Пример спецификации для дескриптивной логики на языке OWL 109


Введение

В современном мире информационных технологий наблюдается постоянный рост интереса к методам интеллектуальной обработки данных. Эти тенденции определяются, с одной стороны, растущими объемами хранимой информации и интеграцией хранилищ данных, а с другой – постоянным ростом спроса на информационные услуги, связанные с обработкой этих данных. Указанные факторы проявляются как на уровне корпоративных информационных систем в области медицины, экономики, прогнозирования и т.д., так и на глобальном уровне, где одним из следствий возросших потребностей в интеллектуальной обработке данных стало возникновение парадигмы Semantic Web. Основой многих систем интеллектуального поиска и обработки информации являются машины логического вывода, реализующие те или иные методы доказательства логических теорем. Одной из основных проблем построения эффективных машин вывода является скорость вычислений, которая обычно определяется как количество вычислительных операций, требуемых для обработки базы знаний заданного объема. Следует отметить, что скорость вычислений также зависит от степени выразительности языка описания предметной области. Так, существуют современные реализации машин вывода для логики высказываний (построенные, например, на базе табличного (tableaux) метода) которые позволяют добиться линейных вычислительных затрат на осуществление вывода относительно объема базы знаний [32]. Однако вывод на сложных моделях, описанных на языке логики предикатов или дескриптивной логики зачастую приводит к полиномиальному или даже экспоненциальному росту вычислительных затрат в зависимости от объема исходной спецификации.

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



Область исследования диссертационной работы ограничена дедуктивным подходом, где программа извлекается из доказательства соответствующей теоремы. Появление первых работ в области автоматического синтеза программ на основе дедуктивного подхода приходится на 60-е гг. прошлого столетия. В работах Р. Уолдингера, Ц. Ченя, Р. Ли, З. Манны [42–44, 58] при доказательстве теоремы использовался метод резолюций Робинсона и различные его вариации, направленные на повышение вычислительной эффективности [26, 30]. Важный теоретический и практический вклад в развитие данного направления внесли работы отечественных исследователей. Н.Н. Непейвода предложил формальную теорию, устанавливающую соответствие между предложениями доказательства теорем и терминами структурного программирования [11–13]. Э.Х. Тыугу в 70-х гг. прошлого столетия предложил аппарат вычислительных моделей, использование которого для синтеза ветвящихся программ и программ с подпрограммами обосновано в публикациях [9, 10, 29]. В работах
А.Я. Диковского на основе теории вычислительных моделей исследуются возможности синтеза программ с рекурсией [1, 2].

Традиционным методом дедуктивного доказательства логической теоремы является движение от целей к посылкам, что позволяет избежать лишних построений. Известно, что этот метод приводит к издержкам, связанным с необходимостью возврата (так называемого «бэктрекинга», согласно спецификации языка Пролог [27, 40, 41]) при установлении недостижимости очередной подцели. Подходы, где вывод осуществляется в обратном направлении, от аксиом к целям, менее распространен, т.к. без применения специальных приемов приводит к значительному росту пространства вывода и издержек на хранение элементов исходной спецификации. Идея метода поиска доказательства от аксиом впервые была высказана Г. Генценым [38] и впоследствии получила развитие в работах С.Ю. Маслова и Г.Е. Минца [6–8], где приобрела название «обратного метода».

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

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

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

Для достижения указанной цели в работе решаются следующие задачи:

  1. Формальное определение элементов модели исходных данных и формулировка задачи логического вывода и синтеза программ на базе теории структурных функциональных моделей.
  2. Определение общих принципов, требований и архитектуры машины вывода.
  3. Формулировка правил вывода и разработка структур данных компиляции исходной спецификации с целью снижения вычислительных затрат при выполнении задачи планирования.
  4. Разработка алгоритмов планирования и синтеза программ.
  5. Расчет вычислительных затрат и экспериментальная оценка скорости разработанного алгоритма с использованием тестовых выборок данных.
  6. Сопоставление выразительных возможностей и определение правил трансформации элементов спецификации языка Пролог и конструкций теории структурных функциональных моделей.
  7. Адаптация разработанной машины вывода для решения задач, выраженных на языках ряда логических исчислений: логики высказываний, логики первого порядка, дескриптивной логики.
  8. Экспериментальное сравнение производительности разработанной машины вывода на перечисленных логических языках с существующими аналогами.

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

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

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

Научная новизна работы заключается в следующем:

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

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

… (Внедрение!?)

Основные положения, выносимые на защиту:

  1. Разработанный алгоритм вывода и синтеза программ, использующий метод динамической развертки и стратегию предварительной подготовки исходных данных, обладает высокими показателями производительности, которые характеризуются следующими соотношениями количества операций, затрачиваемых на осуществление вывода относительно объема исходной базы знаний:

а) линейная зависимость для программ с условиями и подпрограммами;

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

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

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

Апробация работы.

Основные результаты работы были представлены в виде:

3-х статей в журнале «Известия ТПУ» Томский политехнический университет, г.Томск,

а также докладов и статей на следующих конференциях:

«IX Всероссийская конференция молодых ученых по математическому моделированию и информационным технологиям (YM-2008)» (г. Кемерово, 28-30 октября 2008 г.);

Международная конференция «Программные системы: теория и приложения (PSTA-2009)» (г. Переславль-Залесский, ИПС РАН, 13-15 мая 2009 г.);

Международная конференция «Теоретические и прикладные вопросы современных информационных технологий (ТиПВСИТ’2009)»
(г. Улан-Удэ, 20-26 июля 2009 г.)

Всего по теме диссертации опубликовано 6 работ, из них 3 статьи в журнале, входящем в перечень ВАК, 2 статьи опубликованные по материалам конференций и 1 работа, опубликованная в качестве тезисов доклада на конференции.

Личный вклад:

  1. Формальное описание модели данных и постановки задачи построены на основе теории структурных функциональных моделей, предложенной проф. В.Б. Новосельцевым.
  2. Алгоритмы планирования и синтеза линейных программ, программ с ветвлениями, подпрограммами и рекурсией, а также оригинальный алгоритм динамической развертки разработаны автором и являются развитием идей, предложенных проф. В.Б. Новосельцевым.
  3. Формальное обоснование применения разработанной машины вывода для решения задач, сформулированных на языках логики высказываний, первого порядка и дескриптивной логики предложено лично автором.
  4. Реализация машины вывода и экспериментальное сравнение производительности выполнены лично автором.

Объём и структура работы. Диссертация состоит из введения, четырёх глав, заключения, списка источников из 58 наименований и 13 приложений. Содержит 9 рисунков и 1 таблицу.

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

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

В третьей главе дается теоретическая и экспериментальная оценка эффективности разработанного алгоритма планирования.

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

1. ФОРМАЛЬНАЯ ТЕОРИЯ

В главе предлагается формальная модель описания предметной области и постановки задачи планирования и синтеза. В качестве базового математического аппарата используется теория структурных функциональных моделей (С-моделей), предложенная В. Б. Новосельцевым [16], которая в свою очередь опирается на достаточно распространенные вычислительные модели, введенные Э. Х. Тыугу [29] и А. Я. Диковским [1]. Теория структурных функциональных моделей обладает необходимой и достаточной мощностью для создания строгих и в то же время выразительных моделей исходных данных, естественным образом проецируется на термины и конструкции структурного программирования [13] и весьма эффективна при описании методов планирования и синтеза.

    1. Основные определения

Определение 1.1. Описание модели предметной области, называемое сигнатурой, состоит из четырех множеств (A, F, P, D) и представляет собой множество атрибутов, функциональных связей, селекторов (предикатов) и схем отношений соответственно. Считается также, что выделено некоторое непустое подмножество первичных или примитивных схем ED.

Атрибуты, составляющие множество А, фиксируют некоторые характеристики объекта предметной области. Каждый атрибут связан со схемой из множества D. Если ТD\Е, то связь атрибута а со схемой Т выражается записью а:Т и атрибут называется непервичным. В противном случае, если ТЕ, то атрибут является примитивным (например, целое число, строка) и запись а:Т может быть заменена просто на а, если ссылка на схему не имеет значения.

Определение 1.2. Выражение вида:

f: a1,…, an a0, (1.1)

где ai, i = 0…n – имена атрибутов, называется функциональной связью (ФС). В записи (1.1) f – имя ФС, ai – аргументы (i = 1…n), a0 – результат ФС.

Неформально функциональная связь трактуется как возможность вычисления атрибута a0 по значениям атрибутов a1,…, an с помощью отображения f.





При описании модели предметной области на языке структурных функциональных моделей важнейшим является понятие схемы.

Определение 1.3. Схема T атрибута t определяется выражением вида:

t:T=(a0:S00, a1:S01, …, an:S0n

if p1(…) a10:S10, a11:S11…| f_set1 (1.2)

...

pk(…) ak0:Sk0, ak1:Sk1… | f_setk endif

| f_set),

где tA – имя атрибута схемы, TD\Е обозначает имя схемы. Для всех возможных значений индексов i, j символы SijD обозначают собственные подсхемы, aijA – собственные атрибуты схемы T.

Обозначение f_set в заключительной части определения схемы скрывает список собственных ФС схемы T.

Часть выражения (1.2) находящаяся между обозначениями if…endif является опциональной и определяет вариантную или условную часть схемы. Вариантная часть состоит из условных ветвей, разделенных символом, которые соответствуют традиционной программной конструкции if…elseif…else или ветвям оператора case. В условных ветвях символы piP, i=1...k называются выбирающими селекторами и представляют собой логическую функцию вида pi(аn0,…), где аn0,… – набор атрибутов заголовка схемы T. Следом за описанием селектора pi указываются условные атрибуты ai0:Si0, ai1:Si1… Выражение f_seti, следующее за описанием условных атрибутов, скрывает множество условных ФС. Условная ФС может включать в качестве аргументов и результатов атрибуты заголовка схемы и условные атрибуты своей ветви условия. Условие pi определяет допустимость условных атрибутов и ФС, входящих в i ветвь схемы. Иными словами, условные атрибуты и ФС имеют смысл только в соответствующей им ветви вариантной части схемы.

Далее, определим, какие имена атрибутов порождаются в описании схемы.

Определение 1.4. Пусть t – имя непервичного атрибута, связанного со схемой Т, т.е. t:T. Пусть a0,…,an – имена собственных атрибутов, определенных в схеме Т. Тогда, t.a0, …, t.an – также являются именами атрибутов. Набор атрибутов a0,…,an, будем называть суб-атрибутами по отношению к атрибуту t.

Теперь определим некоторые правила, ограничивающие ФС, входящие в множества f_set описания схемы.

Определение 1.5. Функциональная связь f: a1,…,ana0, входящая в описание схемы Т, является допустимой если a0,…,an – примитивные атрибуты схемы Т, либо примитивные суб-атрибуты непервичного атрибута, принадлежащего схеме Т. Схема называется синтаксически замкнутой, если f_set содержит только допустимые ФС. Предметом исследования в настоящей работе являются только синтаксически замкнутые схемы.

Кроме этого ФС, входящие в определение схемы, должны отвечать следующим требованиям:

  • ФС содержит по крайней мере один собственный атрибут схемы;
  • в наборе f_set нет ФС, в которые вовлечены атрибуты из разных вариантных ветвей схемы или атрибуты из вариантных частей ее подсхемы;
  • длина любого атрибута, связанного ФС, не превышает двух.

Для пояснения введенных обозначений приведем пример модели, описывающей простейшую систему уравнений:

, где n = x2.

Основная схема:

T = (x, y

if p1(x) | f11: xy... p2(x) r:R | f21: xr.m; f22: r.n, xy endif )

Схема для вычисления квадрата числа:

R = (m, n | fsq: m n).

    1. Нерекурсивные и рекурсивные детерминированные С-модели

Определим понятие структурной функциональной модели.

Определение 1.6. Конечная совокупность схем М=(T1,…,Ts) называется структурной (С-) функциональной моделью. Каждая схема Ti, i=1…s должна являться примитивной или удовлетворять определению 1.3.

Определение 1.7. С-модель М=(T1,…,Ts) является синтаксически замкнутой, если подсхемы, встречающиеся в определении каждой схемы TiM, являются элементарными либо входят в состав модели M.

Далее, введем понятие детерминированной схемы.

Определение 1.8. Схема является детерминированной, если она не содержит вариантной части либо ее вариантная часть содержит две взаимоисключающие условные ветви и определяется записью

if p(…) a00:S00, a01:S01…| f_set0 ; a10:S10, a11:S11… | f_set1 endif

Данное определение означает, что a00:S00, a01:S01…| f_set0 имеют смысл при истинности p, а a10:S10, a11:S11… | f_set1 – в обратном случае. Наличие у некоторого атрибута a условия p может быть выражено записью a/p, а обратное условие (соответствующее else в двухальтернативной вариантной части) обозначается a/~p.

Определение 1.9. С-модель М=(T1,…,Ts) является нерекурсивной детерминированной (НД-) С-моделью, если она удовлетворяет следующим условиям:

  • модель М является синтаксически замкнутой (см. Определение 1.7);
  • схемы T1,…,Ts являются детерминированными;
  • любая схема Ti модели М определяется через элементарные атрибуты либо через схемы, предшествующие Ti в модели М.

Введение рекурсивных выражений порождает в описаниях схем конструкции следующего вида: T1 = (…, t2:T2, …), T2 = (…, t3:T3, …), …, Tk = (…, t1:T1, …), где T1, T2, T3, …, Tk – схемы С-модели.

Определение 1.10. Будем называть рекурсию явной, если для рекурсивного вхождения T1 = (…, t2:T2, …), …, Tk = (…, t1:T1, …), значение k=1, т.е. T1 = (…, t1:T1, …), и неявной или опосредованной, если k>1. Соответственно, вхождение атрибута t1:T1 в схему Tk при k=1, будем называть явным, а при k>1 неявным или опосредованным вхождением рекурсивной подсхемы.

Определение 1.11. С-модель М=(T1,…,Ts) является рекурсивной детерминированной (РД-) С-моделью, если она удовлетворяет следующим ограничениям:

  • модель М является синтаксически замкнутой (см. Определение 1.7);
  • схемы T1,…,Ts являются детерминированными;
  • для каждой TiM явные или опосредованные вхождения подсхем вида t:Ti, могут появляться только в одной из двух альтернативных ветвей схемы Ti.

Отметим, что введенное здесь определение РДС-модели идентично по смыслу с определением, приведенным в [16, 17], однако избегает использования понятия полной развертки схемы.

В рамках работы рассматриваются только НДС- и РДС-модели. Далее, при использовании понятия С-модели без указания наличия рекурсивных вхождений будем подразумевать модель, удовлетворяющую определению НДС-модели.

В качестве примера рассмотрим описание РДС-модели для задачи «член ряда» Понятие «член ряда» (series element) определяет n-й член натурального ряда, либо ряда Фибоначчи в зависимости от равенства s значению “natural” или “fibonacci” соответственно. ФС fA означает операцию присваивания. Предикат equals проверяет равенство двух значений.

SERIES = ( s : STRING, x : INTEGER, n : INTEGER,

if equals(s, “natural”) xn : INTEGER | fA: n xn, fA: xn x

equals(s, “fibonacci”) xf : FIBONACCI_NUMBER|

fA: n xf.n, fA: xf.a x endif ).

Для натурального ряда, значение n-го члена совпадает с его номером n – это отражено ФС первой ветви условия. Число Фибоначчи вычисляется при помощи неэлементарной рекурсивной схемы FIBONACCI, содержащей рекурсивный вызов собственной схемы. В схеме FIBONACCI ФС fsubstract реализует операцию вычитания, а fsum – сложения. Предикат equals_in определяет равенство первого значения одному из двух последующих, предикат greater определяет больше ли значение первой переменной значения второй переменной.

FIBONACCI = ( n : INTEGER, a : INTEGER,

if equals_in(n, ‘0’, ‘1’) fa: INTEGER | fA: ‘1’ fa, fA: fa a

greater(n, ‘1’) p: FIBONACCI,

pp : FIBONACCI |

fsubstract : n, ‘1’ p.n,

fsubstract: n, ‘2’ pp.n,

fsum : p.a, pp.a a endif ).

Третья ветвь содержит основные вычисления – до тех пор пока n>1 рекурсивно производится суммирование двух чисел натурального ряда предшествующих текущему. Первые две ветви условия обеспечивают выход из рекурсии по достижении n=0,1.

    1. Постановка задачи

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

Определение 1.12. Задачей планирования на С-модели M называется тройка S=(A0,X0,T), где A0 и X0 – наборы имён соответственно исходных и искомых атрибутов, а TM – схема, в которой определены эти имена.

Для приведенной в предыдущем разделе РДС-модели «член ряда» может быть сформулирована следующая постановка задачи:

Модель «член ряда» = (SERIES, FIBONACCI)

Постановка задачи S = ({s, n}, {x}, SERIES)

Выводы к главе 1

Теория структурных функциональных моделей является достаточно мощным инструментом описания предметной области и постановки задачи планирования и синтеза программ. Представленные классы НДС- и РДС- моделей обладают следующими важными характеристиками:

1. Представляют необходимый и достаточный набор условий и ограничений для обеспечения разрешимости вывода.

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

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

2. АЛГОРИТМЫ ПЛАНИРОВАНИЯ И СИНТЕЗА ПРОГРАММ

    1. Проблема эффективности и общие принципы построения машины вывода для устойчивых баз знаний

В [17] показано, что полная развертка НДС-модели соответствует некоторой детерминированной (Д-) модели Диковского [1]. При этом,
А. Я. Диковским доказано, что при решении задачи синтеза на Д-моделях без использования внешней памяти, задача является NP-полной. Класс РДС-моделей включает в себя класс НДС-моделей. В [17] показано, что на развертке РДС-модели теоретически возможно построение алгоритмов вывода и синтеза, которые решают задачу за полиномиальное время, а также определен принцип динамической развертки, позволяющий значительно сократить издержки. В связи с этим перспективной задачей представляется построение машины вывода, использующей внешнюю память, избегающей построения статической развертки на подсхемах и обладающей полиномиальными характеристиками отношения вычислительных затрат к объему исходной модели.

Основные модули программной реализации машины вывода представлены на рис. 2.1.

 1. Структура машины вывода на С-модели Кратко поясним основные-1

Рис. 2.1. Структура машины вывода на С-модели

Кратко поясним основные составляющие предлагаемой архитектуры машины вывода.

Чтение файла описания С-модели. Исходная С-модель поставляется в виде спецификации, описанной на языке XML. Отметим, что формат описания исходных данных не имеет принципиального значения, так как при чтении модели данные преобразуются к единому внутреннему представлению. Язык XML был выбран лишь потому, что он является универсальным и наиболее распространенным языком описания данных, а также по причине наличия готовых программных библиотек по его обработке. Внутреннее представление С-модели представляет собой результаты синтаксического анализа и разбора (парсинга) файла описания, представленные в виде простых программных структур.

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

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

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

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

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

2.2. Планирование и синтез в классе НДС-моделей

2.2.1. Правила вывода

В качестве основного метода планирования на С-моделях используется классическое правило вывода. Для данного выше определения ФС (Определение 1.2):

, (2.1)

т.е. при выявлении достижимости аргументов А, утверждается достижимость результата х функциональной связи f.

При планировании на схемах с подсхемами это правило вывода распространяется на доставляющие ФС подсхем и используется для реализации динамической развертки:

(2.2)

т.е. достижимость суб-атрибута непервичного атрибута определяет достижимость собственного атрибута подсхемы, соответствующей этому непервичному атрибуту.

Исходя из (2.1) при планировании в классе НДС-моделей на схеме с вариантной частью в условной ветви p действует правило:

(2.3)

Данное правило определяет условие допустимости p атрибута x при наличии условия допустимости p функциональной связи f, т.е. при достижимости условных аргументов А условной ФС f, утверждается достижимость результата ФС в соответствующей ветви условия.

Условие x/p&~p определяет достижимость атрибута при всех альтернативных ветвях и тождественно записи х без указания условий допустимости. Согласно этому, может быть сформулировано третье правило вывода:

(2.4)

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

2.2.2 Трансформация вариантной части

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

pnvirt = pn(аn0,…), (2.5)

где pnvirt – виртуальный атрибут; pn – селектор.

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

T = (a0:S0,…,an:S1, p1virt, p2virt

if p1virt a10,…| f11:ai,…, p1virt…... pkvirt ak0,…| fk1: aj,…, pkvirt…endif |

f_set, p1virt = p1(…), pkvirt = pk (…)).

2.2.3. Компиляция НДС-модели

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

Предлагаемая модель данных результатов компиляции приведена
в виде UML-диаграммы на рис. 2.2.

 2. Структуры данных компиляции НДС-модели Модель данных включает в-6

Рис. 2.2. Структуры данных компиляции НДС-модели

Модель данных включает в себя следующие элементы:

  • набор объектов типа Схема;
  • пара объектов ВетвьУсловия, если схема обладает вариантной частью. Каждый объект содержит указатель на соответствующий объект типа Условие, а также изначально пустой список шагов доказательства, принадлежащих этой ветви. Каждый объект Условие однозначно соответствует ветви условия и содержит имя условия и признак отрицания[1]. Разделение на два типа Условие и ВетвьУсловия выполнено исключительно из практических соображений для того, чтобы отделить исходную информацию об условной ветви от списка шагов доказательства в условной ветви.
  • список объектов типа ФункциональнаяСвязь. Содержит параметр счетчикАргументов, который перед началом планирования содержит число аргументов ФС и ссылку атрибутРезультат на целевой атрибут ФС. Если на ФС наложено некоторое условие (f/р), то при компиляции определяется ссылка на соответствующий объект типа Условие;
  • список объектов типа Атрибут, содержащий:
    • непервичные атрибуты вида «t:T», определяемые ссылкой сложныйТип;
    • суб-атрибуты непервичных атрибутов вида «t.a», которые являются доставляющими атрибутами вызовов подпрограмм (фактические параметры) и обладают ссылкой вызовПодпрограммыАргумент и рекурсивной ссылкой субАтрибут на соответствующий атрибут вызываемой подсхемы (формальный параметр);
    • элементарные атрибуты текущей схемы, которые могут обладать ссылкой фсАргумент на ФС, в которых они участвуют в качестве аргумента.
  • если на атрибут наложено некоторое условие (а/р), то при компиляции определяется ссылка исходноеУсловие на соответствующий объект типа Условие. Список условияДопустимости изначально также содержит это условие и пополняется в процессе вывода достигнутыми условиями допустимости;
  • по каждому атрибуту непервичного типа создается объект типа ВызовПодпрограммы. Для каждого вызова объявляется список аргументов и результатов. Аргументы вызова процедуры определяются в ходе выполнения доказательства, атрибуты-результаты – в процессе подготовки структур данных по суб-атрибутам подсхем, служащих аргументами ФС текущей схемы. В процессе доказательства могут быть достигнуты не все атрибуты-результаты, поэтому их список может быть сокращен.

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

Поясним некоторые наиболее важные элементы предлагаемой модели. Как видно из приведенной схемы, на этапе компиляции выполняется «инверсия» ассоциации «функциональная связь – аргументы». Чтобы выяснить преимущества предлагаемого метода, обратимся к правилам вывода (2.1 – 2.4). Применение этих правил на этапе планирования требует выявления ФС, в которых достижимый атрибут входит в качестве аргумента. Предлагаемый подход решает эту проблему за счет заблаговременной подготовки и записи информации об этих взаимосвязях. Вполне очевидно, что перечисление всех аргументов всех ФС по каждому атрибуту схемы приводит к нелинейному росту количества операций относительно количества атрибутов и ФС схемы (для общего случая, когда ФС максимально используют набор атрибутов). Напротив, инверсная связь позволяет реализовать поиск ФС за линейное количество операций относительно числа аргументов за счет прямого, безызбыточного обращения к ФС по ссылке фсАргумент.

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

Следующим важным элементом предлагаемого подхода является использование счетчика аргументов ФС. Вновь обратимся к правилам вывода (2.1 – 2.4). Так как достижимость целевого атрибута устанавливается за счет установления достижимости всех атрибутов-аргументов ФС, возникает необходимость учета уже достигнутых и еще не достигнутых аргументов. Так как аргументы ФС не оказывают какого-либо влияния друг на друга, то информация о конкретных достигнутых аргументах не является важной. Подход со счетчиками реализует простой и эффективный метод контроля, где обнаружение очередного достижимого аргумента не требует его хранения и сопоставления с аргументами, достигнутыми ранее, а приводит лишь к уменьшению счетчика. Соответственно сокращение счетчика до нуля означает выполнение соответствующего правила вывода.

Отметим также оригинальность подхода к представлению условных атрибутов и ФС. Выполнение правил (2.3, 2.4) требует во-первых, хранения исходной информации о вхождении атрибутов и ФС в ту или иную условную ветвь, во-вторых, возможность «переноса» условия допустимости на вновь достигнутые атрибуты и, в-третьих, возможность проверки достижимости атрибута при всех альтернативных ветвях за минимальное количество операций. Первое требование достигается путем реализации ассоциаций исходноеУсловие и условие объектов Атрибут и ФункциональнаяСвязь. Благодаря этим ассоциациям в совокупности с инверсным представлением связи атрибутРезультат, перенос условия допустимости на вновь достигнутый атрибут может быть выполнен за одну простую операцию копирования ссылки условие в список условияДопустимости достижимого атрибута. И, наконец, третье требование, соответствующее правилу вывода (2.4) обеспечивается при помощи метода являетсяДопустимым класса Атрибут, который возвращает результат проверки наличия прямого и обратного условия в списке условияДопустимости, т.е. выполняет простейшую булевскую операцию “исключающее или” (XOR) над двумя значениями.

2.2.4. Постановка задачи и алгоритм вывода

Для постановки задачи поиска доказательства необходимо создать атрибут непервичного типа на исходной схеме и объявить объект типа ВызовПодпрограммы, со ссылками на исходные и целевые атрибуты (списки атрибутыАргументы и аргументыРезультаты). Результатом вывода является список достижимых атрибутов из числа целевых. Сравнивая эти списки можно сделать вывод об успешном доказательстве теоремы. В результате планирования исходный вызов подпрограммы связывается с объектом типа Подпрограмма (рис. 2.3), содержащим шаги доказательства. Структура объекта ШагДоказательства рассматривается ниже.

 3. Модель данных подпрограммы Шаги доказательства формируются в-7

Рис. 2.3. Модель данных подпрограммы

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

  • Функциональная связь;
  • Вызов подпрограммы (в свою очередь ссылающийся на подпрограмму);
  • Вариантная часть (в виде пары ветвей условия).

Функциональные связи и вызовы подпрограмм являются программными термами, вычисляющие по строго определенному набору аргументов значения определенных целевых атрибутов. Будем называть такие программные термы предложениями вычислимости (ПВ).

Структуры данных для хранения шагов доказательства представлены на рис. 2.4. Отметим, что вполне применимое в представленной модели отношение наследования заменено на отношение композиции в целях увеличения производительности алгоритма.

 4. Модель данных результатов вывода Используя описанные выше-8

Рис. 2.4. Модель данных результатов вывода

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

 5. Алгоритм поиска доказательства В процессе вывода используется-9

Рис. 2.5. Алгоритм поиска доказательства

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

Важным этапом процесса доказательства является обработка условий (рис. 2.6) Если на ФС наложено условие, то шаг помещается как в список шагов доказательства текущей подпрограммы, так и в список шагов соответствующей ветви условия. Условие ФС добавляется в список условий допустимости достижимого атрибута (поле условияДопустимости объекта Атрибут). Затем с помощью метода являетсяДопустимым, проверяется, достижим ли атрибут при всех альтернативных частях условия, т. е. достижим при /p и /~p. Если получен утвердительный ответ, атрибут помещается в список достижимыеАтрибуты шага доказательства, содержащего вариантную часть. Этот специфичный шаг доказательства создается заблаговременно для каждой подпрограммы, содержащей вариантную часть, и добавляется в список шагов доказательства подпрограммы однократно при достижении первого безусловного атрибута – результата условных ФС.

 6. Алгоритм обработки условий Значение, полученное в результате-10

Рис. 2.6. Алгоритм обработки условий

Значение, полученное в результате вызова метода являетсяДопустимым достижимого атрибута, назначается свойству являетсяДопустимым шага доказательства. Если при обработке очередного аргумента ФС выясняется, что ФС является безусловной (т. е. допустимой), а шаг доказательства, в котором был получен атрибут-аргумент, не является допустимым, то уменьшение счетчика аргументов ФС не выполняется. Игнорируется также шаг доказательства, содержащий ссылку на вариантную часть, он используется в дальнейшем при синтезе программы.

В отношении подсхем при осуществлении вывода используется стратегия динамической развертки (рис. 2.7). В процессе вывода фиксируется текущая подпрограмма, перед началом планирования текущей объявляется процедура, на которой была поставлена задача. Выполняется вывод на ФС текущей подпрограммы – поиск всех достижимых атрибутов текущей схемы, без спуска во вложенные вызовы подпрограмм, которые помещаются во временный стек. Затем, при невозможности дальнейшего планирования, осуществляется вывод на очередной подпрограмме из стека, после чего продолжается вывод на текущей подпрограмме. Процесс поиска решения является рекурсивным – вывод всех возможных аргументов вызова внутренних подпрограмм в текущей подпрограмме, рекурсивный запуск планирования на очередной внутренней подпрограмме, получение списка достигнутых целей и продолжение работы во внешней подпрограмме.

 7. Алгоритм динамической развертки на подсхемах Каждый спуск в-11

Рис. 2.7. Алгоритм динамической развертки на подсхемах

Каждый спуск в подсхему приводит к созданию нового объекта типа Подпрограмма (изначально присутствуют только вызовы подпрограмм). При спуске и подъеме из подпрограммы с помощью рекурсивной ссылки субАтрибут осуществляется перевод фактических параметров в формальные.

Приведенное выше описание отражает общие принципы построения доказательства. Более подробно алгоритм вывода можно представить с помощью следующего псевдокода:

# используемые сокращения: ш/д – шаг доказательства

proc планирование (вызовПодпрограммы)

begin

Создать подпрограмму, связать с вызовом подпрограммы, зафиксировать ее как текущую

Объявить стек внутренних вызовов подпрограмм

Установить счетчик обработанных ш/д равным 0

Получить атрибуты-аргументы и атрибуты-результаты текущего вызова подпрограммы

Установить счетчик недостижимых целевых атрибутов равным кол-ву атрибутов-результатов

По каждому аргументу создать ш/д и поместить в список ш/д текущей подпрограммы

while (счетчик обработанных ш/д меньше кол-ва ш/д в текущей подпрограмме) begin

Получить очередной ш/д из списка

while (обработаны не все достижимые атрибуты ш/д) begin

Получить очередной достижимый атрибут из ш/д

if (достижимый атрибут входит в список целевых атрибутов and

ш/д является допустимым) then

Поместить атрибут в список достигнутых целей

Уменьшить счетчик недостижимых целевых атрибутов на 1

if (счетчик недостижимых целевых атрибутов равен 0) then

Теорема доказана, выход из программы

end_if

end_if

Получить список ФС, в которых достижимый атрибут является аргументом

while (обработаны не все ФС) begin

Получить очередную ФС

if (ФС является безусловной and ш/д не является допустимым) then

пропустить обработку ФС

end_if

Уменьшить счетчик аргументов ФС на 1

if (счетчик аргументов равен 0) then

Получить атрибут-результат ФС

Создать ш/д и поместить в список шагов текущей подпрограммы

if (ФС является условной) then

Получить соотв. ветвь условия и поместить в нее ш/д

Добавить условие допустимости в атрибут-результат

if (атрибут-результат достижим на всех ветвях условия) then

Установить свойство ш/д являетсяДопустимым в true

Добавить атрибут-результат в список достижимых

атрибутов вариантной части

Добавить в список ш/д текущей подпрограммы вариантную часть, если не была добавлена ранее

end_if

end_if

Увеличить счетчик необработанных ш/д на 1

end_if

end_while

if (достижимый атрибут является аргументом вызова подпрограммы) then

Добавить атрибут в аргументы вызова подпрограммы

Поместить вызов подпрограммы в стек

end_if

if (счетчик обработанных ш/д равен кол-ву ш/д текущей подпрограммы and

обработан не весь стек внутренних вызовов подпрограмм) then

Получить очередной внутренний вызов подпрограммы из стека

Рекурсивно запустить процедуру планирования на внутреннем вызове подпрограммы

Получить достижимые атрибуты-результаты вызова подпрограммы

Создать ш/д вызова внутренней подпрограммы и поместить его в список ш/д текущей подпрограммы

if (непервичный атрибут, соответствующий внутреннему вызову подпрограммы

является условным) then

Получить соотв. ветвь условия и поместить в нее ш/д

Добавить условие допустимости в атрибут-результат

while (обработаны не все атрибуты-результаты вызова подпрограммы) begin

получить очередной атрибут-результат

if (атрибут-результат достижим на всех ветвях условия) then

Установить свойство ш/д являетсяДопустимым в true

Добавить атрибут-результат в список достижимых

атрибутов вариантной части

Добавить в список ш/д текущей подпрограммы вариантную часть, если не была добавлена ранее

end_if

end_while

end_if

end_if

end_while

Увеличить счетчик обработанных ш/д на 1

end_while

Теорема не доказана, выход из программы

end_proc

2.2.5. Извлечение программы из доказательства

Синтез программы осуществляется на основе списка шагов доказательства, полученного в результате планирования. Процесс синтеза осуществляется в два этапа: очистка и сборка программы. Очистка включает в себя обработку списка шагов доказательства подпрограммы «снизу-вверх» и удаление элементов не участвующих в получении целей (рис 2.8). Кроме того, из списка шагов доказательства подпрограммы удаляются условные шаги доказательства, дублируемые в списке ветвей условия. Процесс очистки является рекурсивным в том смысле, что он выполняется для всех внутренних подпрограмм, встречаемых среди шагов доказательства текущей подпрограммы.

 8. Алгоритм очистки На вход процедуры очистки подается главная-12

Рис. 2.8. Алгоритм очистки

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

proc очистка (подпрограмма)

begin

Получить список аргументов

Получить список целей

Получить список шагов доказательства

while (обработаны не все шаги доказательства) begin

Получить очередной шаг, начиная с конца списка

while (обработаны не все достижимые атрибуты шага док-ва) begin

Получить очередной достижимый атрибут шага док-ва

if (достижимый атрибут содержится в списке целей) then

if (ш/д является условной ФС или условным вызовом подпрограммы) then

Удалить шаг доказательства

else_if (ш/д является вариантной частью) then

Удалить достижимый атрибут из списка целей

Запустить процедуру очистки вариантной части

Получить список входных атрибутов вариантной части

Добавить входные атрибуты вариантной части в список целей

else

Добавить аргументы доставляющего ш/д в список целей

Удалить достижимый атрибут из списка целей

if (доставляющим ш/д является вызов подпрограммы) then

Рекурсивно запустить процедуру очистки на вызываемой подпрограмме

end_if

end_if

end_if

end_while

end_while

end_proc

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

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

2.3. Планирование и синтез в классе РДС-моделей

Выделенный в п. 1.2 класс РДС-моделей (Определение 1.11) является подклассом Д-моделей, однако обладает важным свойством полиномиальной разрешимости. В [17] предложены базовые правила вывода и обозначены основные проблемы эффективности алгоритма доказательства на рекурсивных моделях. Среди этих проблем выделяются сложность обнаружения рекурсивного вызова и определения аргументов и результатов ПВ, являющегося вызовом рекурсивной процедуры. Для преодоления указанных сложностей были поставлены задачи разработки общей процедуры поиска доказательства, определения оптимальных с точки зрения производительности структур данных и реализации алгоритма доказательства. В настоящем разделе приводится формальная схема доказательства, дополнительные элементы структур данных компиляции и алгоритм вывода на РДС-моделях.

2.3.1. Формальная модель доказательства

Для наглядного описания предлагаемого алгоритма представим РДС-модель в виде схемы (рис. 2.9).

 9. Структура РДС-модели и последовательность этапов доказательства -13

Рис. 2.9. Структура РДС-модели и последовательность этапов доказательства

На представленной схеме прямоугольниками изображены схемы, входящие в РДС-модель, в левом верхнем углу каждой схемы отмечено ее имя и имя атрибута, порождающего явный или опосредованный потенциальный рекурсивный вызов. Эллипсами отображены исходные (А0) и целевые (Х0) атрибуты из постановки задачи на схеме. Жирными линиями отображается последовательность ФС схемы (f_set), дуга в левой части отображает f_set альтернативной ветви p, в правой – f_set ветви ~p. Из схемы видно, что в ветви ~p содержится ряд вызывающих друг друга промежуточных подсхем (T2…Tk-1) и, наконец, схема Tk, содержащая обращение t1:T1 к головной схеме Т1. Стрелками (1), (2), (3) обозначенная предлагаемая последовательность этапов обработки при осуществлении вывода. Рассмотрим эти этапы.

Первый этап включает в себя идентификацию рекурсии – определение является ли вхождение подсхемы рекурсивным, а также построение транзитивного замыкания – определение множества аргументов рекурсивной процедуры. Предположим, что наличие в Т1 явного или неявного вхождения подсхемы Tk уже установлена и известна последовательность (T1, T2…Tk–1, Tk). Будем называть вызов головной подпрограммы Т1 внешним вызовом, а вызов подпрограммы, соответствующий вхождению t1:T1 внутренним вызовом. Для обнаружения потенциально рекурсивного вхождения t1:T1 для каждой подсхемы строится цепочка вызовов внешних схем и осуществялется восходящее перечисление этих схем для обнаружения вхождений, идентичных текущей схеме. Более подробное описание этого алгоритма приведено в п.2.3.2, посвященном реализации алгоритма. При первом достижении потенциально рекурсивной подсхемы Tk определяется множество достижимых атрибутов t1.A0' поступающих на вход вызова t1:T1. Если t1.A0 t1.A0', то подсхема идентифицируется как рекурсивная и выполняется переход ко второму шагу. Иначе, если t1.A0 t1.A0' =, то вызов не является рекурсивным – вывод на Tk осуществляется в обычном режиме (хотя не исключено обнаружение рекурсии при дальнейшем выводе на t1.A0'). Самая сложная ситуация возникает, когда зафиксировано сужение множества аргументов, т. е. t1.A0 t1.A0', t1.A0 t1.A0'. В этом случае выполняется присвоение t1.A0 = t1.A0' и осуществляется повторный вывод по ветви ~p схемы Т1 с целью получения нового множества t1.A0' (этап (1) на рис. 2.5). Эта операция выполняется итеративно до тех пор, пока не будет выполнено одно из условий: t1.A0 t1.A0' =, или t1.A0 t1.A0'. В первом случае делается заключение о том, что обращение к подсхеме не является рекурсивным, во втором – фиксирует обнаружение рекурсивного вызова и выполняется переход на следующий этап.

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

Второй и третий этапы вывода осуществляются, если подсхема идентифицирована как рекурсивная. Вывод на рекурсивной подсхеме основан на принципе структурной индукции – устанавливается выводимость (t:T1, A0, X0/p) (база индукции), затем, исходя из предположения, что (tk:Tk, t1.A0', t1.X0') доказуемо (гипотеза индукции), выполняется доказательство теоремы (t1:T1, t1.X0', X0/~p). Предлагаемый подход позволяет синтезировать программы, в которых предусмотрен выход из рекурсии по одной из ветвей условия на синтаксическом уровне и, следовательно, завершаемость таких программ зависит от задания интерпретации РДС-модели.

2.3.2. Подготовка данных и алгоритм вывода на РДС-модели

Подготовка (компиляция) схем РДС-модели не требует каких-либо дополнительных действий в связи с введением рекурсивных конструкций. Выявление и обработка рекурсивных вхождений выполняется на стадии вывода. Для этих целей в структуры данных добавляются следующие элементы (рис. 2.10):

  • ссылка внешнийВызовПодпрограммы – указывает на вызов подпрограммы, который инициирует данный вызов. Благодаря этому свойству становится возможным идентификация потенциально рекурсивных вызовов. Для вызова подпрограммы, на котором поставлена задача вывода, эта ссылка не определена;
  • свойство логического типа содержитРекурсивныйВызов объекта Условие служит для выделения рекурсивной ветви вариантной части.

 10. Модификация модели исходных данных Полная схема структур данных-14

Рис. 2.10. Модификация модели исходных данных

Полная схема структур данных компиляции и доказательства приведена в Приложении 1.

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

, 11. Алгоритм вывода на РДС-модели Фрагмент псевдокода,-15

Рис. 2.11. Алгоритм вывода на РДС-модели

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

...

if (счетчик обработанных ш/д равен кол-ву ш/д текущей подпрограммы and

обработан не весь стек внутренних вызовов подпрограмм) then

Получить очередной внутренний вызов подпрограммы из стека

Установить внешний вызов этой подпрограммы равным текущему

Зафиксировать внутренний вызов в качестве очередного

while (у очередного вызова подпрограммы существует внешний вызов) begin

Получить внешний вызов подпрограммы

if (имена схем текущего и внешнего вызова совпадают and

список аргументов текущего и внешнего вызова пересекаются) then

Зафиксировать обнаружение рекурсивного вызова

Зафиксировать найденный внешний вызов подпрограммы

end_if

Зафиксировать внешний вызов в качестве очередного

end_while

if (обнаружен рекурсивный вызов and сужение множества аргументов) then

Запустить процедуру построения замыкания

if (кол-во аргументов в результате построения замыкания равно 0) then

Отменить обнаружение рекурсивного вызова

end_if

end_if

if (обнаружен рекурсивный вызов) then

Связать внутренний вызов подпрограммы с подпрограммой,
соответствующей внешнему вызову

Скопировать множество достижимых атрибутов-целей внешнего вызова подпрограммы во внутренний вызов подпрограммы

else

Рекурсивно запустить процедуру планирования на внутреннем вызове подпрограммы

...

end_if

Получить достижимые атрибуты-результаты вызова подпрограммы

Создать ш/д вызова внутренней подпрограммы и поместить его в список ш/д текущей подпрограммы

...

end_if

...

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

proc построениеЗамыкания (внутреннийВызовПодпрограммы, внешнийВызовПодпрограммы)

begin

while (обнаружено сужение множества атрибутов and
список аргументов внутреннего вызова не пустой) begin

Заменить множество фактических и формальных параметров внешнего вызова параметрами
внутреннего вызова

Получить список шагов доказательства рекурсивной процедуры

Получить список исключенных атрибутов, т.е. аргументов внешнего вызова,
отсутствующих во внутреннем вызове

Удалить входные шаги доказательства, соответствующие исключенным атрибутам

Запустить процедуру очистки на внешнем вызове подпрограмме

end_while

Вернуть количество аргументов внутренней подпрограммы

end_proc

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

proc очистка (внешнийВызовПодпрограммы, внутреннийВызовПодпрограммы, исключенныеАтрибуты)

begin

while (обработаны не все ш/д внешней подпрограммы) begin

Получить очередной шаг доказательства

if (доставляющее ПВ является ФС and

(ФС является безусловной or условная ветвь ФС является рекурсивной) and

среди ФС, в которых недостижимые атрибуты участвуют в качестве аргументов,
содержится доставляющая ФС текущего ш/д) then

Добавить результат ФС в список исключенных атрибутов

if (ФС доставляет результат вызова текущей подпрограммы) then

Добавить соответствующий фактический параметр–результат вызова подпрограммы в список недостижимых атрибутов

end_if

if (результат ФС является аргументом вызова промежуточной подпрограммы) then

Добавить соответствующий формальный параметр – аргумент подпрограммы
в список недостижимых атрибутов

end_if

if (ФС является доставляющей в рекурсивную процедуру) then

Удалить результат ФС из числа аргументов рекурсивного вызова

end_if

else_if (доставляющее ПВ является вызовом подпрограммы and

(вызов подпрограммы является безусловным or условная ветвь вызова
подпрограммы является рекурсивной) and

среди вызовов подпрограммы, в которых недостижимые атрибуты участвуют в качестве аргумента содержится доставляющий вызов подпрограммы текущего ш/д) then

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

end_if

end_while

end_proc

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

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

2.4. Программная реализация

Предложенные в главе алгоритмы вывода на НДС- и РДС-моделях были реализованы с использованием языка Java SE 6 [54].

Приложение принимает на вход описание С-модели в виде RDF/XML-файла. Такой формат представления исходных данных был выбран по причине универсальности и распространенности, а также наличия множества доступных программных библиотек для его обработки. Структура и формат данных описания определяется XML-cхемой, представленной в Приложении 2. Ниже приведен листинг XML-файла исходных данных РДС-модели «член ряда», приведенной в первой главе работы (п. 1.2):

<!-- FILENAME: source-files/frsSeries1.xml -->

<?xml version="1.0"?>

<rdf:RDF xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"

xmlns:ex="http://example.org/terms#"

xml:base="http://example.org">

<ex:Scheme name="SERIES">

<ex:TitleAtribute name="s"/>

<ex:TitleAtribute name="n"/>

<ex:TitleAtribute name="x"/>

<ex:Condition name="equals_natural" negation="false" condIndex="0">

<ex:PredicateAtribute name="s"/>

<ex:CondAtribute name="xn"/>

<ex:CondFunctionalRelation name="fa_n_xn">

<ex:InputAtribute name="n"/>

<ex:OutputAtribute name="xn"/>

</ex:CondFunctionalRelation>

<ex:CondFunctionalRelation name="fa_xn_x">

<ex:InputAtribute name="xn"/>

<ex:OutputAtribute name="x"/>

</ex:CondFunctionalRelation>

</ex:Condition>

<ex:Condition name="equals_natural" negation="true" condIndex="1">

<ex:PredicateAtribute name="s"/>

<ex:CondAtribute name="xf" type="FIBONACCI"/>

<ex:CondFunctionalRelation name="fa_n_xfn">

<ex:InputAtribute name="n"/>

<ex:OutputAtribute name="xf.n"/>

</ex:CondFunctionalRelation>

<ex:CondFunctionalRelation name="fa_xfa_x">

<ex:InputAtribute name="xf.a"/>

<ex:OutputAtribute name="x"/>

</ex:CondFunctionalRelation>

</ex:Condition>

</ex:Scheme>

<ex:Scheme name="FIBONACCI">

<ex:TitleAtribute name="n"/>

<ex:TitleAtribute name="a"/>

<ex:Condition name="equalsin" negation="false" condIndex="0">

<ex:PredicateAtribute name="n"/>

<ex:CondAtribute name="fa"/>

<ex:CondFunctionalRelation name="fa_1_fa">

<ex:OutputAtribute name="fa"/>

</ex:CondFunctionalRelation>

<ex:CondFunctionalRelation name="fa_fa_a">

<ex:InputAtribute name="fa"/>

<ex:OutputAtribute name="a"/>

</ex:CondFunctionalRelation>

</ex:Condition>

<ex:Condition name="equalsin" negation="true" condIndex="1">

<ex:PredicateAtribute name="n"/>

<ex:CondAtribute name="p" type="FIBONACCI"/>

<ex:CondAtribute name="pp" type="FIBONACCI"/>

<ex:CondFunctionalRelation name="fsub_n_1">

<ex:InputAtribute name="n"/>

<ex:OutputAtribute name="p.n"/>

</ex:CondFunctionalRelation>

<ex:CondFunctionalRelation name="fsub_n_2">

<ex:InputAtribute name="n"/>

<ex:OutputAtribute name="pp.n"/>

</ex:CondFunctionalRelation>

<ex:CondFunctionalRelation name="fsum_pa_ppa_a">

<ex:InputAtribute name="p.a"/>

<ex:InputAtribute name="pp.a"/>

<ex:OutputAtribute name="a"/>

</ex:CondFunctionalRelation>

</ex:Condition>

</ex:Scheme>

</rdf:RDF>

Загрузка файла данных выполняется с помощью класса анализатора XMLHandler (рис 2.12).

 12. Загрузчик файла исходных данных Основной метод загрузки имеет-16

Рис. 2.12. Загрузчик файла исходных данных

Основной метод загрузки имеет следующую сигнатуру:

/**

* Загрузка данных С-модели из файла

* @param inputFileName файл с описанием С-модели

* @return набор схем в виде множества пар <имя_схемы, схема>

*/

public HashMap<String, Scheme> loadSchemeDataFromXML(String inputFileName) {

...

}

}

Анализатор выполняет чтение исходного файла и возвращает описание элементов модели в виде объектов следующих классов (рис. 2.13).

 13. Классы для внутреннего представления исходных данных Загруженные-17

Рис. 2.13. Классы для внутреннего представления исходных данных

Загруженные данные передаются в компилятор, реализованный в виде класса CompilerForReasoning (рис. 2.14):

 14. Класс-компилятор Класс-компилятор содержит два метода: public>-18

Рис. 2.14. Класс-компилятор

Класс-компилятор содержит два метода:

public>

// коллекция для хранения результатов компиляции

private HashMap<String, PreparedScheme> preparedSchemes =

new HashMap<String, PreparedScheme>();

/**

* Возвращает подготовленные данные

* (для повторного использования ранее откомпилированных схем)

* @return множество откомпилированных схем модели

*/

public HashMap<String, PreparedScheme> getPreparedSchemes() {

return preparedSchemes;

}

/**

* Выполяет подготовку (компиляцию) схем

* @param schemes исходное описание модели

* @return множество откомпилированных схем модели

*/

public HashMap<String, PreparedScheme> prepareSchemes (

HashMap<String, Scheme> schemes) {

...

}

Результаты компиляции возвращаются в виде следующего набора объектов (рис. 2.15). Эти же структуры используются в процессе вывода для создания подпрограмм и хранения шагов доказательства.

 15. Классы для представления результатов компиляции и шагов-19

Рис. 2.15. Классы для представления результатов компиляции и шагов доказательства



Pages:     || 2 | 3 |
 





<
 
2013 www.disus.ru - «Бесплатная научная электронная библиотека»

Материалы этого сайта размещены для ознакомления, все права принадлежат их авторам.
Если Вы не согласны с тем, что Ваш материал размещён на этом сайте, пожалуйста, напишите нам, мы в течении 1-2 рабочих дней удалим его.