Схемы программ с константами


Скачать 49,45 Kb.
PDF просмотр
НазваниеСхемы программ с константами
Русаков Дмитрий Михайлович
Дата конвертации15.08.2012
Размер49,45 Kb.
ТипАвтореферат
СпециальностьДискретная математика и математическая кибернетика
Год2008
Московский государственный университет
имени М. В. Ломоносова
На правах рукописи
Русаков Дмитрий Михайлович
СХЕМЫ ПРОГРАММ С КОНСТАНТАМИ
Специальность 01.01.09 – дискретная математика и
математическая кибернетика
АВТОРЕФЕРАТ
диссертации на соискание учёной степени
кандидата физико-математических наук
Москва – 2008


Работа выполнена на кафедре математической кибернетики факультета вычис-
лительной математики и кибернетики Московского государственного универси-
тета имени М.В. Ломоносова.
Научный руководитель:
доктор физико-математических наук,
профессор
Подловченко Римма Ивановна.
Официальные оппоненты:
доктор физико-математических наук,
профессор
Ломазова Ирина Александровна,
кандидат физико-математических наук,
доцент
Хачатрян Владимир Ервандович.
Ведущая организация:
Институт системного программирования
Российской Академии наук.
Защита состоится 12 декабря 2008 г. в 11.00 на заседании диссертационного со-
вета Д 501.001.44 при Московском государственном университете имени М. В.
Ломоносова по адресу: 119991, ГСП-1, Москва, Ленинские горы, МГУ, 2-й учеб-
ный корпус, факультет ВМиК, аудитория 685.
С диссертацией можно ознакомиться в библиотеке факультета ВМиК МГУ.
С текстом автореферата можно ознакомиться на официальном сайте факульте-
та ВМиК Московского государственного университета имени М. В. Ломоносова
http://www.cs.msu.su в разделе «Наука» – «Работа диссертационных советов» –
«Д 501.001.44».
Автореферат разослан __ ноября 2008 г.
Учёный секретарь
диссертационного совета
профессор
Трифонов Н. П.

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ
Актуальность темы. Диссертационная работа относится к
теории алгебраических моделей программ и посвящена изуче-
нию семантических свойств моделей, именуемых моделями про-
грамм с константами.
В теории программирования изначально модели программ
создавались для исследования различных свойств самих про-
грамм, и главным из них является отношение функциональной
эквивалентности программ. Алгебраические модели программ
введены Р.И. Подловченко в 1981 году как обобщение ранее
известных моделей, объектами которых являются операторные
схемы Ляпунова-Янова, и моделей, называемых дискретными
преобразователями Глушкова-Летичевского. Объекты алгебра-
ических моделей программ называются схемами программ, и
отдельная модель определяется введением отношения эквива-
лентности в множестве схем программ.
Предпринятое обобщение базируется на следующих концеп-
циях:
• отталкиваться от предварительно заданной формализации
понятия программы;
• при переходе от формализованной программы к моделиру-
ющей её схеме сохранять структуру самой программы.
Преследуемая при этом цель состоит в том, чтобы рассмат-
ривать модели программ, обладающие свойством: для них суще-
ствуют аппроксимируемые ими классы формализованных про-
грамм, то есть такие классы, в которых функциональная эк-
вивалентность программ следует из эквивалентности построен-
ных для них схем, принадлежащих модели.
Изложим вкратце, как реализован этот замысел.
Формализованные программы строятся над базисом опера-
торов и логических условий применением всех традиционных
средств композиции операторов, кроме аппарата процедур. Эти
средства реализуются в управляющем графе программы, вер-
шины которого нагружены базисными операторами и логиче-
скими условиями.
3

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

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

ским. Им установлена разрешимость проблемы эквивалентно-
сти в этих моделях, однако факт существования разрешающего
алгоритма не сопровождается его построением. Вместе с тем
ощущается сложность распознавания эквивалентности, ставя-
щая под вопрос практическое использование процедуры распо-
знавания.
Факт разрешимости проблемы эквивалентности в моделях
программ с константами можно извлечь из результатов иссле-
дований моделей вычислений, введённых Л.П. Лисовиком. Од-
нако этот окольный путь не применялся для оценки сложности
распознавания эквивалентности.
Проблема включения вообще не рассматривалась для моде-
лей программ с константами.
Актуальность исследований. Из сделанного нами очерка
исследований в теории алгебраических моделей программ вы-
текает актуальность выявления места, занимаемого моделями
программ с константами среди полугрупповых моделей, для ко-
торых установлена разрешимость проблемы эквивалентности в
модели. Это место определяется оценкой ёмкостной сложности
разрешения проблемы эквивалентности в моделях программ с
константами.
Цель исследований. Цель исследований состоит в следую-
щем: установить разрешимость проблемы включения в произ-
вольной модели программ с константами; найти оценки ёмкост-
ной сложности разрешения проблемы включения, в результате
чего будут получены оценки ёмкостной сложности разрешения
проблемы эквивалентности.
Основные результаты работы и научная новизна. В
диссертации исследованы проблемы включения и эквивалент-
ности в алгебраической модели программ с константами.
Основные результаты данной диссертации следующие:
1. Построен алгоритм разрешения проблемы эквивалентно-
сти в множестве схем программ, принадлежащих произ-
вольной алгебраической модели программ с константами и
6

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

