авторефераты диссертаций БЕСПЛАТНАЯ БИБЛИОТЕКА РОССИИ

КОНФЕРЕНЦИИ, КНИГИ, ПОСОБИЯ, НАУЧНЫЕ ИЗДАНИЯ

<< ГЛАВНАЯ
АГРОИНЖЕНЕРИЯ
АСТРОНОМИЯ
БЕЗОПАСНОСТЬ
БИОЛОГИЯ
ЗЕМЛЯ
ИНФОРМАТИКА
ИСКУССТВОВЕДЕНИЕ
ИСТОРИЯ
КУЛЬТУРОЛОГИЯ
МАШИНОСТРОЕНИЕ
МЕДИЦИНА
МЕТАЛЛУРГИЯ
МЕХАНИКА
ПЕДАГОГИКА
ПОЛИТИКА
ПРИБОРОСТРОЕНИЕ
ПРОДОВОЛЬСТВИЕ
ПСИХОЛОГИЯ
РАДИОТЕХНИКА
СЕЛЬСКОЕ ХОЗЯЙСТВО
СОЦИОЛОГИЯ
СТРОИТЕЛЬСТВО
ТЕХНИЧЕСКИЕ НАУКИ
ТРАНСПОРТ
ФАРМАЦЕВТИКА
ФИЗИКА
ФИЗИОЛОГИЯ
ФИЛОЛОГИЯ
ФИЛОСОФИЯ
ХИМИЯ
ЭКОНОМИКА
ЭЛЕКТРОТЕХНИКА
ЭНЕРГЕТИКА
ЮРИСПРУДЕНЦИЯ
ЯЗЫКОЗНАНИЕ
РАЗНОЕ
КОНТАКТЫ


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

Томский политехнический университет

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

НОВОСЕЛЬЦЕВ Виталий Борисович

ФОРМАЛЬНАЯ ТЕОРИЯ СТРУКТУРНЫХ

МОДЕЛЕЙ ОПИСАНИЯ

ИНФОРМАЦИОННЫХ СИСТЕМ И МЕТОДЫ УСТАНОВЛЕНИЯ

ВЫВОДИМОСТИ

Специальность 05.13.01 – Системный анализ, управление и

обработка информации (в отраслях информатики, вычислительной

техники и автоматизации)

Диссертация на соискание ученой степени доктора физико-математических наук

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

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

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

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

Реферат.................................................................................................................. Введение.................................................................................................................. Глава 1. Логические подходы к управлению знаниями................................... 1.1. Подход на базе классических и интуиционистских теорий................... 1.2. Модальные логики...................................................................................... 1.3. Дескриптивные логики.............................................................................. 1.4. Выводы........................................................................................................ Глава 2. Структурные функциональные модели.............................................. 2.1. Язык теории. Основные определения...................................................... 2.2. Нерекурсивные детерминированные С-модели.

..................................... 2.3. Рекурсивные детерминированные С-модели.......................................... 2.4. Интерпретация С-модели........................................................................... 2.5. Выводы........................................................................................................ Глава 3. Установление выводимости в РДС-модели....................................... 3.1. Формальное исчисление. Правила вывода.............................................. 3.1.1. Исчисление SR.................................................................................... 3.1.2. Корректность и полнота исчисления SR......................................... 3.2. Стратегия и алгоритм вывода в классе РДС............................................ 3.2.1. Описание алгоритма.......................................................................... 3.2.2. Корректность алгоритма построения вывода................................. 3.2.3. Особенности введения рекурсии...................................................... 3.3. Проблемы реализации систем построения вывода................................. 3.4. Выводы........................................................................................................ Глава 4. Модальная логика и обратный метод.................................................. 4.1. Базовые понятия и соглашения................................................................. 4.1.1. Синтаксис и семантика логики КТ................................................. 4.1.2. Мультимножества и секвенции...................................................... 4.1.3. Прямое и обратное исчисление секвенций для логики знания... 4.2. Исчисление путей для логики КТ........................................................... 4.2.1. Прямое исчисление путей............................................................... 4.2.2. Обратное исчисление путей............................................................ 4.3. Анализ избыточностей и полнота KTФ,*IP.............................................. 4.4. Выводы...................................................................................................... Глава 5. Ф-упорядочение.................................................................................. 5.1. Определения и соглашения..................................................................... 5.2. Полнота KTФIP без секвенций, относящихся к.................................. 5.3. Предпосылка как критерий избыточности............................................ 5.4. Выводы...................................................................................................... Заключение......................................................................................................... Список цитируемой литературы....................................................................... Введение Интенсивное проникновение компьютеров во все области человеческой деятельности естественным образом приводит к необходимости моделировать и анализировать все более сложные прикладные области. Если первоначально компьютеры предназначались, преимущественно, для решения строго алгоритмизируемых задач, ассоциированных с теми или иными вычислительными проблемами, то, с недавних пор, информационно вычислительные комплексы все чаще начинают служить «интеллектуальными помощниками». При этом нередко моделируемые области являются слабо формализованными, когда анализ конкретной задачи и поиск ее решения подразумевает присутствие «творческого начала» – способности программного комплекса так или иначе моделировать интеллектуальные возможности человека, чтобы решать возникающие задачи, использовать эвристики, обучаться, накапливать и применять накопленный опыт. Такая необходимость обусловлена, как правило, полным отсутствием либо недостаточной степенью формализованности предметной области.

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

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

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

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

обилие вовлеченных в модель базовых понятий;

тотальное взаимовлияние этих понятий, приводящее, как правило, к NP (P-SPACE) полноте соответствующих алгоритмов;

отсутствие единой (общей) теории для прикладной области, т.е.

существенная необъективность при формировании модели.

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

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

Одной из важнейших проблем современных компьютерных наук (computer science) является построение инструментальных средств, максимально сокращающих объем специальных навыков, необходимых при использовании информационно-вычислительных технологий. Отметим три наиболее значимых, на наш взгляд, области, для которых «интеллектуализация» является чрезвычайно важной. По степени вовлеченности пользователей на первое место, несомненно, следует поставить «Всемирную паутину» (World wide web или WWW) с ее гигантскими информационными ресурсами и сопутствующими проблемами менеджмента данных, с быстрорастущим количеством сетевых сервисов и недостатками механизмов реализации этих служб, с необходимостью управления сложной структурой Паутины и т.д.

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

Наконец, третья из приводимых здесь областей практической деятельности относится, главным образом, к науке или инженерии. Речь идет о (возможном) желании прикладного специалиста самостоятельно и за короткий срок создать необходимый ему программный продукт. – Здесь одним из наиболее перспективных подходов является разработка систем с возможностями автоматического синтеза программ.

Наиболее распространенными при построении программных комплексов управления и обработки знаний являются дедуктивные системы.

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

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

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

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

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

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

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

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

Научная новизна полученных результатов определяется следующими положениями:

построена формальная теория структурных рекурсивных импликативных моделей SR, для нее показаны свойства эффективной распознаваемости и эффективной разрешимости, а также приведены варианты прикладного использования;

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

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

