«НОВОСЕЛЬЦЕВ Виталий Борисович ФОРМАЛЬНАЯ ТЕОРИЯ СТРУКТУРНЫХ МОДЕЛЕЙ ОПИСАНИЯ ИНФОРМАЦИОННЫХ СИСТЕМ И МЕТОДЫ УСТАНОВЛЕНИЯ ВЫВОДИМОСТИ Специальность 05.13.01 – Системный анализ, управление и обработка информации (в ...»

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

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

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

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

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

ВЫВОДИМОСТИ

Специальность 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 Всероссийская конференция по прикладной логике – Новосибирск, управления и ИИ» – Иркутск, ИрВЦ СО РАН, 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. Логические подходы к управлению знаниями Возможности организации и автоматической (алгоритмической) обработки информации привлекала внимание исследователей с давних пор. По сути дела приписывается формулирование алгоритма поиска наибольшего общего делителя двух целых чисел. С появлением и развитием компьютерной техники и соответствующего программно-математического инструментария интерес к исследованиям в отмеченной области только возрос, причем значительные усилия прикладываются к вопросам моделирования интеллектуальных процессов. Можно утверждать, что приоритеты в 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). Задача синтеза удовлетворяющему условию P(x), вычислить значение y, удовлетворяющему условию Q(x,y). Считается, что спецификация R=(P(x),Q(x,y)) содержит достаточно информации для построения программы, которая реализует вычисление значений выходных величин по значениям входных. Задача однозначно представляется тройкой (x,y,R). Теорема существования решения доказательства теоремы существования решения обеспечивает получения требуемой программы. Из такой постановки исходят [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. Ясно, что семантическая нагрузка центральной импликации при этом определенные ограничения на практическое применение теории.

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

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

унаследовавшие возможности комплексов ПРИЗ и НУТ – [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.

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

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

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

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

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

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

где 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. Структурные функциональные модели В этой главе предпринимается попытка построения формализма, призванного обеспечить возможность создания строгих и, в то же время, адекватных моделей для широкого круга предметных областей. Для достижения этой цели мы будем отталкиваться от хорошо разработанной теории вычислительных моделей ([Тыугу 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. Выражение вида где 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), где 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 при этом не нарушается.

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

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

совокупность схем 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) заголовка 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), subtract:n,’1’ nf.n; subtract:n,’2’ nnf.n;

Для практической деятельности используемый в диссертации язык теории мало пригоден – на его основе с соблюдением традиций и практики программирования создан более удобный язык 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) называется нерекурсивной детерминированной (НДС-) моделью, если выполнены следующие условия:

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

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

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

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

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

детерминированной (Д-) вычислительной моделью понимается конечная система детерминированных уравнений. Детерминированное уравнение для величины (атрибута) a – это выражение (a) вида в котором n>0, 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.»

опускается) В этом случае атрибуту 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) n>0; (ii) Pf1,…,Pfn – попарно-различны; (iii) для каждого атрибута c имеется не более одного (c); (iv) детерминированных уравнений конечное число.

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

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

При этом атрибуты (аргументы и результаты ФС) определяют множество вершин первого сорта (на рисунке – точки), а функциональному символу сопоставляется вершина второго сорта (кружок). Схема изображается графом, являющимся объединением графов, которые соответствуют ФС этой схемы. Выделяя схему, будем заключать её в прямоугольник, в левом верхнем углу которого указывается имя схемы. Схеме «член_ряда», которая описана в разделе 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(…).

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

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

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

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

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

