Введение к работе
АКТУАЛЬНОСТЬ ТЕШ. Работа посвящена исследованию некоторых вопросов, связанных о дедуктивним синтезом алгоритмов. Под дедуктивным синтезом да понимаем создание алгоритмов с помощью построения конструктивных доказательств осуществимости объектов, вычисляемых этими алгоритмами. В широком смысле конструктивными считается доказательства, обосновывавшие существование объектов путем явного указания па способы их построения. Благодаря этой особенности, конструктивное доказательство существования объекта, в суаности, содержит алгоритм его вычисления. Такої! подход основан на теоретических работах, берущих начало от реализационной семантики Рейтинга - Колмогорова - Клини -Геделя (1,2,3,4] и продолжающихся многочисленными современными публикациями (см., например, [5,6,7,8]).
Для любой практической реализации этого подхода, допускающей автоматизации какой-либо части процесса построения алгоритмов, необходимо, во-первых, выбрать формальный язык для записи предлогеннй о существовании объектов, которые требуется вычислять (т.е. язык формулировок теорем), во-вторых, зафиксировать способ интерпретации предложений этого языка, при котором предложениям о существовании объектов соответствуют алгоритмы их построения, в-третьих, построить формальную систему для доказательства таких предложений, в-четвертых, показать, что эта система корректна, т.е. соответствует выбранному способу интерпретации предпокений. Корректность означает, что для каждой доказанного
существования можно построить алгоритм (программу) вычисления существующего объекте Корректность должна быть обоснована также конструкт зно. Это значит, что это обоснование должно содержать алгоритм построения упомянутых программ по доказательствам.
В некоторых случаях выбранная формальная теория настолько проста, что удается построить алгоритм, выводящий доказательство любого ее истинного предложения. В других случаях такой алгоритм невозможен. ' Последнее означает, что некоторые, доказательства необходимо, строить с творческой помощью человека, или необходимо сузить класс задач для решения. .
К частичным практическим реализациям этого подхода можно, согласно работам Г.Е.Минца и Э.Х.Тыугу [9], отнести такие системы, как ПРИЗ, разработанную под руководством Э.Х.Тыугу {10], СПОРА, разработанную под руководством С.С. Лаврова [11], СПРУТ [12], САТУРН [13]. В этих системах используются очень простые теории, что за счет сужения класса решаемых задач позволяет получить высокую степень автоматизации построения алгоритмов.
Можно отметить отличительную особенность всех упомянутых работ - невозможность задания ограничений на объем вычислительных ресурсов, используемых синтезируемыми алгоритмами. При практичэской реализации в сложных случаях эта особенности., является недостатком: в таких системах могут синтезироваться алгоритмы, выполнение которых затруднено или нетвозмої-'Ю вследствие слииком большой их потребности в ' «.^числительных ресурсах. В настоящей работе преодолевается
этот недостаток - предлагаются теории, в которых можно задать ограничения на объем вычислительных ресурсов.
В основном, в работе строятся подходящие дедуктинние системы для синтеза различных классов алгоритмов. При этом главное вншхание уделено не исследованной другими авторами возможности ограниченния объемов вычислительных ресурсов, Используемых этими алгоритмами . Как правило, это - время С"процессорное") выполнения алгоритмов. Таким образом, направление, к которому относятся основные результаты данной работы, можно охарактеризовать названием "дедуктивная теория сложности алгоритмов".
Актуальность разрабатываемого направления определяется тем, что оно позволяет соединить оценки сложности вычислений н автоматизации порождения компьютерных программ дедуктивными средствами.
ЦЕЛЬ РАБОТЫ - создание формальных теорий, на ' основе которых можно строить системы дедуктивного синтеза программ для различных классов предметных областей, различных стилей программирования, для баз данных, учитывавши расход в процессе вычисления различных вычислительных ресурсов, таких как время вычисления.
ОБЩАЯ МЕТОДИКА ВЫПОЛНЕНИЯ ИССЛЕДОВАНИЙ. В работе используются методы теории формальных систем и методы алгоритмической теории сложности. Для объединения этих методов предложено новое понятие реализационной семантики формул на основе понятия вычислительной среды.
НАУЧНАЯ НОВИЗНА. В работе содержится ряд существенно новых результатов. Построены формальные теории,
- Є -
предназначенные для дедуктивного синтеза алгоритмов с учетом в постановках задач расходуемых вычислительных ресурсов, таких, как процессорное время вычисления. Некоторые из теорий учитывают изначальную ограниченность времени, доступного для вичисленім независимо от того, указано ли это в постановке задачи. Кроме этих общих теорий, построены подобные специализированные теории для синтеза программ с абстрактными типаии данных, синтеза программ анализа текстов и списков древовидной структуры. Построены методы и теории дедуктивного синтеза запросов в базах данных как с учетом эффективности запроса; так и для синтеза ЕСТЕСТВЕННЫХ запросов по их неполным . спецификациям с использованием релевантных конструктивных логик. Исследованы свойства реализационной полноты и непротиворечивости основных теорий. Доказаны теоремы о содержательной непротиворечивости всех теорий по отношению к приводимым для них реализационным семантикам и теоремы о содержательной полноте по отношению к этим семантикам для наиболее простых теорий. Даны некоторые сложностныэ оценки для распознавания выводимости в теории дедуктивного синтеза запросов в базах данных.
ПРАКТИЧЕСКАЯ ЦЕННОСТЬ. Хотя данная работа носит теоретический характер, ее результаты могут быть использованы при построении практических систем дедуктивного , синтеза программ. На практике полученные результаты, относящиеся к области баз данных были применены при построении системы управления базами данных, разработанной автором для государственного предприятия "Боткинский завод".
АПРОБАЦИЯ РАБОТЫ. Результаты работы докладывались на семинарах по алгоритмической теории сложности Петербургского отделения Математического института РАН, Всесоюзных и Межреспубликанской конференциях по матеыатическо логике, теоретической кибернетике, синтезу, верификации и отладке nporpat-tM, Всесоганом семинаре по оптимизации и преобразованиям программ и др.
ПУБЛИКАЦИИ. По теме диссертации опубликовано 15 работ, которые OTpasaDT ее основное содержание.
СТРУКТУРА И ОБЪЕМ РАБОТЫ. Диссертация состоит из введения, трех глаз, разбитых на 6 параграфов, заключения и списка использованной литературы. Объем работы - 130 стр., вкличая 11 страниц списка использованной литератури, насчитывающего 94 наименовании.