сформулирован и обоснован подход к установлению выводимости формул для систем классов КТ и KT45 (S5) (модальных логик знания и автоэпистемической логики);

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

Практическая значимость. Все теоретические построения, приведенные в диссертационном исследовании, формально строго обоснованы и опираются на новейшие результаты в области автоматического доказательства теорем. Полученные результаты частично использовались в реальных разработках (см. [Новосельцев 1985в], [Новосельцев и Калайда 1986] и [Новосельцев, Калайда и Шагисултанов 1991]) и применяются в настоящее время в ряде аспирантских исследований, которые ведутся под руководством автора. Они также могут быть использованы для реализации и исследования экономических моделей с конкурентным взаимодействием субъектов, децентрализованных комплексов управления сложными прикладными структурами, распределенных информационных систем различного назначения.

Апробация работы. Результаты работы докладывались в профильных семинарах ВМиК МГУ, ММФ СПбГУ, ФПМиК и ММФ ТГУ, АВТФ ТПУ, а также на ряде научных форумов различного уровня, среди которых можно отметить следующие:

II Всероссийская конференция по прикладной логике – Новосибирск, ИМ СО РАН, 1988, IX Международная школа ПП-91 «Программное обеспечение управления и ИИ» – Иркутск, ИрВЦ СО РАН, 1991, Международная конференция «Параллельные вычисления – 91» – Киев, ИК АН Украины, 1991, Международная конференция «Логика и семантическое программирование» – Новосибирск, ИМ СО РАН, 1992, 5th International Symp. on Applied Logic – Tallinn, 1996, Международная конференция «Всесибирские чтения по математике и механике. Томск 1997» – Томск, ТГУ, 1997, 8th Korean-Russian International Symposium on Science and Technology – KORUS 2004, Томск, ТПУ, 8th WSEAS International Conference on APPLIED MATHEMATICS Puerto De La Cruz, Tenerife, Canary Islands, Spain, 2005, 9th Korean-Russian International Symposium on Science and Technology – KORUS 2005, Новосибирск, НГТУ.

Результаты, выносимые на защиту

:

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

Эффективные обратные стратегии и алгоритмы установления выводимости формулы в теории SR.

Формальный подход к установлению выводимости формул для модальных систем классов КТ и KT45 (S5) с использованием обратного метода.

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

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

общий объем составляет страниц, включая иллюстрации.

Глава 1. Логические подходы к управлению знаниями 1.

1.

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

Логика, как инструмент анализа абстрактных построений, связанных с моделированием «интеллектуальных» процессов, предлагает широкий набор теорий, обеспечивающих работу со знаниями. Понятие «знание» при этом трактуется, разумеется, не в общефилософском смысле, а значительно уже. – Как правило, элементарной когнитивной единицей выступает семантически нагруженная импликация или ее подобие, а собственно «знанием» становится комплекс таких единиц в сочетании с методами манипулирования (навигации, порождения и т.д.). – В частности, размеченные дуги в семантических сетях или фишки (переходы) в сетях Петри также могут быть промоделированы нагруженными импликациями. Зачастую, проблема построения выводов из некоторых исходных данных заключается в том, что анализ антецедента простой импликации типа «если P, то Q» связан с необходимостью учета контекста, в котором данное предложение имеет место, то есть с учетом пути, приведшего к посылке импликации.

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

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

Обеспеченность вывода здесь понимается следующим образом: применение правил построения заключений из ранее определенных фактов не зависит от текущего состояния системы либо определяется строго заданными метаправилами, а правил и метаправил – существенно ограниченное количество. – К теориям подобного сорта, в частности, можно отнести классическую механику, радиотехнику (без учета квантовых эффектов) и ряд иных хорошо формализованных предметных областей. Проблемы выводимости для таких ПО достаточно глубоко исследованы в ряде работ отечественных и зарубежных авторов, главным образом, в связи с решением задачи автоматического синтеза расчетных программ (см., например, [Минц и Тыугу 1982], [Минц 1981], [Непейвода 1978,1979] и др.).

Появление ранних систем, в которых из доказательства соответствующей теоремы извлекалась программа, удовлетворяющая некоторому отношению на вход/выход [Waldinger and Lee 1969], было результатом первых попыток синтеза последовательных программ. Такие системы начали появляться в 60-х годах прошлого столетия в области исследований искусственного интеллекта. При доказательстве теоремы существования решения в первых системах прямо применялась теорема Эрбрана [Чень и Ли 1983], на смену которой пришел принцип резолюций [Робинсон 1970] и/или его модификации, а также ряд специализированных методов.

В работах по автоматическому синтезу программ традиционно различают три подхода:

дедуктивный;

индуктивный;

трансформационный.

Работы [Constable 1972] и [Manna and Waldinger 1977] являются примерами дедуктивного подхода к автоматическому синтезу программ.

Входными данными задачи выступают конечные множества x и y входных и выходных величин, соответственно, и условия P(x) и Q(x,y). Задача синтеза трактуется следующим образом: по заданному значению x, удовлетворяющему условию P(x), вычислить значение y, удовлетворяющему условию Q(x,y). Считается, что спецификация R=(P(x),Q(x,y)) содержит достаточно информации для построения программы, которая реализует вычисление значений выходных величин по значениям входных. Задача однозначно представляется тройкой (x,y,R). Теорема существования решения x(P(x)yQ(x,y)).

задачи имеет вид: Построение интуиционистского доказательства теоремы существования решения обеспечивает получения требуемой программы. Из такой постановки исходят [Waldinger and Lee 1969], [Manna and Waldinger 1977] и в [Girard, Lafont and Taylor 1989].

Важные теоретические результаты, связанные с «корректным синтезом»

программ, приведены в работах [Непейвода 1978, 1979]. – В первой выделен класс интуиционистских теорий, для которых существует прямая связь между предложениями доказательств теорем в этих теориях и конструкциями языков программирования (Алгол-68, Лисп), а во второй предложен алгоритм извлечения программы из доказательства соответствующей теоремы. В [Лавров 7] отмечаются трудности, которые возникают при дедуктивном подходе к синтезу программ. Успех возможен в том случае, когда спецификация «достаточно хорошо» описывает условие задачи. Это означает, что автоматическое построение программ осуществимо для формализуемых предметных областей в тех случаях, когда разработка спецификации программы по тем или иным соображениям проще разработки самой программы либо экономически целесообразней.

В начале семидесятых годах прошлого столетия появился аппарат вычислительных моделей, предложенный в [Тыугу 1970]. Глубокое обоснование использования этого аппарата для синтеза ветвящихся программ и программ с параметрами-процедурами приводится в работах [Минц и Тыугу 1982, 1983]. Предложенное Г.Е.Минцем исчисление не выводит за рамки исчисления высказываний, что, в определенной степени, снимает проблему разрешимости. При построении конструкций, соответствующих процедурам языков программирования с процедурными же параметрами, используются конструкции типа ((XY)(AB)), содержательно означающие, что для реализации вычисления B по A необходим вызов процедуры, вычисляющей Y по X. Ясно, что семантическая нагрузка центральной импликации при этом отличается от таковой для крайних импликаций, что накладывает определенные ограничения на практическое применение теории.

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