Ясно, что глубина такой развёртки не превышает |M|-1. Таким образом, затраты третьего этапа могут быть оценены величиной O(|M|((|M|(|M|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 имеется фрагмент то..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 извлекается из доказательства теоремы существования (решения) вида формулируемой на основании задачи 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.

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

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

где 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 – терм (оператор рекурсии). Других термов третьего сорта нет.

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

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

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) из предположения о достижимо 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.

Доказательство.

Утверждение теоремы означает следующее: если ПВ F:AX выведено с помощью правил SR на основании информации об исходной схеме S модели M, то, независимо от интерпретации I, для любых двух кортежей типа S|I, таких что |I имеет для них смысл, компоненты, соответствующие атрибутам A и X в этих кортежах, совпадают и связаны соотношением, задаваемым |I. – Рассмотрим поочередно схему и все правила и покажем, что они позволяют выводить из ПВ, удовлетворяющих исходной схеме, только те ПВ, которые также ей удовлетворяют.

(0) Очевидно. Независимо от интерпретации I, в S|I не может быть двух кортежей таких, что в них присутствуют одни и те же компоненты A|I, и компонентам.

(1) F:AX,Y – антецедент правила – удовлетворяет схеме S. Это означает, что любые два кортежа, для которых |I имеет смысл, совпадающие по A|I, совпадают также по всему набору X|I,Y|I.

Следовательно, эти кортежи совпадают и по набору X|I. Поскольку весь набор X|I,Y|I является результатом применения отображения F|I к A|I, то X|I получается применением того же F|I к A|I с последующей проекцией (2) (правило суперпозиции). Пусть опять посылками правила являются ПВ, удовлетворяющие схеме S. Рассмотрим два кортежа s и t, для которых реализации посылок имеют смысл, причём s и t совпадают по компонентам A|I. Предположим, что правило (2) некорректно, это означает, что s и t не совпадают по какой-либо компоненте из набора X|I, Z|I, x|I. Несовпадение по фрагменту из X|I, Z|I противоречит тому, что F:AX,Z удовлетворяет схеме S, т. е. s и t совпадают, в частности, по Z|I, которые вычисляются применением F|I к A|I (с выполнением условия достижимости P|I). Последнее означает, что s и t должны совпадать и по x|I, поскольку f:Zx удовлетворяет схеме S. Отметим, что в качестве второй посылки правила суперпозиции всегда берётся ФС из (развёртки) исходной схемы, именно поэтому p – это условие допустимости x. Условие, при котором f|I обеспечивает возможность вычисления x|I по Z|I не может быть более слабым, чем условие, при котором вычислены Z|I, и условие, при котором в S|I допускается присутствие x|I – оно определяется конъюнкцией P&p. Набор X|I, Z|I, x|I вычисляется последовательным применением F|I к A|I и затем f|I к соответствующим результатам предыдущего отображения, т.е.

суперпозицией отображений. – Этим показано, что правило (2) исчисления SR корректно.

(3) (правило ветвления). Предположим, что ПВ из заключения правила не удовлетворяет исходной схеме, если посылками являются ПВ, удовлетворяющие этой схеме. Введём обозначения для ПВ, из формулировки правила:

Пусть задана интерпретация I. Рассмотрим два кортежа s и t таких, что для них (обоих – одновременно) имеет смысл либо 1|I, либо 2|I.

Очевидно, что в каждом из этих случаев для s и t имеет смысл и |I.

Пусть s и t совпадают по компонентам A|I и пусть для них имеет смысл 1|I. Если наше предположение о том, что ПВ из заключения правила не удовлетворяет схеме, является верным, то s и t должны не совпадать по какой-либо компоненте из X|I, x|I, а это противоречит первой посылке правила. В рассматриваемом случае программный терм из заключения правила вырождается до F1, кортежи s и t, совпадая по A|I, совпадают и по компонентам X|I, x|I, а соотношение между A|I, и X|I, x|I определяется реализацией терма if p then F1 else F2 fi при выполнении p. Второй случай (для s и t имеет смысл 1|I) рассматривается аналогично. – Корректность правила ветвления исчисления SR показана.

(4) Наконец, исследуем вопрос корректности правила введения рекурсии.

Будем обозначать:

Отметим, что, хотя в правиле (4) это явно и не указано, в антецеденте предполагается достижимость nkii(A) по A и X по nkii(X), (i=1,...,s), и эти ПВ удовлетворяют исходной схеме S наряду с прочими посылками правила. Как и прежде предположим, что заключение правила – – не удовлетворяет схеме S. Рассмотрим два кортежа s и t из типа S|I, которые совпадают по компонентам A|I. В силу предположения, s и t должны различаться хотя бы по одной компоненте множества X|I. Пусть для s и t одновременно имеет смысл 1|I (удовлетворено условие p), тогда для s и t имеет смысл и 1|I. – Сделанное предположение входит в противоречие с первой посылкой правила, а программный терм в заключении правила вырождается в F1.

Вообще говоря, кортежи (размеченного) типа S|I могут иметь вид (см.

проинтерпретированными.

Мы находимся в рекурсивной ветви (-p), когда кортежи s и t включают фрагмент, помеченный селектором -p.nkii(p) и совпадают по A|I, следовательно, они совпадают по nkii(A) (по правилу суперпозиции и в аргументов»), совпадают по nkii(X) (по правилу суперпозиции и в силу i) и, наконец, кортежи обязаны совпадать по X (по правилу суперпозиции и в силу наличия неявных ПВ «перевычисления результатов» вида G:…nkii(X)X/Q&-p). Таким образом, мы пришли к исчисления SR также является корректным.

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

Определение 3.4. Пусть S(r) = r.(A,X, … | filter) и пусть A – некоторый набор атрибутов схемы S. Замыканием A+ для A относительно S будем называть объединение всех таких атрибутов X, что ПВ F:AX может быть получено с использованием правил SR из информации о схеме S.

Важное свойство замыкания A+ определяется следующей леммой:

Лемма*. ПВ F:AX выводимо по правилам SR, если и только если X A+.

Доказательство: Пусть X = x1,…,xn и пусть X A+. Из определения A+ следует, что для каждого i, i=1,...,n по правилам SR выводимо ПВ Fi:A…,xi,…, из которого по правилу сужения (0) может быть получено ПВ Fi:Axi. Используя схему аксиом N:AA и правило суперпозиции, получаем Fi:AA,xi. Повторяя эти рассуждения для каждого i, в конце концов, выводим ПВ F:AX. Обратное очевидно следует из определения A+.

Сформулируем и докажем теперь теорему о полноте приведённого исчисления.

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

Доказательство. Пусть S – исходная схема и пусть ПВ F:AX не может быть выведено на основании информации о схеме S с помощью правил SR.

Для доказательства теоремы мы должны построить интерпретацию I такую, что в S|I имеются кортежи s и t, для которых |I имеет смысл и которые, совпадая по компонентам A|I, различаются хотя бы по одной компоненте из X|I. Рассмотрим интерпретацию I, такую, что в S|I содержаться два кортежа s и t, компоненты которых совпадают для атрибутов из A+ и различаются для всех прочих атрибутов схемы S. Предположим противное, что ПВ 1 F1:BY является выводимым, но не удовлетворяет S, и определяется это на зафиксированных кортежах. Из предположения следует, что 1 имеет смысл для s и t и что B A+ (в противном случае кортежи не совпали бы по некоторому атрибуту из B). Кроме того, s и t должны различаться по компонентам из Y, т. е. Y A+ (но, вообще говоря, неверно, что YA+=).

Пусть у-атрибут, yY \ A+. Поскольку B A+, то ПВ G:AB выводимо по лемме*. Отсюда, с учётом 1 по правилу суперпозиции имеем G;F1:AY, значит Y A+, а сделанное предположение неверно. Итак, ПВ, выведенные с помощью правил SR, удовлетворяют исходной схеме.

Покажем теперь, что не удовлетворяет S, в частности, при интерпретации I. Предположим обратное. Поскольку A A+, заключаем, что должно выполняться X A+, так как иначе s и t, совпадая по компонентам A|I, не совпадали бы по компонентам X|I. Отсюда опять по лемме* заключаем, что ПВ F:AX может быть выведено по правилам SR. Это противоречит сделанному предположению, а значит, не удовлетворяет схеме S, в частности, на кортежах s и t рассматриваемой интерпретации I. – Таким образом мы показали полноту правил SR.

3.2. Стратегия и алгоритм вывода в классе РДС Известны эффективные стратегии поиска доказательства теоремы (3.1) в классе линейных программ (когда используются только правила (1) и (2) исчисления SR) и в классе ветвящихся программ (с добавлением к двум первым правилам исчисления правила ветвления). При использовании правила введения рекурсии основная трудность связана с определением множеств A и X – аргументов и результатов ПВ из заключения правила (в синтезированной программе применению этого ПВ будет соответствовать вызов построенной рекурсивной процедуры). Определение множеств A и X может сопровождаться достаточно большими временными затратами – в остальном, применение правила введения рекурсии не ухудшает общей оценки сложности предлагаемых алгоритма и стратегии. Дело в том, что вывод для подзадачи, сформулированной во второй строке правила (4), проводится теми же средствами, что и основной вывод теоремы существования, и полностью включается в последний.

3.2.1. Описание алгоритма Предлагаемый алгоритм использует некоторую ограниченную стратегию поиска решения задачи T=(A0,X0,S), что позволяет ему работать с полиномиальными затратами ресурсов по отношению к длине описания РДСмодели M [Новосельцев 1981].

Входной информацией для алгоритма является описание модели M и формулировка задачи T. Доказательство теоремы существования решения (3.1) заключается в последовательном применении правил SR к аксиомам и ранее полученным утверждениям. Аксиомами являются ФС из описания схемы модели M. Поиск доказательства ведётся от данных к целям методом, обратным по отношению к стандартным целеориентированным («прямая волна» – [Новосельцев 1985а]), при этом всё время преследуется цель расширить множество достижимых из данных атрибутов и ослабить условия, при которых показана достижимость 1.

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

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

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

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

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

Ck – множество у-атрибутов исходной схемы, достижимость которых установлена в текущий момент;

по-аксиома – проблемно-ориентированная или предметная аксиома – ФС из (развёртки) исходной схемы;

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

A0 и S берутся из формулировки задачи T.

Описание алгоритма:

«установить i=0, С0=A0»;

«поднять флаг “продолжать доказательство”»;

«текущей схемой объявить S»;

while «поднят флаг “продолжать доказательство”» do if «имеется по-аксиома текущей схемы, аргументы которой входят в Ci» then «применить правило композиции, и, если возможно, правило ветвления»;

«Ci+1: к Ci добавить новые у-атрибуты либо изменить условия «установить i=i+1»; «если определился вход в подсхему, запомнить её»

else if «имеется подсхема, в которую определён вход» then else if «текущая – рекурсивная схема» then «применить правило введения рекурсии; установить i=i+1»;

else «объявить текущей внешнюю схему»

if «текущая – исходная и нет по-аксиом, аргументы которых входят в Ci» then «опустить флаг “продолжать доказательство”» fi Использование специальных структур данных, различные тактики выбора очередной по-аксиомы для использования её в доказательстве позволяют получать весьма эффективные реализации приведённого алгоритма. Подробнее этот вопрос рассматривается ниже.

3.2.2. Корректность алгоритма построения вывода Здесь нас интересует проблема корректности алгоритма. Покажем, что каждый у-атрибут, попавший в некоторое Ci, содержится в A0+ и обратно – каждый элемент A0+ попадает в некоторое Ci.

Теорема 3.3. Приведённый здесь алгоритм корректно вычисляет A0+.

Доказательство.

(i) Индукцией по i покажем, что если некоторый у-атрибут e помещается в Ci, то eA0+.

База индукции (i=0). eA0+, и по схеме аксиом (0) и правилу (1) получаем A0e.

Индукция. Пусть i>0 и Ci состоит из атрибутов, которые принадлежат A0+.

Пусть также на i+1-ом шаге используется ПВ F:BY и eY. BA0+, поскольку BCi, следовательно, по лемме* имеется G:A0B. Используя правила композиции и сужения, получаем G;F:A0e, т. е. e A0+.

(ii) Покажем теперь, что если у-атрибут e входит в A0+, то e попадает в некоторое Ci. Точнее, докажем более общее утверждение: если на основании информации о схеме S по правилам SR выведено ПВ G:A0B, то множество у-атрибутов B содержится в некотором Ci.

Вывод ПВ представляет собой последовательность применений правил SR к по-аксиомам и ранее полученным предложениям вычислимости (начальное ПВ N:A0A0 получается в результате использования схемы аксиом). Доказательство проводим индукцией по длине вывода.

База индукции (минимальная длинна вывода).

Вывод заканчивается применением схемы аксиом – A0 состоит в точности из B, очевидно, BC0. Длинна вывода – два – схема аксиом (0) и правило сужения (1). – Здесь, очевидно, также BC0.

Индукция. Предположим, сделанное утверждение истинно для выводов, длина которых не превосходит k, и пусть вывод ПВ F:AB имеет длину k+1. Если получается по правилу сужения, то B принадлежит Ck, которое найдётся по предположению для вывода, предшествующего получению. Пусть B получено применением правила суперпозиции, например, из полученных ранее 1 F1:AZ и 2 f:Zb (B=Zb).

Вывод каждого из двух последних ПВ имеет длину меньше k+1.

Следовательно по предположению, найдётся такое Ci (im, то он встречается в k - m раз, в противном случае он не встречается в никогда.

Аналогично, мультимножественной суммой двух мультимножеств и называют мультимножество + такое, что если элемент встречается в k раз и в m раз, то тогда он встречается в + k + m раз.

Традиционно в монографиях по математической логике (например, [Мендельсон 1976] или [Барвайс 1983]) под секвенцией понимают структуру вида:, где = A1,..., An, = В1,..., Вm – множества формул. Каждой секвенции стандартным образом сопоставляется формула (так называемый формульный образ секвенции): ИA1...AnВ1...ВmЛ. Эта формула основание говорить о секвенции как о множестве формул.

С другой стороны, для определения секвенции довольно часто используется подход, несколько отличающийся от классического (см., например, [Драгалин 1979], [Воронков 1996] или [Воронков 2000]). Этот подход заключается в следующем: под секвенцией понимают (как и в традиционном случае) структуру вида:, но и здесь не множества, а мультимножества формул. Таким образом, и формульный образ секвенции есть не множество, а мультимножество формул.

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

Секвенцию будем называть подсеквенцией секвенции, если является мультиподмножеством. Пусть дана секвенция = A1,...,An, тогда A1,..., An, аналогично, A1,...,An.

Пусть дана секвенция = A1,...,An. Секвенцию будем называть выполнимой, если существует модель Крипке для всех формул A1,...,An.

Для исчисления секвенций KTseq, которое является секвенциальным вариантом описанной выше дедуктивной системе КТ, в этой работе мы будем использовать традиционные понятия вывода и, соответственно, дерева вывода (см. [Bachmair L. Gansinger H. 2000]). Для устранения разногласий ниже приведены используемые в работе варианты этих определений.

конкретную последовательность применений правила вывода. Под деревом вывода секвенции Ф будем понимать любое дерево, образованное выводами и имеющее Ф своим корнем.

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

4.1.3. Прямое и обратное исчисление секвенций для логики знания Пусть Ф – формула логики KT. Для анализа Ф удобнее использовать не саму систему KT, а эквивалентное ей исчисление секвенций KTseq (см.

[Wallen 1990]). Справедлива следующая теорема (полноты KTseq): Ф невыполнима в KT тогда и только тогда, когда существует опровержение Ф в KTseq. Доказательство теоремы приведено в [Fitting 1983], оттуда же заимствовано и подходящий вариант исчисления секвенций KTseq (здесь p – пропозициональная переменная):

Аксиомы: Г, p, ~p Правила вывода:

Как отмечалось ранее, поиск опровержения мы переносим в инверсное исчисление KTФinv (формулами KTФinv являются все подформулы исходной Ф, что, собственно, и определяет настройку на анализируемую формулу).

Исчисление KTФinv приводится ниже:

Правила вывода:

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

подсеквенциальности, которая позволяет «переносить» найденное в KTseq опровержение Ф в исчисление KTФinv..

Лемма подсеквенциальности. Пусть Ф – формула KT и Г – секвенция, состоящая из подформул Ф и имеющая опровержение в KTseq, тогда существует секвенция такая, что Г и имеет опровержение в KTФinv..

Доказательство. Доказательство ведется индукцией по длине вывода Г в KTseq.

Рассмотрим правило вывода () в KTseq:

опровержение в KTФinv. Необходимо найти секвенцию ` (Г, АВ), имеющую опровержение в KTФinv. В зависимости от того, встречаются ли А и В в, мы получаем три различных случая:

случая имеет вид:

этого случая имеет вид:

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

Итак, правило вывода ( ) в KTseq:

опровержение в KTФinv. Необходимо найти секвенцию ` (Г, А), имеющую опровержение в KTФinv. В зависимости от того, встречается ли А в, мы получаем два различных случая:

1) Пусть А. Мы имеем = (, А), где Г. Вывод для этого случая имеет вид: