Схемы программ с константами тема автореферата и диссертации по математике, 01.01.09 ВАК РФ

, Московский государственный университет

имени М. В. Ломоносова

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

Русаков Дмитрий Михайлович

СХЕМЫ ПРОГРАММ С КОНСТАНТАМИ

Специальность 01.01.09 - дискретная математика и математическая кибернетика

АВТОРЕФЕРАТ диссертации на соискание учёной степени кандидата физико-математических наук

РОУЧЭЧ'---

Москва - 2008

003454069

Работа выполнена на кафедре математической кибернетики факультета вычислительной математики и кибернетики Московского государственного университета имени М.В Ломоносова

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

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

Подловченко Римма Ивановна

Официальные оппоненты

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

Ломазова Ирина Александровна,

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

Хачатрян Владимир Ервандович.

Ведущая организация.

Институт системного программирования Российской Академии наук.

Защита состоится 12 декабря 2008 г. в 11.00 на заседании диссертационного совета Д 501.001.44 при Московском государственном университете имени М. В. Ломоносова по адресу 119991, ГСП-1, Москва, Ленинские горы, МГУ, 2-й учебный корпус, факультет ВМиК, аудитория 685.

С диссертацией можно ознакомиться в библиотеке факультета ВМиК МГУ.

С текстом автореферата можно ознакомиться на официальном сайте факультета ВМиК Московского государственного университета имени М. В Ломоносова Шр7/чдг'№-и'.с5 т.чи ей в разделе «Наука» - «Работа диссертационных советов» -

«Д 501 001.44.

Автореферат разослан__ноября 2008 г.

Ученый секретарь диссертационного совета профессор

Трифонов Н. П.

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

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

В теории программирования изначально модели программ создавались для исследования различных свойств самих программ. и главным из них является отношение функциональной эквивалентности программ. Алгебраические модели программ введены Р.И. Подловченко в 1981 году как обобщение ранее известных моделей, объектами которых являются операторные схемы Ляпунова-Янова, и моделей, называемых дискретными преобразователями Глушкова-Летичевского. Объекты алгебраических моделей программ называются схемами программ, и отдельная модель определяется введением отношения эквивалентности в множестве схем программ.

Предпринятое обобщение базируется на следующих концепциях:

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

• при переходе от формализованной программы к моделирующей её схеме сохранять структуру самой программы.

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

Изложим вкратце, как реализован этот замысел.

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

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

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

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

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

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

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

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

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

Модели программ с константами изучались A.A. Летичев-

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

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

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

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

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

Основные результаты работы и научная новизна. В

диссертации исследованы проблемы включения и эквивалентности в алгебраической модели программ с константами.

Основные результаты данной диссертации следующие:

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

имеющих не более одного вхождения любой константы в схему.

2. Впервые рассмотрена проблема включения в произвольной алгебраической модели программ с константами и доказана её разрешимость. Установлено, что проблема включения, следовательно, и проблема эквивалентности, в этой модели являются PSPACE-полными.

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

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

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

Апробация работы. Представленные в диссертации результаты докладывались на семинаре факультета ВМиК МГУ по теоретическим вопросам программирования под руководством профессора Р.И. Подловченко и доцента В.А. Захарова, на V-й международной конференции ''Дискретные модели в теории управляющих систем" (2003, Москва), на VI-й международной конференции "Дискретные модели в теории управляющих систем" (2004, Москва), на всероссийской конференции студентов, аспирантов и молодых учёных "Технологии Microsoft в теории и практике программирования'', (2005, Москва), на VII-й меж-

дународной конференции "Дискретные модели в теории управляющих систем", (2006, Москва).

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

КРАТКОЕ СОДЕРЖАНИЕ РАБОТЫ

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

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

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

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

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

Пусть Мао — изучаемая алгебраическая модель программ с константами.

Во второй главе ставится задача: построить алгоритм, разрешающий проблему включения в множестве М.\ схем программ, принадлежащих модели Л4Х и таких, в которые любая константа из заданного базиса входит в схему не более одного раза.