Широкое распространение дедуктивные технологии получили при разработке систем принятия решений, экспертных систем и комплексов проектирования [Харф 1983,1984], где предлагается дедуктивный планировщик, работающий в классе линейных и ветвящихся программ.

Синтезатор входит составной частью в системы проектирования, унаследовавшие возможности комплексов ПРИЗ и НУТ – [Harf 1994], [Grossschmidt and Harf 2001].

Индуктивный подход к автоматической генерации программ характеризуется поиском общих закономерностей на основании анализа свойств некоторого ряда объектов и, в определённом смысле, является моделированием метода обобщений, применяемого человеком. В рамках этого подхода может осуществляться синтез программ по предъявленным примерам её работы [Burstall and Darlington 1976], синтез общего доказательства по образцам, по частным случаям и т.д. Обобщение строится как с учётом семантики анализируемых объектов, так и на чисто внешнем, синтаксическом уровне. Последний метод детально исследуется Я.М.Барздинем. В [Барздинь 1981] рассматриваются правила индуктивного вывода для случая, когда исходными данными являются деревья специального вида, там же доказывается теорема о полноте приведённых правил. Теорема гарантирует построение общей закономерности (программы) при условии, что исходных примеров достаточно много, правда, конкретизации понятия «достаточно много» не приводится. В [Барздинь 1983] предлагается осуществлять синтез в языке многоточечных термов, которые являются формализацией понятия перечисления. Индуктивный подход допускает использование в качестве объектов анализа пар «вход-выход» требуемой программы. Примером этого может служить система, описываемая в [Hardy 1975], которая позволяет строить простые лисповские программы обработки списков.

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

Некоторые соображения по этому поводу приводятся в [Новосельцев и Тютерев 2001] и [Новосельцев и Аксенов 2006].

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

В работах [Burstall and Darlington 1976,1977] предлагается характерный метод преобразования программ путем свертки-развертки (fold-unfold). При этом выполняются следующие действия:

производится развертка исходного текста – вызов фиксированной процедуры заменяется ее телом;

развернутый текст преобразуется и оптимизируется (настраивается);

тело процедуры свертывается с элиминированием соответствующих фрагментов.

Система, описанная в [Касьянов и Поттосин 1982], позволяет получить эффективные конкретизации исходной универсальной программы за счёт сужения классов входных данных и оптимизации, которая проводится на основе анализа текста программы. Последующие работы В.Н.Касьянова и соавторов включают еще больше элементов дедуктивного подхода, что подтверждает перспективность интеграции. Это же подтверждает и широкое распространение инструментальных оболочек, поддерживающих элементы технологии CASE (Computer Aided Software Engineering) – см., например, [Leblang and Chase 1984] и огромный репозитарий на www.bitpipe.com.

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

1.2. Модальные логики Содержательно, логика представляет собой совокупность формальных языков, обладающих различными свойствами. Специалисты в области IT, которые работали с инструментарием классической логики, наверняка по чувствовали неадекватность этого формализма для целей представления некоторых форм знаний и для осуществления некоторых типов рассуждений, а точнее, знаний приблизительных, интроспективных или меняющихся со временем. Для представления таких приблизительных или изменчивых знаний подходят неклассические логики знания и веры. Они же позволяют про водить модифицируемые рассуждения с позиций «здравого смысла». Эти логики знания и веры составляют часть класса логик, называемых модальными (см. [Gabbay and Guenther 1984]), среди которых различают эпистемические, деонтические, временные и ряд других.

Обычно, говоря о приложениях модальных теорий, имеют в виду область математической лингвистики – проблемы, связанные с формализацией и распознаванием семантики естественных языков (см. [John and Bennet 1982], [Lakoff 1972] и т.д.). В то же время следует упомянуть работы, относящиеся и к другим прикладным областям. В частности, динамические и временные логики используются для формализаций программной семантики [Тейз и др. 1998]. Значительное число работ посвящено вопросам управления базами данных с использованием модальностей (см. [Тейз и др. 1990]). Обоснованный интерес модальные теории вызывают у специалистов в области экспертных систем ([Heeffer 1986]), поскольку приватность и относительная достоверность экспертных оценок, а, следовательно, и возможная противоречивость базы экспертных знаний, не могут поддерживаться аппаратом классических теорий.

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

Прекрасное изложение базовых положений модальной логики приведено в трудах [Фейс 1977], [Тейз и др. 1990, 1998], там же упоминаются области и варианты практического приложения достижений из этой области. – Из этих источников заимствованы основные обозначения и базовые утверждения, что отмечается при необходимости соответствующими ссылками.

В качестве исходного модального исчисления часто рассматривают минимальную модальную логику (систему K), которая определяется соотношением K = {i i есть нормальная логика}.

В свою очередь нормальность определяется наличием в логике схемы K: (АB)( А B) и модального правила вывода необходимости: A А.

Стоит отметить, что многие нормальные теории обладают дополнительными для использования в прикладных областях выразительными средствами, но сохраняют при этом базовые черты класса K.

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

по отношению к целеориентированным (более распространенным) методам.

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

Идея поиска доказательства от аксиом была впервые высказана в [Gentzen 1934]. В этой работе Генцен показал, как доказать разрешимость интуиционистской пропозициональной логики, используя поиск снизу вверх в исчислении секвенций. Доказательство основывалось на свойстве подформульности. К сожалению, эта работа довольно долгое время осталась незамеченной. Всеобщий интерес к обратному методу установления выводимости появился в связи с серией работ С.Ю.Маслова:

[Маслов 1964,1966,1967,1968,1969], [Давыдов и др. 1969], [Маслов 1971] и [Маслов 1972].

Сам термин «обратный метод» был введен в [Маслов 1964]. В этой работе был предложен метод установления выводимости для формул классического исчисления предикатов без равенства и функциональных символов, при этом не использовалась скулемизация, и метод был разработан для применения к формулам канонического вида:

i Q1x1... Qnxn( Dij), i =1 j = где Q1x1... Qnxn – кванторный префикс, а Dij – дизъюнкции литер. Там же был выделен важный класс формул:

i ***( Dij), i =1 j = где 1 2,..., 2. Этот класс формул в дальнейшем получил название Масловский класс формул [Borger and others 1997]. Чрезвычайно интересная работа [Маслов 1969] содержит обсуждение соотношения между обратным методом и методом резолюций.

Общая схема обратного метода заключается в следующем. Для данного произвольного исчисления секвенций генценовского типа G, обладающего свойством подформульности, и произвольной секвенции строится -наборов».

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

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

В работе [Минц 1981] обратный метод был впервые применен к неклассическим пропозициональным логическим исчислениям, правда, под названием «резолюции». В [Воронков 1985] впервые появляется другая формулировка обратного метода. В этой работе обратный метод рассматривается для классической логики без равенства на основе обратного исчисления свободных переменных. В 1992 году, в работе [Воронков 1992] появляется описание обратных исчислений со свободными переменными для неклассических предикатных логик.