дународной конференции “Дискретные модели в теории управ-
ляющих систем”, (2006, Москва).
Структура и объем работы. Диссертация состоит из вве-
дения, пяти глав, заключения и списка литературы, включаю-
щего 37 наименований. Общий объем диссертации составляет
90 страниц.
8

КРАТКОЕ СОДЕРЖАНИЕ РАБОТЫ
Диссертация имеет следующую структуру. Она состоит из
введения, пяти глав и краткого заключения.
Во введении описывается область исследований, к которой
относится данная работа, и рассматриваемые в ней проблемы.
Первая глава диссертации содержит формальное определе-
ние алгебраической модели программ с константами и проблем
включения и эквивалентности в ней.
Здесь же используется известный ранее результат о сводимо-
сти проблем включения и эквивалентности в рассматриваемых
моделях к одноимённым проблемам в классе унифицированных
схем, принадлежащих модели (лемма 1). Унификация схемы со-
стоит в группировке в одинакового вида фрагменты разбросан-
ных ранее по схеме логических условий.
Далее теоремой 1 устанавливается сводимость проблем вклю-
чения и эквивалентности в множестве унифицированных схем к
одноимённым проблемам в множестве матрично-алгебраических
схем программ. Алгоритм сведения устанавливает взаимно-одно-
значное соответствие между элементами этих множеств.
Пусть M∞ — изучаемая алгебраическая модель программ с
константами.
Во второй главе ставится задача: построить алгоритм, разре-
шающий проблему включения в множестве M1 схем программ,
принадлежащих модели M∞ и таких, в которые любая констан-
та из заданного базиса входит в схему не более одного раза.
Цель решения этой задачи — прощупать методику разреше-
ния проблемы включения в общем случае, то есть для M∞.
Методика получения этого результата следующая. Вначале
устанавливается, что для проверки включения схем в M1 до-
статочно научиться проверять включение в множестве схем про-
грамм без констант и проверять включение областей определе-
ния схем в M1 (теорема 2). Областью определения схемы на-
зывается множество ситуаций, на которых выполнение схемы
завершается.
Далее выявляется, что для проверки включения областей це-
9

лесообразно построить специальные объекты, именуемые нами
диаграммами. В диаграммах учтено следующее обстоятельство:
выполнение схемы из M∞ незавершаемо, если путь его прохо-
дит более одного раза через вершину с константой (утвержде-
ние 2). Диаграмма схемы представляет собой дерево, вершины
которого помечены константами; при этом метки вершин одной
ветви диаграммы не повторяются. Дуги диаграммы помечены
схемами программ без констант. Описан алгоритм построения
по унифицированной схеме из M1 соответствующей ей диаграм-
мы (лемма 3).
Теоремой 3 устанавливается сведение проблем включения и
эквивалентности в множестве схем из M1 к проблеме включе-
ния в множестве диаграмм, соответствующих схемам из M1. В
частности, проблема включения областей определения схем из
M1 сводится к проблеме включения областей определения диа-
грамм. Последняя проблема, в свою очередь, сводится к про-
блеме включения областей определения схем программ без кон-
стант (лемма 4). Решение этой проблемы сводится к проверке
определённых отношений в множестве конечных автоматов, ко-
торые строятся по схемам без констант (теорема 4).
Третья глава посвящена выявлению сложности проблемы
включения в M∞. Теоремой 6 доказано, что эта проблема яв-
ляется PSPACE-полной. Параметром, по которому оценивается
сложность распознавания отношения включения одной схемы в
другую, является общее число вершин с константами в обеих
сравниваемых схемах.
Для доказательства теоремы 6 строится алгоритм, разреша-
ющий проблему включения в модели и использующий для это-
го не более чем полиномиальную память (лемма 6). Этот ал-
горитм для каждой пары ветвей диаграмм сравниваемых схем
использует три конечных автомата. Эти автоматы имитируют
параллельное выполнение схем программ без констант, постро-
енных для каждой дуги ветвей диаграмм; при этом учитывают-
ся константы, соответствующие вершинам ветвей. Задача алго-
ритма состоит в проверке пустоты языков этих автоматов. Про-
10