Цель решения этой задачи — прощупать методику разрешения проблемы включения в общем случае, то есть для М.^.

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

Далее выявляется, что для проверки включения областей це-

лесообразно построить специальные объекты, именуемые нами диаграммами. В диаграммах учтено следующее обстоятельство: выполнение схемы из М.^ незавершаемо, если путь его проходит более одного раза через вершину с константой (утверждение 2). Диаграмма схемы представляет собой дерево, вершины которого помечены константами: при этом метки вершин одной ветви диаграммы не повторяются. Дуги диаграммы помечены схемами программ без констант. Описан алгоритм построения по унифицированной схеме из Л4] соответствующей ей диаграммы (лемма 3).

Теоремой 3 устанавливается сведение проблем включения и эквивалентности в множестве схем из М.\ к проблеме включения в множестве диаграмм, соответствующих схемам из М.\. В частности, проблема включения областей определения схем из М\ сводится к проблеме включения областей определения диаграмм. Последняя проблема, в свою очередь, сводится к проблеме включения областей определения схем программ без констант (лемма 4). Решение этой проблемы сводится к проверке определённых отношений в множестве конечных автоматов, которые строятся ио схемам без констант (теорема 4).

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

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

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

Таким образом устанавливается, что проблема входит в класс PSPACE.

PSPACE-полнота доказывается сведением известной PSPACE-полной проблемы — проблемы пересечения языков /с конечных автоматов к проблеме включения схем в .Моо

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

В связи с этим четвёртая глава посвящена построению альтернативного алгоритма, решающего проблему включения в М« и применимого на практике. Идеи данного алгоритма развивают идеи алгоритма проверки включения в .Mi- Теперь пх реализация становится значительно сложнее. Так, если проблема включения в yVii сводилась к проверкам отношений Gx и

Dom(G 1) С Dom(G2),

то проблема включения в Л4.х сводится к проверке отношений

Со

G1 С С2, гДе А) = DomiG-i) П Dom{Gi) cap ■ • ■ П Dom(Gn), и