Метод свободных переменных для классической логики с равенством был введен в работе [Degtyarev and Voronkov 1995]. В этой же работе рассматривается ряд критериев избыточности, в том числе и критерий, основанный на отношении упорядочивания. Реализация обратного метода для предикатной интуиционистской логики описана в работе [Tammet 1996], а в [Voronkov 2000] было впервые введено понятие исчисления путей (достаточно ограниченное).

1.3. Дескриптивные логики Как отмечалось выше, подходы к работе с когнитивной информацией начали активно разрабатываться в 60-70-х годах прошлого века и разделились на направления: логические формализмы и представления, основанные не на логике. Последние подходы позиционировались, как предлагающие универсальный инструментарий для различных типов задач. Знания в них представляются разнообразными информационными структурами (семантические сети и матрицы, фреймовые комплексы, потоковые сети и т.д.). Вообще говоря, выразительные возможности некоторых из перечисленных методик приближаются к выразительности естественного языка, при этом, правда, перспективы построения строгих формальных процедур манипулирования знаниями являются столь же отдаленными (возможно, недостижимыми), как и в случае естественного языка. Для работы со знаниями вводятся специальные стратегии, зачастую сильно зависящие от конкретной интерпретации моделируемой предметной области, частных взглядов разработчика и иных моментов субъективного характера. В последнее время в этих областях в качестве инструмента «наведения порядка»

стали очень популярны так называемые дескриптивные логики (ДЛ).

Дескриптивные логики являются подмножеством модальных логик, при этом они рассматриваются как специализированные языки, поддерживающие типизацию и композицию [Borgida 1995]. Все ДЛ обладают, как минимум, двумя видами термов: концептами (классами – элементами базового домена) и ролями (бинарными отношениями на домене). Называя вещи своими именами, следует отметить, что ДЛ являются типизированными теориями, снабженными набором конструкторов специального вида. Концепт может быть комбинацией ранее определенных концептов и ролей, которая строится с использованием одного из конструкторов конкретного диалекта дескриптивного языка, что должно обеспечивать моделирование более сложных объектов анализируемой ПО [Borgida 1996]. При этом повторяем, дескриптивные логики позволяют расширять набор конструкторов относительно стандартного набора (конъюнкции, отрицания, квантора всеобщности и т.д.).

Важнейшей особенностью дескриптивных логик, их визитной карточкой, является возможность строить иерархии на концептах. Говорят, что концепт С является подклассом концепта D, если при любой интерпретации I, CI DI. Вводятся также понятия несвязных и согласованных концептов, т.е. определяется некоторый частичный порядок. Предлагаемые механизмы вывода большей частью используют семантические матрицы [Brachman and other 1993].

В тех или других вариантах дескриптивные логики применяются в области баз данных [Buchheit and others 1997], в лингвистике, медицинских приложениях [Rector and others 1997] – область их применения постоянно растет. Помимо ставших уже классическими вариантов дескриптивных логик, разрабатываются расширения для вероятностных ДЛ [Koller, Levy and Pfeffer 1997], логик с n-арными ролевыми отношениями [Luntz, Sattler and Tobies 1995]. Появляются и другие вариации, увеличивающие выразительность языка и стройность создаваемых с их помощью моделей предметной области.

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

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

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

Глава 2. Структурные функциональные модели 2.

2.

В этой главе предпринимается попытка построения формализма, призванного обеспечить возможность создания строгих и, в то же время, адекватных моделей для широкого круга предметных областей. Для достижения этой цели мы будем отталкиваться от хорошо разработанной теории вычислительных моделей ([Тыугу 1970], [Минц и Тыугу 1983]) и использовать ряд современных подходов и достижений.

2.1. Язык теории. Основные определения Дадим основные определения. Прежде всего, зафиксируем сигнатуру :

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

Элементы множества A называются именами объектов или объектами, если это не приводит к двусмысленности. Связь объекта a со схемой S отражается записью S(a). Если объект a связан со схемой S и SE, стандартная запись S(a) заменяется записью aS либо просто a, когда ссылка на NB: Подчеркнем, что реализации первичных схем экспортируют также первичные свойства (операции и отношения) соответствующих типов.

схему не важна или очевидна из контекста. – Истинностное значение синонимов aS и S(a) будем определять следующим образом: aS=И, тогда и только тогда, когда aISI, где aI и SI обозначают реализации (на интерпретации I) величины и схемы соответственно.

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

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

Имена объектов при моделировании конкретной ПО формируются из элементов множества A и удовлетворяют следующему рекурсивному определению:

Определение 2.3. Пусть aA, – имя объекта, тогда a,.a и a. также являются именами объектов. В записи вида.a называется префиксом.

Длина произвольного имени определяется числом вхождений элементов множества A (с учетом возможных повторений), из которых сформировано имя.

Реализация f – вычислимая функция.

Одним из базовых является понятие (непервичной) схемы объекта:

Определение 2.4. Схема S объекта r определяется выражением вида S(r) = r.(S01(a01),…, S0N0(a0N0), p1 S11(a11),…,S1N1(a1N1) … if (2.2) pk Sk1(ak1),…,SkNk(akNk) fi filter ), где SD\E, rA. Для всех возможных значений индексов i, j, SijD – собственные подсхемы схемы S, aijA – ее собственные величины, piP – (возможно, параметризованные) выбирающие селекторы. В правой части (2.2) r называется префиксом схемы, участок до вертикальной черты – заголовком, фрагмент if…fi – вариантной его частью, а остальная часть заголовка – постоянной частью. Символ « » заимствован из нотации «охраняемых команд» (см. [Дейкстра 1975]) и, в некотором смысле, соответствует традиционному «case». Иероглиф filter скрывает список собственных ФС схемы S. Считается, что префикс r может «проноситься» в скобочный фрагмент, так что r.(S(a),…) (r.S(a),…) (S(r.a),…). Аналогичным образом префиксируются имена селекторов и отображений, а также имена величин, вовлеченных в формирование ФС из набора filter 1.

Замечание. Фиксация множества ED для конкретной ПО не является статической. При необходимости, можно сделать доопределение «вниз», представив ранее первичный элемент в форме (2.2) и детализировать Определение 2.4, на первый взгляд, предоставляется не более чем механизмом введения сокращения при описании ПО, однако смысл использования данного понятия, является существенно более глубоким.

E.

рассматриваемую ПО соответствующей модификацией множества Требование конечности множества E при этом не нарушается.

Селекторы на интерпретации I получают истинностные (шкальные) значения и образуют полную систему, т.е. i,j, ij, pi|I&pj|I=Л и p1|I…pk|I=И.

Синтаксическая конструкция (2.2) на интерпретации I определяет размеченное отношение в смысле [Дейкстра 1975].

Можно отметить некоторую аналогию между введенным здесь понятием схемы и отношением в теории реляционных баз данных [Ульман 1983]. Используя это, мы иногда будем употреблять термины реляционного подхода, такие как «атрибут», «подсхема», «кортеж» и т.д. Укажем теперь требования, которым удовлетворяет набор filter схемы. Для этого, прежде всего, определим, какие имена величин порождаются заголовком схемы.