странства состояний этих автоматов экспоненциальны, поэтому
алгоритм не выполняет их полного построения в памяти. Раз-
работанный алгоритм позволяет проверить пустоту автоматов,
строя их фрагменты “на лету”.
Таким образом устанавливается, что проблема входит в класс
PSPACE.
PSPACE-полнота доказывается сведением известной PSPACE-
полной проблемы — проблемы пересечения языков k конечных
автоматов — к проблеме включения схем в M∞.
Итак, в третьей главе диссертации предложен алгоритм, ре-
шающий проблему включения в M∞ и требующий для сво-
ей работы полиномиальной памяти. Этот алгоритм не приме-
ним в практическом программировании, причиной чего являет-
ся “трюк”, использованный при проверке пустоты языков авто-
матов, пространство состояний которых экспоненциально.
В связи с этим четвёртая глава посвящена построению аль-
тернативного алгоритма, решающего проблему включения в M∞
и применимого на практике. Идеи данного алгоритма развива-
ют идеи алгоритма проверки включения в M1. Теперь их реа-
лизация становится значительно сложнее. Так, если проблема
включения в M1 сводилась к проверкам отношений
G1
G2
и
Dom(G1) ⊆ Dom(G2),
то проблема включения в M∞ сводится к проверке отноше-
нийL0
G1
G2, где L0 = Dom(G3) ∩ Dom(G4) cap · · · ∩ Dom(Gn),
и
Dom(G1) ∩ Dom(G2) ∩ · · · ∩ Dom(Gn−1) ⊆ Dom(Gn).
Здесь G1, G2, . . . , Gn — схемы программ без констант; Dom(G)
L0
— область определения схемы G; а отношение G1
G2 справед-
ливо в том и только том случае, когда выполняется требование:
если схема G1 завершит работу на ситуациях из множества L0,
то на этих ситуациях завершит работу и схема G2, и полученные
ими результаты совпадают.
11

В четвёртой главе дано крупноблочное описание алгоритма,
распознающего включение в M∞, и доказана его корректность
(теорема 8).
В пятой главе детально выписывается сам алгоритм и стро-
ится оценка его сложности по используемой памяти (теорема
9); она выглядит следующим образом:
O(n6k),
где n — общее число вершин в сравниваемых схемах, а k —
общее число вершин с константами в сравниваемых схемах.
В итоге проведёнными исследованиями моделей программ с
константами выявлен её, в известном смысле, пограничный ста-
тус среди полугрупповых моделей программ с установленной
для них разрешимостью проблемы эквивалентности. Примени-
мость на практике алгоритма распознавания эквивалентности
схем программ с константами на грани возможного.
12

ОСНОВНЫЕ РЕЗУЛЬТАТЫ
В диссертации исследованы проблемы включения и эквива-
лентности в алгебраической модели программ с константами.
Основные результаты данной диссертации следующие:
1. Построен алгоритм разрешения проблемы эквивалентно-
сти в множестве схем программ, принадлежащих произ-
вольной алгебраической модели программ с константами и
имеющих не более одного вхождения любой константы в
схему.
2. Впервые рассмотрена проблема включения в произвольной
алгебраической модели программ с константами и доказа-
на её разрешимость. Установлено, что проблема включе-
ния, следовательно, и проблема эквивалентности, в этой
модели являются PSPACE-полными.
3. Построен альтернативный алгоритм, разрешающий пробле-
му включения в алгебраической модели программ с кон-
стантами. Дана оценка его ёмкостной сложности, и этим
установлена оценка ёмкостной сложности алгоритма, ре-
шающего проблему эквивалентности.
В итоге выявлен статус произвольной алгебраической моде-
ли программ с константами среди полугрупповых моделей про-
грамм с установленной для них разрешимостью проблемы эк-
вивалентности. Применимость в практике программирования
алгоритма, распознающего эквивалентность в алгебраической
модели программ с константами, находится на грани возмож-
ного.
13

ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ
[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
14

// В сборнике “Труды института системного программирова-
ния”.— М.: Институт Системного Программирования РАН,
2006.— Т. 11.— С. 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.
15


Разместите кнопку на своём сайте:
поделись


База данных защищена авторским правом ©dis.podelise.ru 2012
обратиться к администрации
АвтоРефераты
Главная страница