Dom(Gi) П Dom(G2) П • • • П Dom{GnС Dom(Gn).

Здесь G\, G-2, ...,(?„ — схемы программ без констант; Dom(G)

Со

область определения схемы G: а отношение Gi С G2 справедливо в том и только том случае, когда выполняется требование: если схема G\ завершит работу на ситуациях из множества С0, то на этих ситуациях завершит работу и схема 6'2, и полученные ими результаты совпадают.

В четвёртой главе дано крупноблочное описание алгоритма, распознающего включение в и доказана его корректность (теорема 8).

В пятой главе детально выписывается сам алгоритм и строится оценка его сложности по используемой памяти (теорема 9); она выглядит следующим образом:

0(п6к),

где п — общее число вершин в сравниваемых схемах, а, к — общее число вершин с константами в сравниваемых схемах.

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

ОСНОВНЫЕ РЕЗУЛЬТАТЫ

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

Основные результаты данной диссертации следующие:

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

2. Впервые рассмотрена проблема включения в произвольной алгебраической модели программ с константами и доказана её разрешимость. Установлено, что проблема включения, следовательно, и проблема эквивалентности, в этой модели являются РЭРАСЕ-полными.

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

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

ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

[1] Подловченко Р. И., Русаков Д. М. Каноническая форма схемы программ с однократным вхождением константы // Труды V международной конференции "Дискретные модели в теории управляющих систем" (Ратмино 26-29 мая 2003).- М.: изд. отдел ф-та ВМиК МГУ, 2003 - С. 65-66.

[2] Подловченко Р. И., Русаков Д. М. О проблеме включения для схем программ с константами // Труды VI международной конференции "Дискретные модели в теории управляющих систем" (Москва. 7-11 декабря 2004).— М.: изд. отдел ф-та ВМиК МГУ, 2004,- С. 137-140.

[3] Подловченко Р. И., Русаков Д. М. Схемы программ с константами // Программирование.— 2005.— № 3.— С. 5-18.

[4] Подловченко Р. И., Русаков Д. М. Проблема включения в алгебраической модели программ с константами // Программирование.- 2007.- № 3.- С. 3-15.

[5] Русаков Д. М. О проблеме эквивалентности схем программ с константами // Сборник тезисов лучших дипломных работ 2004 года,- М.: изд. отдел ф-та ВМиК МГУ, 2004.- С. 61-63.

[6] Русаков Д. М. О проблеме включения для схем программ с константами // Технологии Microsoft в теории и практике программирования.— 2005.— С. 134.

[7] Русаков Д. М. Проблема эквивалентности схем программ с константами // Труды VII международной конференции "Дискретные модели в теории управляющих систем" (Петровское, 4-6 марта 2006 г.).- М.: МАКС Пресс, 2006.- С. 309-314.

[8] Русаков Д. М. Алгоритм проверки включения схем в алгебраической модели программ с константами // Программирование,- 2007.- № 5.- С. 3-13.

[9] Podlovchenko R., Rusakov D., Zakharov V. The equivalence problem for programs with mode switching is PSPACEcomplete

//В сборнике "Труды института системного программирования". М.: Институт Системного Программирования РАН, 2006.- Т. П.- С. 109-128.

[10] Podlovchenko R., Rusakov D., Zakharov V. On the equivalence problem for programs with mode switching // Lecture Notes in Computer Science.- 2006.- Vol. 3845,- Pp. 351-352.

и

Автореферат

Дмитрий Михайлович РУСАКОВ СХЕМЫ ПРОГРАММ С КОНСТАНТАМИ

Подписано в печать 07.11.2008 Форматб0х84 1/16. Усл. печ. л. 1.0. Тираж 100 экз. Зак. № 199

Отпечатано в ООО «Типография «Славянская лавка» Г. Москва, Переведеновский пер., д. 18 Тел.: (495) 645-79-32 E-mail: tipograf-sl@mail.ru

Страница

Введение

ГЛАВА 1. Алгебраическая модель программ с константами 13 »

1.1. Алгебраические модели программ.

1.2. Матрично-алгебраические модели программ

1.3. Модель программ с константами.

ГЛАВА 2. Подкласс схем с однократным вхождением константы

2.1. Критерий включения в классе ЛЛ\.

2.2. От схем программ к диаграммам.

2.3. Проблема включения области определения для диаграмм из Diag и проблема включения в Л4\

2.4. Решение задач 1-3.

ГЛАВА 3. Сложность проблемы включения

3.1. Каркас схемы.

3.2. Алгоритм проверки включения схем.

3.3. Сложность проблемы включения.

ГЛАВА 4. Концепция альтернативного алгоритма проверки включения

4.1. От схем программ с константами — к диаграммам.

4.2. Задачи для схем программ без констант.

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

4.4. Методика проверки требования 2) леммы 7.

ГЛАВА 5. Альтернативный алгоритм проверки включения в 9Яоо

5.1. Алгоритм включения диаграмм.

5.2. Использование конечных автоматов для проверки отношений над схемами программ без констант.

5.3. Алгоритмы над автоматами.

5.4. Оценка сложности.

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

В теории программирования изначально модели программ создавались для исследования различных свойств самих программ, и главным из них является отношение функциональной эквивалентности программ [4]. Алгебраические модели программ [15, 17] введены Р.И. Подловченко в 1981 году как обобщение ранее известных моделей, объектами которых являются операторные схемы Ляпунова-Янова [14, 32], и моделей, называемых дискретными преобразователями Глушкова-Летичевского [1, 7, 8, 9]. Объекты алгебраических моделей программ называются схемами программ, и отдельная модель определяется введением отношения эквивалентности в множестве схем программ.

Предпринятое обобщение базируется на следующих концепциях:

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

• при переходе от формализованной программы к моделирующей её схеме сохранять структуру самой программы.

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

Изложим вкратце, как реализован этот замысел.

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

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

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

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

В теории алгебраических моделей программ найден достаточный признак того, что модель является аппроксимирующей [19], и изучаются только аппроксимирующие модели. Установлено, что среди них имеются как модели с разрешимой проблемой эквивалентности [21, 22], так и модели с неразрешимой проблемой эквивалентности. При обращении к проблеме включения обнаружен факт существования моделей с неразрешимой проблемой включения, но с разрешимой проблемой эквивалентности.

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

Для многих полугрупповых моделей, удовлетворяющих требованию: определяющие их полугруппы не обладают циклами, найдены приемлемые по сложности алгоритмы распознавания в них проблемы эквивалентности [23, 21, 22]. Подверглись рассмотрению и полугрупповые модели, для которых полугруппа имеет циклы. Они имеют следующий тип: среди базисных операторных символов имеются символы, названные константами, и две операторные цепочки полагаются эквивалентными в одном из двух случаев: либо обе не содержат вхождений констант и полностью совпадают, либо обе имеют вхождения констант, и тогда совпадают хвосты цепочек, начинающиеся последним вхождением константы. Такие модели названы нами моделями программ с константами.

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

Модели программ с константами изучались А. А. Летичевским [6, 10]. Им установлена разрешимость проблемы эквивалентности в этих моделях, однако факт существования разрешающего алгоритма не сопровождается его построением. Вместе с тем ощущается сложность распознавания эквивалентности, ставящая под вопрос практическое использование процедуры распознавания.

Факт разрешимости проблемы эквивалентности в модели программ с константами можно извлечь из результатов исследований моделей вычислений, введённых Л.П. Лисовиком [13, 11, 12]. Однако этот окольный путь не применялся для оценки сложности распознавания эквивалентности.

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

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

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

Диссертация имеет следующую структуру.

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

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

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

Пусть Adoo ~ изучаемая алгебраическая модель программ с константами.

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

Цель решения этой задачи — прощупать методику разрешения проблемы включения в общем случае, то есть для М.^.

Методика получения этого результата следующая. Вначале устанавливается, что для проверки включения схем в A4i достаточно научиться проверять включение в множестве схем программ без констант и проверять включение областей определения схем в Л4\ (теорема 2). Областью определения схемы называется множество ситуаций, на которых выполнение схемы завершается.

Далее выявляется, что для проверки включения областей целесообразно построить специальные объекты, именуемые нами диаграммами. В диаграммах учтено следующее обстоятельство: выполнение схемы из АЛ^ неза-вершаемо, если путь его проходит более одного раза через вершину с константой (утверждение 2). Диаграмма схемы представляет собой дерево с вершинами-константами, каждая ветвь которого не несёт повторяющихся вершин-констант. Дуги диаграммы помечены схемами программ без констант. Описан алгоритм построения по унифицированной схеме из ЛЛ\ соответствующей ей диаграммы (лемма 3).

Теоремой 3 устанавливается сведение проблем включения и эквивалентности в множестве схем из М,\ к проблеме включения в множестве диаграмм, соответствующих схемам из В частности, проблема включения областей определения схем из Л41 сводится к проблеме включения областей определения диаграмм. Последняя проблема, в свою очередь, сводится к проблеме включения областей определения схем без констант (лемма 4). Решение этой проблемы сводится к установлению определённых отношений в множестве конечных автоматов, которые строятся по схемам (теорема 4).

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

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

Таким образом устанавливается, что проблема входит в класс PSPACE. PSPACE-полнота доказывается сведением известной PSPACE-полной проблеи мы — проблемы пересечения языков к конечных автоматов — к проблеме включения схем ъ ЛЛ^.

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

В связи с этим четвёртая глава посвящена построению альтернативного алгоритма, решающего проблему включения в АЛоо и применимого на практике. Идеи данного алгоритма развивают идеи алгоритма проверки включения в М.\. Теперь их реализация становится значительно сложнее. Так, если проблема включения в сводилась к проверкам отношений

• Gi С G2 и

• Dom(Gi) С Dom{G2), то проблема включения в Л4оо сводится к проверке отношений

• Gi □ С?2, где Cq = Dom{Gz) П Dom{G<i) cap. П Dorn{Gn), и

• Dom(Gi) П Dom(G2) П . П Dom(Gn-1) С Dom{Gn).

Здесь G\, G2, • ■ ■ 5 Gn — схемы программ без констант; Dom(G) — область определения схемы G\ а отношение G\ С G2 справедливо в том и только том случае, когда выполняется требование: если схема G\ останавливается на начальных данных /л из £q, то на fi останавливается и G2, и результаты их выполнения совпадают.

В четвёртой главе дано крупноблочное описание алгоритма, распознающего включение в Л^оо, и доказана его корректность.

В пятой главе детально выписывается сам алгоритм и строится оценка его сложности по используемой памяти (теорема 9); она выглядит следующим образом:

0(n6fc), где п — общее число вершин в сравниваемых схемах, а к — общее число вершин с константами в сравниваемых схемах.

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

Основные результаты данной диссертации следующие:

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

2. Доказана разрешимость проблемы включения в алгебраической модели программ с константами. Установлено, что проблема включения, а следовательно, и проблема эквивалентности, в этой модели являются PSPACE-полными.

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

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

ЗАКЛЮЧЕНИЕ

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

1. Глушков В. М., Летичевский А. А. Теория дискретных преобразователей // Избранные вопросы алгебры и логики.— 1973.— С. 5-39.

2. Касьянов В. Н., Евстигнеев В. А. Графы в программировании: обработка, визуализация и применение. — БХВ-Петербург, 2003.

3. Корман Т., Лейзерсон Ч., Ривсст Р., Штайн К. Алгоритмы: построение и анализ. Второе издание. — Вильяме, 2005.

4. Котов В. Е., Сабельфельд В. К. Теория схем программ, — М.: Наука, 1991.- 248 с.

5. Кудрявцев В. В., Алёшин С. В., Подколзин А. С. Введение в теорию автоматов. — М.: Наука, 1985.— 320 с.

6. Летичевский А. А. Эквивалентность автоматов с заключительным состоянием относительно свободной полугруппы с правым нулём // Доклады Академии наук СССР. 1968. - Т. 182, № 5. - С. 1007-1009.

7. Летичевский А. А. Функциональная эквивалентность дискретных преобразователей I // Кибернетика. — 1969.— № 2.— С. 5-15.

8. Летичевский А. А. Функциональная эквивалентность дискретных преобразователей II // Кибернетика. — 1970.— № 2.— С. 14-28.

9. Летичевский А. А. Практические методы распознавания эквивалентности дискретных преобразователей и схем программ // Кибернетика. — 1973. № 4. - С. 15-26.

10. Летичевский А. А. Эквивалентность автоматов относительно полугрупп с сокращением // Проблемы кибернетики. Вып. 27. — М.: Наука, 1973. — С. 195-212.

11. Лисовик Л. П. О конечных преобразователях над размеченными деревьями и квазитождествах в свободной полугруппе // Проблемы кибернетики. Вып. 40.- 1983.-С. 19-42.

12. Лисовик Л. П. Металинейные схемы с засылками констант // Программирование. — 1985. — № 2. — С. 29-38.

13. Лисовик Л. П. Схемы программ и преобразователи над размеченными деревьями // Математические вопросы кибернетики. Вып. 6.— М.: Наука, 1996.- С. 281-320.

14. Ляпунов А. А. О логических схемах программ // Проблемы кибернетики. Вып. 1, — М.: Физматгиз, 1958.— С. 46-74.

15. Подловченко Р. И. Полугрупповые модели программ // Программирование. 1993. - № 4. - С. 3-13.

16. Подловченко Р. И. Специальные перегородчато-автоматные модели рекурсивных программ // Программирование. — 1994. — № 4. — С. 3-26.

17. Подловченко P. PL От схем Янова к теории моделей программ // Математические вопросы кибернетики. Вып. 7. — М.: Наука, 1998. — С. 281-302.

18. Подловченко Р. И. Об одном массовом решении проблемы эквивалентных преобразований схем программ I. // Программирование. — 2000. — № 1. — С. 64-77.

19. Подловченко Р. И. Эквивалентные преобразования схем программ для "запутывания" самих программ // Программирование. — 2002,— № 2.— С. 66-80.

20. Подловченко Р. П., Аланакян П. А. Регулярные модели программ // Программирование. — 1993. — № 4. — С. 3-11.

21. Подловченко Р. И., Захаров В. А. Быстрые алгоритмы распознавания эквивалентности в моделях программ с коммутирующими операторами // В сборнике "Компьютерные аспекты в научных исследованиях и учебном процессе", М.: Изд-во МГУ, 1996,- С. 3-8.

22. Подловченко Р. И., Захаров В. А. Полиномиальный по сложности алгоритм, распознающий коммутативную эквивалентность схем программ // Доклады РАН. М.: Изд-во МГУ, 1998. - Т. 362, № 6. - С. 744-747.

23. Подловченко Р. И., Русаков Д. М. О проблеме включения для схем программ с константами // Труды VI международной конференции "Дискретные модели в теории управляющих систем" (Москва, 7-11 декабря 2004).- М.: изд. отдел ф-та ВМиК МГУ, 2004. С. 137-140.

24. Подловченко Р. И., Русаков Д. М. Схемы программ с константами // Программирование. — 2005. — № 3. — С. 5-18.

25. Подловченко Р. П., Русаков Д. М. Проблема включения в алгебраической модели программ с константами // Программирование. — 2007. — № 3. — С. 3-15.

26. Русаков Д. М. О проблеме эквивалентности схем программ с константами // Сборник тезисов лучших дипломных работ 2004 года. — М.: изд. отдел ф-та ВМиК МГУ, 2004.- С. 61-63.

27. Русаков Д. М. О проблеме включения для схем программ с константами // Технологии Microsoft в теории и практике программироания. — 2005,- С. 134.

28. Русаков Д. М. Проблема эквивалентности схем программ с константами // Труды VII международной конференции "Дискретные модели в теории управляющих систем" (Петровское, 4-6 марта 2006 г.). — М.: МАКС Пресс, 2006. С. 309-314.

29. Русаков Д. М. Алгоритм проверки включения схем в алгебраической модели программ с константами // Программирование. — 2007. — № 5. — С. 3-13.

30. Янов Ю. И. О логических схемах алгоритмов // Проблемы кибернетики. Вып. 1.-М.: Физматгиз, 1958. С. 75-127.

31. Hopcroft J. Е., Motwani R., Ullman J. D. Introduction to Automata Theory, Languages and Computation. — Addison-Wesley, 2001.

32. Podlovchenko R., Rusakov D., Zakharov V. The equivalence problem for programs with mode switching is PSPACE-complete // В сборнике "Труды института системного программирования".— М.: Институт Системного Программирования РАН, 2006. —Т. 11.—С. 109-128.

33. Podlovchenko R., Rusakov D., Zakharov V. On the equivalence problem for programs with mode switching // Lecture Notes in Computer Science. — 2006. Vol. 3845. - Pp. 351-352.

34. Savitch W. J. Relationships between nondeterministic and deterministic space complexities // Journal of Computer and System Science. — 1970. — Vol. 4, no. 2. Pp. 177-192.

35. Valiant L. G. The equivalence problem for deterministic finite-turn pushdown automata // Information and Control.— 1974. — Vol. 25.— Pp. 123-133.