Определение 2.5. Пусть S(r)=(…Sij(r.aij)…) – схема. Если SijE, то r.aij – имя величины схемы S. Если SijD\E и – имя величины схемы Sij, то r.aij. – имя величины схемы S. В дальнейшем имена величин схемы S будем называть её атрибутами.

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

Определение 2.6. Рассмотрим схему S. ФС f:1,…,n0 из filter называется допустимой для схемы S, если и только если 0,1,…,n – атрибуты схемы S.

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

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

ФС содержит по крайней мере один собственный атрибут схемы;

в наборе filter нет ФС, в которые вовлечены атрибуты из разных альтернативных ветвей схемы S или атрибуты из альтернативных частей её подсхемы;

длина любого атрибута, связанного ФС, не превышает двух (то есть мы не опускаемся более чем на один уровень в структуре подсхем).

Иногда величины предметной области, для которой строится модель, имеют смысл только при выполнении некоторого критерия. Так, о гипотенузе и катетах можно говорить лишь в контексте прямоугольного треугольника. – Для отражения подобных фактов служит альтернативная часть заголовка схемы – она указывает, когда определены те или иные атрибуты. В ряде случаев информацию об осмысленности атрибутов схемы бывает важно иметь в наборе filter. Для этого вводится понятие атрибута с условием (атрибута, модифицированного селектором) или у-атрибута:

Определение 2.7. Факт наличия условия p у атрибута будем отмечать записью /p, а соответствующее выражение называть у-атрибутом.

Будем считать, что с атрибутами, определёнными в общей части заголовка, связывается условие И. Если в записи у-атрибута /p p И, то /p можно опустить.

В качестве примера схемы приведём описание понятия член_ряда, определяющего n-й член натурального ряда либо ряда Фибоначчи (в зависимости от значения скаляра s). По-прежнему, символом «N» будем обозначать тождественное отображение:

член_ряда(r) = r.(scalar(s), integer(x), integer(n), if (= s «натуральный») integer(xn) число_фиб(xf) fi | (= s «Фибоначчи») N : n xn ;

N : xn x ;

N : n xf.n ;

N : xf.f x ).

В этом примере неэлементарной является схема число_фиб, которая определяет член ряда Фибоначчи. Описание этой схемы будет приведено позднее, когда мы коснёмся рекурсивных конструкций. Собственными атрибутами схемы член_ряда являются s, x, n, xn и xf. В схеме число_фиб, связанной с атрибутом xf, определены атрибуты n и f, таким образом, в схеме член_ряда появляются префиксированные атрибуты xf.n и xf.f. Для натурального ряда значение n-го члена совпадает с его номером n – этот факт отражается двумя первыми ФС схемы. Число Фибоначчи вычисляется по более сложным законам, определяемым схемой число_фиб. Вход в подсхему число_фиб схемы член_ряда и выход из неё осуществляется посредством двух последних ФС набора filter схемы член_ряда 1.


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

Определение 2.8. Структурной (С-) моделью называется конечная совокупность схем M=(S1,…,Sm), где каждая Si, i=1,…,n, является элементарной или задана в соответствие с определением 2.4 2.

Определение 2.9. С-модель M является (синтаксически) замкнутой, если и только если для каждого её элемента SiM схемы, встречающиеся в определении Si, являются элементарными либо определены в описании С модели M.

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

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

Можно заметить сходство определяемого здесь понятия модели и библиотеки классов в популярном «объектно-ориентированном» подходе.

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

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

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

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

При исследовании свойств С-моделей и алгоритмов синтеза программ в них нам потребуется понятие развёртки схемы S. Оно определяется через развёртку схемы на атрибуте.

В определении задачи не все имена атрибутов из наборов A0 и X0 обязаны явно присутствовать в заголовке схемы S – это могут быть и произвольные атрибуты схемы.

Определение 2.11. Пусть S(r)=r.(…Sij(aij)…| filter) – схема, и SijE. Развёрткой схемы S на атрибуте aij будем называть выражение, получающееся в результате a) подстановки в заголовок исходной схемы на место Sij(aij) заголовка схемы Sij и b) присоединения к набору filter схемы S всех ФС схемы Sij.

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

Процесс построения развёртки на атрибуте может повторяться многократно – пока имеются атрибуты, связанные с неэлементарными схемами.

Определение 2.12. Под полной развёрткой S С-модели понимается объект, полученный из схемы S, у которой в результате последовательности развёрток на атрибутах в заголовке остаются только атрибуты, связанные с элементарными схемами.

Полная развёртка, вообще говоря, не является схемой в смысле определения 2.4, однако понятие схемы нетрудно переопределить с тем, чтобы оно оставалось корректным для развёртки на атрибуте и полной развёртки. Для этого необходимо в выражении (2.2) разрешить появление нескольких if…fi-участков и потребовать, чтобы единственным видом их пересечения было строгое вложение (как оно трактуется в структурном подходе [Вирт 1977]).

При построении С-модели допускаются возможность рекурсивных определений схем. Рекурсивная конструкция должна содержать, по меньшей мере, одну цепочку определений вида S1=(…[S2]…), S2=(…[S3]…),…, Sk=(…[S1]…), обеспечивающую участие в дефиниции некоторого понятия ссылки на себя. Схемы Si, i=1,…,k будем называть рекурсивными. Ясно, что полная развёртка рекурсивной схемы не определена – процесс её построения не завершается. Ниже будет показано, что некоторые естественные ограничения позволяют выделить класс С-моделей, включающий рекурсивные схемы, в котором проблема выводимости эффективно решается, т.е., по меньшей мере, не требуется полная развертка схемы.

Приведем пример рекурсивной схемы, определяющей n-й элемент ряда Фибоначчи:

число_фиб(r) = r.(integer(n), integer(f), if (= n ‘0’) integer(ff) (= n ‘1’) integer(sf) ( n ‘1’) число_фиб(nf), число_фиб(nnf) fi | N:’1’ff;

N:sff;

N:’1’ff;

N:fff;

subtract:n,’1’ nf.n;

subtract:n,’2’ nnf.n;

sum:nf.f, nnf.f f) Для практической деятельности используемый в диссертации язык теории мало пригоден – на его основе с соблюдением традиций и практики программирования создан более удобный язык Bool, применяемый, правда, пока только в исследовательских целях.

2.2. Нерекурсивные детерминированные С-модели В этом параграфе мы выделим полезный класс С-моделей. Для этого понадобится понятие детерминированной схемы. Чтобы подчеркнуть факт детерминируемости (отвлекаясь пока от вопроса задания интерпретации С модели) мы будем использовать двухальтернативную форму записи if…fi участка: if p S11(a11),…;

S21(a21),… fi – подразумевая, что реализация S11… осмыслена при истинности реализации p, а S21… – в противном случае.

Определение 2.13. Схему S вида (2.2) будем называть детерминированной, если она не имеет альтернативной части либо её альтернативная часть имеет форму if p …;

… fi.

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

Определение 2.14. С-модель M=(S1,…,Sm) называется нерекурсивной детерминированной (НДС-) моделью, если выполнены следующие условия:

