- ТЕОРЕТИЧЕСКИЕ ВОПРОСЫ ПРОГРАММИРОВАНИЯ ~
УДК 519.6
ОБ ОДНОМ КЛАССЕ АЛГЕБРАИЧЕСКИХ МОДЕЛЕЙ ПРОГРАММ, ПРЕДСТАВЛЯЮЩЕМ ПРАКТИЧЕСКИЙ
ИНТЕРЕС
© 2013 г. Р.И. Подловченко
Научно-исследовательский вычислительный центр МГУ 119991 Москва, Ленинские горы,дом 1, стр. 4 E-mail: rip@vvv.srcc.msu.ru Поступила в редакцию 25.08.2012
Алгебраические модели программ предназначены для исследования семантических свойств программ на их моделях - схемах программ. В статье изложены концепции их построения, и рассмотрен класс моделей, аппроксимирующих реальные последовательные программы. Построены алгоритмы, распознающие эквивалентность схем программ в моделях данного класса с приемлемой на практике сложностью. Установлена пригодность этих алгоритмов для построения эквивалентных преобразований схем программ.
1. ВВЕДЕНИЕ
Алгебраические модели программ введены в [1] для решения глобальной задачи в теории схем программ - разрабатывать на схемах программ эквивалентные преобразования самих программ.
Характерными особенностями алгебраических моделей программ являются следующие:
• их введению предшествует формализация программ, в которой программа, по существу, совпадает с разделом операторов в реальных программах, записанных на императивном алгоритмическом языке программирования;
берется совпадающей с формализованной программой; это обеспечивает ситуацию: всякое структурное преобразование схемы программы одновременно является структурным преобразованием программы, для которой построена эта схема;
•
шение их эквивалентности, и так образуется
отдельная модель программ; поскольку отношения эквивалентности составляют параметрическое множество, возникает множество моделей программ; все они используют одно и то же множество схем программ и отличаются друг от друга только их эквивалентностью;
•
что подлежат изучению, осуществляется на основе определения аппроксимирующей модели; так называется модель, для которой существует класс формализованных программ, отвечающий требованию: из эквивалентности схем программ, принадлежащих рассматриваемой модели, следует функциональная эквивалентность программ, принадлежащих данному классу и совпадающих по структуре с этими схемами; таким образом, всякое эквивалентное преобразование схем из аппроксимирующей модели является эквивалентным преобразованием соответствующих им программ из аппроксимируемого класса программ; принимается решение - изучать только аппроксимирующие модели;
метры модели, строится множество заведомо аппроксимирующих моделей, и рассматриваются модели, ему принадлежащие.
В проблематике теории алгебраических моделей программ основной является проблема эквивалентных преобразований (э.п.) в модели; она состоит в построении системы э.п. схем из рассматриваемой модели, обладающей свойством: существует алгоритм, который, получив на свой вход две эквивалентные схемы из этой модели, строит конечную цепочку э.п., принадлежащих данной системе, трансформирующую первую схему во вторую; описанная система э.п. называется полной в рассматриваемой модели. Актуальность проблемы э.п. очевидна: система э.п. схем, полная в аппроксимирующей модели, является самой богатой среди систем э.п., разрабатываемых в данной модели для аппроксимируемого ею класса программ.
Для разработки полной системы э.п. предварительно должна быть решена проблема эквивалентности схем программ в рассматриваемой модели, т.е. построен алгоритм, который, получив на свой вход две произвольные схемы программ из этой модели, устанавливает, эквивалентны они в ней или нет.
Так на центральное место в проблематике теории алгебраических моделей выходит проблема эквивалентности.
Заметим, что ее решение в аппроксимирующей модели программ используется и для частичного разрешения эквивалентности программ в аппроксимируемом ей классе.
Из сказанного следует, что результаты, полученные для обеих проблем в алгебраической модели программ, можно использовать в практике программирования. И вот тут возникает задача: выделить модели, для которых сложность разрешения в них проблемы эквивалентности позволяет использовать эти результаты. В теории схем программ принято считать, что приемлемым для практического использования является алгоритм, разрешающий эквивалентность схем с полиномиальной сложностью относительно размеров схем, поступивших на его вход, и при этом степень полинома не превышает числа три.
Исходя из этого, рассматриваемые в данной статье алгебраические модели программ
представляют практический интерес, поскольку сложность алгоритмов, разрешающих в них проблему эквивалентности, является действительно приемлемой.
Рассматриваемые модели именуются частично коммутативными и представляют собой подкласс так называемых уравновешенных полугрупповых моделей с левым сокращением. Для последних в [2] решена проблема эквивалентности, а в [3] - проблема э.п. Однако сложность решения проблемы эквивалентности экспоненциальна, что и заставило обратиться к данному подклассу моделей.
В статье исследуются те подмодели частично коммутативных моделей, которые состоят из схем программ специальной структуры: эти схемы называются матричными. Обоснованием этому служат следующие факты, установленные в [2]: для произвольной схемы можно построить матричную схему, которая будет эквивалентна ей в любой алгебраической модели программ; алгоритм, осуществляющий это построение, имеет приемлемую полиномиальную сложность относительно размера исходной схемы.
Статья, помимо введения, состоит из четырех разделов и приложения.
В разделе 2 описываются частично коммутативные подмодели программ, и это делается без обращения к самой модели, что упрощает изложение статьи. Введенные подмодели классифицируются на свободные, транзитивно коммутативные и нетранзитивно коммутативные.
Раздел 3 посвящен описанию ряда семантических свойств, присущих схемам программ в частично коммутативной подмодели. Часть свойств формулируется со ссылкой на работы, где они установлены; вместе с тем, леммаии 3 и 4 доказываются два новых свойства, являющиеся необходимыми для эквивалентных схем именно в частично коммутативной подмодели.
В разделе 4 излагаются алгоритмы, разрешающие эквивалентность схем по отдельности в свободной подмодели, транзитивно коммутативной подмодели и нетранзитивно коммутативной подмодели. Для каждого алгоритма дана оценка его сложности.
В разделе 5 обсуждается проблема э.п. в частично коммутативной подмодели. Кратко излагается метод, которым она решена в уравнове-
шенной полугрупповой модели программ с левым сокращением. Устанавливается, что построенные в разделе 4 алгоритмы дают необходимую информацию для использования этого решения.
Наконец, приложение посвящено демонстрации на примере конкретной формализации программ того, каковы условия, выполнение которых достаточно для утверждения: алгебраические модели программ, аппроксимирующие классы этих программ, являются частично коммутативными.
2. ЧАСТИЧНО КОММУТАТИВНАЯ ПОДМОДЕЛЬ ПРОГРАММ
Как было отмечено во введении, проблему эквивалентности в алгебраической модели программ достаточно рассматривать в ее подмодели, состоящей из специального вида схем программ, называемых матричными. Описание подмодели сводится к описанию ее объектов, именуемых матричными схемами, и механизма, которым в множестве матричных схем вводится отношение их эквивалентности. Этот механизм используется при построении самой алгебраической модели программ.
Алгебраическая модель программ строится над конечными алфавитами Y и P; элементы из Y называются операторными символами, а элементы из P логическими переменными; каждая из них принимает значение из множества {0,1}. Следовательно, и подмодель
YP
При определении матричной схемы, являющейся объектом подмодели, будем пользоваться упрощенным ее описанием, принятым в [2].
YP
собой конечный ориентированный граф, удовлетворяющий требованиям: в нем имеются три выделенные вершины - вход, выход и loop; каждой из других вершин (они называются преобразова-
Y
шины графа, кроме выхода и loop, исходят дуги в количестве, равном числу элементов в множестве X, где X = {x|x : P ^ {0,1}}; всякая дуга помечена элементом x из X; любые две дуги из одной вершины имеют различные метки; добавочным требованием является следующее: любой преобразователь в схеме находится на ориен-
тированном пути, ведущем из входа схемы в ее выход.
На рис. 1 дан пример матричной схемы, по-
Y P Y жит символы y 1 и y2, a P состоит из переменных pi и p2. Вершины схемы обозначены символами v0, vi5 v2, v3; vo - это вход схемы, v1 и v2 - преобразователи и V3 - выход схе мы; loop в схеме onv-vi v2 yi y2
X
для большей обозримости наборы не заключаются в скобки; первая компонента набора фиксиру-
pi
p2
На рис. 2 приведена схема общего вида, для которой построена схема с рис. 1.
Функционирование матричной схемы (далее -просто схемы) осуществляется на отображениях множества Y* (его элементы называются опера-
X
жения именуются функциями разметки; их множество обозначается £.
Пусть G - схема над Y, P, и ^ £ £. Выполнение схемы G на ^ представляет собой обход схемы, который начинается во входе схемы при пустой операторной цепочке и подчиняется следу-
v
схемы, и h - цепочка, с которой пришли в v; ес-vy h hy
из v осуществляется по дуге с меткой ^(hy); если v loop
мы прекращается, в первом случае - с результа-h
G
множества L в множество Y*, частичное в общем случае.
Обратимся к механизму введения отношения эквивалентности в множестве матричных схем YP
двумя параметрами - v и L, где v - это эквивалентность в Y% a L ~ подмножество множества £. По определению, две схемы (v, L)-эквивалемтпы, если, какой бы ни была функция разметки ^ из L, всякий раз, когда выполнение на ^ одной из схем результативно, результативно и выполнение на ^ другой схемы, и при этом
v
операторные цепочки.
Рис. 1. Пример матричной схемы.
Рис. 2. Схема общего вида.
С введением (V, Ь)-эквивалентности в множестве схем над У, Р это множество, по определению, становится (и, Ь)-подмоделью программ.
(V, Ь)-подмодель называется частично коммутативной, если V и Ь ст
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.