M – синтаксически замкнута;

S1,…,Sm – детерминированные схемы;

любая схема Si модели определяется только через элементарные схемы либо через схемы, которые предшествуют Si в модели M.

Ясно, что в НДС-модели полная развёртка любой схемы является конечной. Различные задачи в НДС-модели приводят к различным в смысле [Диковский 1984] вычислительным моделям. Это может происходить, в частности, если задачи ставятся на разных схемах НДС-модели.

Рассмотрим подробнее вопрос о соотношении НДС-моделей и детерминированных вычислительных моделей, которые определяет А.Я.Диковский. Для этого введем понятие строго детерминированной схемы.

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

Напомним ключевые определения из [Диковский 1984]. Под детерминированной (Д-) вычислительной моделью понимается конечная система детерминированных уравнений. Детерминированное уравнение для величины (атрибута) a – это выражение (a) вида if p 1 1 … p n n fi, в котором n0, p1,…,pn – попарно различные селекторные символы и 1,…,n – символы отображений, у которых результатом является атрибут a.

Покажем, что полная развёртка схемы НДС-модели является Д вычислительной моделью в смысле [Диковский 1984].

Теорема 2.1. Полная развёртка любой схемы S НДС-модели M определяет некоторую модель Диковского, если M составлена только из строго детерминированных схем.

Доказательство. Рассмотрим схему S(r) = r.(S01(a01),…,S0N0(a0N0), if pS11(a11),…,S1N1(a1N1);

Sk1(ak1),…,SkNk(akNk) fi filter ).

Напомним, что атрибутам схемы S естественным образом приписываются условия И, p или –p в зависимости от местоположения в заголовке. В развёртке исходной схемы S может появиться фрагмент (префикс «r.»

опускается) …if p … if ast.q … ast.Sqr(bqr),…, fi … fi.

В этом случае атрибуту ast.bqr приписывается условие p&ast.q. Поскольку полная развёртка схемы в НДС-модели является конечной, возможно произвести переименование и заменить сложные имена (уникальными) простыми. Требование счётности соответствующих элементов сигнатуры при этом не нарушается. Для завершения доказательства достаточно сделать последний шаг. Набор filter развёртки содержит теперь различные ФС вида f:c1/p1,…, cn/pnc0/p0. Припишем каждой ФС условие Pf p0&p1&…&pn.

Соберём все ФС, правые части которых (результаты) совпадают, и сформируем для каждого результата детерминированное уравнение (c0) вида c0 = if Pf 1 f1 Pf 2 f2 … Pf n fn fi. Очевидно по построению, что (i) n0;

(ii) Pf1,…,Pfn – попарно-различны;

(iii) для каждого атрибута c имеется не более одного (c);

(iv) детерминированных уравнений конечное число.

Замечание. А.Я.Диковским показано, что при выборе семантики, в которой не используется внешняя управляющая память для задания условий в детерминированных уравнениях, проблема синтеза в Д-вычислительных моделях является NP-полной. В НДС-моделях алгоритмы, решающие проблему синтеза, обладают полиномиальными характеристиками. Теорема 2.1 позволяет выделить в классе моделей Диковского «хороший» в алгоритмическом плане подкласс моделей.

...

a1 a2 an f a Рис. 2.1. Изображение ФС Для иллюстрации рассуждений в работе используется аппарат теории графов [Оре 1980]. Функциональная связь f:a1,…,an a0 представляется двудольным графом, изображённым на рис. 2.1.

член_ряда n s I I число_фиб xf.n/P xn/Q xf.a/P I I x Рис. 2.2. Схема член_ряда При этом атрибуты (аргументы и результаты ФС) определяют множество вершин первого сорта (на рисунке – точки), а функциональному символу сопоставляется вершина второго сорта (кружок). Схема изображается графом, являющимся объединением графов, которые соответствуют ФС этой схемы. Выделяя схему, будем заключать её в прямоугольник, в левом верхнем углу которого указывается имя схемы. Схеме «член_ряда», которая описана в разделе 2.1, в этих соглашениях соответствует орграф, приведённый на рис.2.2.


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

Определение 2.16. С-модель M=(S1,…,Sm) называется рекурсивной детерминированной (РД) С-моделью, если выполнены следующие требования:

1) M – синтаксически замкнута;

2) S1,…, Sm – детерминированные схемы;

3) при построении развёртки любой схемы Si модели M выражения вида.Si(…), где – (различные) префиксы, появляются только в одной из двух альтернативных ветвей Si. При этом выражения.Si(…) определяют рекурсивные вхождения исходной схемы, ветвь, в которой имеются рекурсивные вхождения, называется рекурсивной ветвью, а сама Si – рекурсивной схемой.

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

Теорема 2.2. Принадлежность С-модели M=(S1,…,Sm) классу РДС устанавливается конструктивно за конечное время, пропорциональное O(|M|4)=C m4.

Доказательство. Построим конструктивную процедуру проверки выполнения определения 2.16.

1) Требование синтаксической замкнутости проверяется со временем, не превышающим O(|M|3). – Рассматриваем последовательно схемы Si модели M. Для каждой подсхемы из заголовка Si со временем не более O(|E|) выясняем, является ли она элементарной;

в случае отрицательного результата со временем O(|M|) ищем её имя среди имен схем модели M, если оно там не обнаруживается, заключаем, что M не относится к классу РДС. Грубая оценка этого этапа |M|O(|M|+|E|)(O(|M|)+O(|E|))O((|M|+|E|)3) может быть улучшена за счёт использования различных технических приёмов при описании модели, таких как аппарат предописаний, традиционный для языков программирования. Количество первичных схем |E| считается фиксированным.

2) Требование детерминированности схем модели заключается в проверке выполнения определения 2.13 – отсутствие вариантной части заголовка, либо вариантная часть в форме if p …;

… fi;

время оценки – O(|M|).

3) Третий этап проверки – наиболее трудоёмкий. При этом также последовательно рассматриваются схемы модели. Производя развёртку Si, останавливаемся, когда доходим до элементарной подсхемы либо до рекурсивного вхождения схемы.Si(…).

| M | Si:

1: Si1 … S i1… S i | M | 2: Si1…Si1 Si 2 Si......

.

..

.

| M | 1 :...............

Рис.2.3. Развертка с вычеркиванием Если при этом не использовать дополнительные соображения, напрашивается очевидная оценка O(|M|N|M|), где N – максимальное количество атрибутов в заголовках схем. Однако, затраты на этом этапе можно радикально уменьшить, заметив, что для анализа характера схемы Si каждую подсхему в её развёртке достаточно рассмотреть один раз. Развёртка, полученная с использованием такой стратегии, схематически изображена на рис.2.3.

В этой развёртке выделены уровни:

первый – совпадает с заголовком исходной схемы, в котором каждая группа атрибутов с совпадающими именами схем (символами из множества D) для дальнейшей развёртки имеет по одному представителю;

второй уровень – в развёртках на оставшихся атрибутах также оставлено по одному представителю для групп, а, кроме того, вычеркнуты атрибуты, имена схем которых совпадают с именами схем – непосредственных предшественников;

последующие – строятся аналогично.

Ясно, что глубина такой развёртки не превышает |M|-1. Таким образом, затраты третьего этапа могут быть оценены величиной O(|M|((|M|(|M| 1)/2)(|M|-1))) = O(|M|4). Суммарные затраты на выполнение всех трёх этапов определяются оценкой для третьего этапа, т. е. O(|M|4).

Класс РДС-моделей включает в себя класс НДС. Задача для РДС моделей удовлетворяет определению 2.10. Решение задачи T=(A0,X0,S) в РДС модели M, неформально, можно трактовать как нахождение пути в графе, соответствующем схеме S. Реализующий вычисление (программный) терм F строится с использованием ФС, которые явно или опосредованно присутствуют в схеме S. Исчисление, используемое при этом, будет строго описано и исследовано в последующих разделах, здесь проблема синтеза рассматривается на содержательном уровне. Подтерм G терма F отражает факт достижимости одних атрибутов схемы через другие, Простейшими подтермами являются имена ФС схемы S. Условие, при котором в процессе построения F обеспечивается достижимость некоторого атрибута, может не совпадать с условием, при котором этот атрибут описан в исходной схеме (в развёртке исходной схемы). В дальнейшем эти условия мы будем называть условиями достижимости и допустимости атрибута соответственно.

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

Требование (в) является естественным отражением того, что величину ПО, имеющую смысл при условии p, нельзя вычислить через другую величину, определённую при дополнительном условии –p. Будем считать, что при использовании ФС f:a1,…,an a0 для построения терма F, условие достижимости a0 определяется конъюнкцией условий достижимости аргументов и условия допустимости результата.

Процесс полной развёртки некоторой схемы S задаёт иерархию, в частности, селекторов – на них может быть определено отношение частичного порядка. Имена селекторов, также как и атрибуты, формируются с использованием префикса, который определяется развёрткой схемы S. Это соглашение гарантирует уникальность имён различных объектов (в том числе и селекторов) в развёртке. Определим отношение порядка следующим образом:

Определение 2.17. Если в развёртке схемы S имеется фрагмент … if.p … if..q … fi … fi…, то..q и дополнительное условие..-q будем называть более сильными условиями по сравнению с.p и отмечать этот факт записью вида..q.p (символ «-» здесь используется как знак принадлежность имени дополняющего селектора, а не обозначение операции). Если A, то..q и..-q будем называть непосредственно более сильными условиями, чем.p и записывать это в форме..q.p.

Определение 2.18. Пусть имеется рекурсивная схема S. Рассмотрим фрагмент её развёртки: (…Sij(aij)…if….Sij(aij)…fi…). Атрибут.aij будем называть следующим за aij и обозначать его nk(aij), где k – длина префикса.

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

2.4. Интерпретация С-модели Интерпретация (или семантика) С-модели задаётся традиционно.

Определение 2.19. Интерпретация I С-модели M задаёт:

для каждой схемы SE непустое множество (первичный тип) S|I;

для каждого fF – отображение f|I:S1|I…Sn|I S0|I ;

для каждого pP – булевское отображение p|I:S1|I…Sn|I{И, Л}.

В результате задания интерпретации каждой неэлементарной схеме сопоставляется отношение. Отношение трактуется как множество наборов, удовлетворяющих некоторым условиям. Наборы принадлежат декартову произведению множеств, сопоставленных подсхемам схемы S. Элементы наборов поименованы атрибутами заголовка. Если в заголовке схемы присутствует альтернативная часть, то наборы отношения выбираются из размеченного декартова произведения [Дейкстра 1975]. Разметку определяют селекторы альтернативной части. Термин «тип атрибута» служит сокращением для выражения «множество, сопоставленное схеме, с которым связан атрибут». В отличие от первичного типа такой тип мы обычно будем называть (непервичным) типом, наборы типа – кортежами, а их именованные элементы – компонентами.

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

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

Определение 2.20. Рассмотрим M=(…S…). Пусть A {a0/pa0,…,an/pan} – множество атрибутов S, f:b1/pb0,…,bk/pbkb0/pb0 – функциональная связь этой же развёртки (bi/pbiA, i=0,…,k), а r – некоторый кортеж, определяемый заголовком схемы S. Будем говорить, что |I имеет смысл для кортежа r, если pbi|I=И, i=0,…,k. Кортеж r принадлежит типу S|I, если на r выполнены все функциональные соотношения, которых имеют смысл для него.

Для класса РДС-моделей кортежи, вообще говоря, сколь угодно длинны.

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

Определение 2.21. Выражение вида F : A X, где F – (программный) терм в сигнатуре, построенный по правилам, приведенным в третьей главе, A и X – непустые наборы у-атрибутов, называется предложением вычислимости (ПВ).

Наборы A и X называются аргументами и результатами ПВ соответственно.

Для определенного выше понятия нарушается классическая «функциональность», однако традиционные приемы («ПВ есть объединение ФС таких, что…») позволяют не выходить за рамки классики.

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

1. Он является собственным подклассом хорошо определенного общего класса Д-моделей, но, в отличие от родительского, обладает свойствами эффективной распознаваемости (по длине описания самой модели, а не ее развертки) и полиномиальной разрешимости.

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

3. Информация о работе на каждой подсхеме фиксируется и может использоваться в дальнейшем – обеспечивается бесповторность поиска решения («запроцедуривание»).

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

Глава 3. Установление выводимости в РДС-модели 3.опр- 3.теор- В этой главе определяется теория, в рамках которой осуществляется построение программного терма-решения для задачи T=(A0,X0,S), когда S является схемой РДС-модели. Показывается полнота и непротиворечивость теории относительно понятия выводимости предложения вычислимости.

Формулируется алгоритм решения задачи T и исследуется вопрос его корректности.

3.1. Формальное исчисление. Правила вывода Будем строить исчисление, проблема установления выводимости формулы в котором сопровождается одновременным построением программного терма решения задачи, соответствующей непроцедурной спецификации. Более строго необходимо, исходя из задачи T=(A0,X0,S), построить программный терм-решение F, такой, что для произвольной интерпретации I принадлежность кортежа r типу S|I гарантирует выполнение на r соотношения, которое задаётся реализацией F|I. Терм-решение F извлекается из доказательства теоремы существования (решения) вида (F) F : A0 X S (3.1) M формулируемой на основании задачи T. Установление выводимости (3.1) проводится в рамках некоторой формальной теории. Содержательно это означает, что, используя информацию о структуре схемы S и соотношения между её атрибутами, а также используя соответствующие правила вывода, мы пытаемся построить ПВ, которое связывает атрибуты множеств A0 и X0 и удовлетворяет схеме S.

Приведем необходимые определения:

Определение 3.1. Пусть M=(…S…) – РДС-модель, пусть также a1/p1,…,an/pn, x1/q1,…,xm/qm – у-атрибуты развёртки S, F:a1/p1,…,an/pnx1/q1,…,xm/qm – предложение вычислимости, а r – кортеж, определяемый заголовком развёртки при некоторой интерпретации I. Говорят, что |I имеет смысл для кортежа r, если pi|I=И, i=1,…,n и qj|I=И, j=1,…,m.

S A n.S /p n.A /-p n.X G1 G X Рис. 3.1. Пример рекурсивной схемы Определение 3.2. Будем говорить, что ПВ F:AX удовлетворяет схеме S, если при любой интерпретации I тип S|I не содержит двух кортежей, для которых |I имеет смысл, таких что их компоненты совпадают для всех атрибутов множества A, но не совпадают по крайней мере для одного атрибута множества X. При этом для произвольного кортежа r, который принадлежит отношению S|I, результатом применения F|I к компонентам r, именованным атрибутами множества A, является набор компонент, именованных атрибутами множества X. Все ФС схемы удовлетворяют ей по определению.

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

S(r) = r.(A,X, if p …;

S(n),… fi | filter), (3.2) где A и X – наборы атрибутов S и n – атрибут, связанный с рекурсивным вхождением схемы. На рис. 3.1 изображён граф, который соответствует (2.2) с точностью до ФС из набора filter. В левой части рисунка сосредоточены ФС, связывающие, атрибуты p-ветви, в правой – атрибуты -p-ветви, такому соглашению мы будем следовать и в дальнейшем.

Значения X могут быть определены по A независимо от условия p в том случае, когда существует A0 A, который обеспечивает – достижимость X/p и – достижимость n.A0/-p (в рекурсивном вхождении), кроме того должна быть обеспечена достижимость X/-p по n.X/-p. В этом случае индукционный переход позволяет предположить существование рекурсивного программного терма, хотя о семантической корректности речи вести и нельзя. Рассуждая неформально, можно отметить, что схема r.S(n) является «копией» схемы S(r) «на более низком уровне». Если предположить существование терма F, который обеспечивает достижимость n.X/-p по n.A/-p, то можно заключить, что вид терма, доставляющего X по A, будет следующим: F = if p then G1 else G2[F] fi. – Именно этими соображениями мы будем руководствоваться, вводя в исчисление соответствующее правило.

3.1.1. Исчисление SR Опишем исчисление, в котором производится поиск доказательства теоремы существования (3.1).

В теории имеется три сорта термов, которые строятся в сигнатуре согласно следующему определению.

Определение 3.3.

(1) Термы первого сорта (а-термы) представляют собой упорядоченные списки (n-ки) атрибутов (атрибуты понимают в смысле второй главы). Они порождаются элементами множества A.

(2) Термы второго сорта (у-термы) строятся из термов первого сорта и предикатных символов, принадлежащих множеству P, согласно следующей рекурсивной процедуре.

Пусть p – селектор, реализуемый n-местной булевской функцией, pP;

A – n элементный терм первого сорта, такой, что его i-й атрибут связан с той же схемой, что и i-й аргумент p;

P и Q – термы второго сорта;

– некоторый атрибут;

«-» и «&» - операции отрицания и конъюнкции соответственно.

Тогда перечисленные выражения являются термами второго сорта:.p(A), -P, P&Q. Других термов второго сорта нет.

(3) Наконец, программные (пр-) термы третьего сорта строятся из термов всех сортов по следующим правилам.

Пусть P – терм второго сорта;

f, g, h – функциональные символы (элементы множества F);

F1, F2, F3 – термы третьего сорта и имеются вхождения символа g в F3;

– некоторый атрибут;

F3[h/g] – обозначение замены вхождения g на h в терме F3. Тогда.h:…… – терм третьего сорта;

F1;

F2 – терм (оператор суперпозиции);

if P then F1 else F2 fi – терм (оператор ветвления);

h= if P then F1 else F3[h/g] fi – терм (оператор рекурсии). Других термов третьего сорта нет.

В исчисление входит одна схема аксиом и четыре правила вывода.

N:A A (N – тождественное отображение) (0) схема аксиом:

F:A X,Z (1) (правило сужения) F:A X F:A X,Z/P f:Z x/p (2) (правило суперпозиции) F;

f: A,Z/P X,Z,x/P&p здесь P – конъюнкция условий достижимости атрибутов из Z, а p – условие допустимости x (напомним, что условие достижимости – это условие, при котором в процессе построения доказательства обеспечивается достижимость некоторого атрибута, а условие допустимости – это условие, при котором атрибут имеет смысл в РДС-модели).

F 1:A X,x / Q&p F 2:A X,x / Q&- p (правило ветвления) (3) if p then F 1 else F 2 fi:A X,x / Q F 1:A X,x /Q & p (4) (правило введения g1:n1 ( A)n1 ( X ),...,gs:n ( A)n ( X ) ks ks k k F 2:A X,x / Q& p s рекурсии) s 1 h=if p then F 1 else F 2[h/ g1]...[h/ gs] fi:A X / Q x1/P,…,xm/P, nk – символ введённого в п.2.3 отношения порядка.

здесь X/P Схема аксиом позволяет формировать «начальные» для вывода ПВ предложения вычислимости, отталкиваясь от заданных атрибутов из формулировки задачи Т. Правило сужения (1) применяется в тех случаях, когда необходимо исключить из рассмотрения часть атрибутов, достижимость которых доказана, например, при использовании правила (4) или в конце доказательства.

Правило суперпозиции (композиции, транзитивности) (2) понимается как обычно: если показана достижимость Z и известно, что по Z вычислим x, то можно считать, что показана достижимость x с учётом условий, при которых достижимы атрибуты из Z.

Правило ветвления (3) позволяет ослабить условие при атрибутах: если показана достижимость x при условии Q&p (терм F1) и одновременно при условии Q&-p (терм F2), то ПВ, у которого программный терм построен с помощью оператора ветвления, обеспечивает достижимость x, с элиминированием условий p и -p.

Наконец, правило введения рекурсии (4). Оно применимо только для случая рекурсивной схемы. Установить рекурсивные схемы модели позволяет процедура, описанная в теореме 2.2. Правило означает, что если (a) показана достижимость X/Q&p по A посредством терма F1 и (b) из предположения о nk11(X),…,nkss(X) достижимости следует достижимость X/Q&-p, то достижимо X/Q (при элиминированных p и -p) посредством применения = рекурсивного программного терма h ifpthenF1 elseF2[h/g1]...[h/gs] fi:A X/Q.

Построенную теорию назовем исчислением SR (structural recursive calculi).

3.1.2. Корректность и полнота исчисления SR Рассмотрим и исследуем свойства исчисления SR, важные при решении вопросов о практических применениях построенного формализма. Покажем, что правила исчисления SR для некоторой схемы S РДС-модели M позволяют получить все ПВ, которые удовлетворяют этой схеме S (свойство полноты исчисления SR) и что, используя правила SR, можно построить только ПВ, удовлетворяющие схеме S (свойство корректности SR).

Теорема 3.1. Исчисление SR является корректным относительно понятия ПВ, удовлетворяющего схеме S.



Pages:   || 2 | 3 |
 





 
© 2013 www.libed.ru - «Бесплатная библиотека научно-практических конференций»

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