научная статья по теме ОБ ОДНОМ КЛАССЕ АЛГЕБРАИЧЕСКИХ МОДЕЛЕЙ ПРОГРАММ, ПРЕДСТАВЛЯЮЩЕМ ПРАКТИЧЕСКИЙ ИНТЕРЕС Математика

Текст научной статьи на тему «ОБ ОДНОМ КЛАССЕ АЛГЕБРАИЧЕСКИХ МОДЕЛЕЙ ПРОГРАММ, ПРЕДСТАВЛЯЮЩЕМ ПРАКТИЧЕСКИЙ ИНТЕРЕС»

- ТЕОРЕТИЧЕСКИЕ ВОПРОСЫ ПРОГРАММИРОВАНИЯ

ОБ ОДНОМ КЛАССЕ АЛГЕБРАИЧЕСКИХ МОДЕЛЕЙ ПРОГРАММ, ПРЕДСТАВЛЯЮЩЕМ ПРАКТИЧЕСКИЙ

Научно-исследовательский вычислительный центр МГУ 119991 Москва, Ленинские горы,дом 1, стр. 4 E-mail: rip@vvv.srcc.msu.ru Поступила в редакцию 25.08.2012

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

Алгебраические модели программ введены в [1] для решения глобальной задачи в теории схем программ - разрабатывать на схемах программ эквивалентные преобразования самих программ.

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

• их введению предшествует формализация программ, в которой программа, по существу, совпадает с разделом операторов в реальных программах, записанных на императивном алгоритмическом языке программирования;

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

шение их эквивалентности, и так образуется

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

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

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

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

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

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

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

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

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

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

Рассматриваемые модели именуются частично коммутативными и представляют собой подкласс так называемых уравновешенных полугрупповых моделей с левым сокращением. Для последних в [2] решена проблема эквивалентности, а в [3] - проблема э.п. Однако сложность решения проблемы эквивалентности экспоненциальна, что и заставило обратиться к данному подклассу моделей.

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

Статья, помимо введения, состоит из четырех разделов и приложения.

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

Раздел 3 посвящен описанию ряда семантических свойств, присущих схемам программ в частично коммутативной подмодели. Часть свойств формулируется со ссылкой на работы, где они установлены; вместе с тем, леммаии 3 и 4 доказываются два новых свойства, являющиеся необходимыми для эквивалентных схем именно в частично коммутативной подмодели.

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

В разделе 5 обсуждается проблема э.п. в частично коммутативной подмодели. Кратко излагается метод, которым она решена в уравнове-

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

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

2. ЧАСТИЧНО КОММУТАТИВНАЯ ПОДМОДЕЛЬ ПРОГРАММ

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

Алгебраическая модель программ строится над конечными алфавитами Y и P; элементы из Y называются операторными символами, а элементы из P логическими переменными; каждая из них принимает значение из множества . Следовательно, и подмодель

При определении матричной схемы, являющейся объектом подмодели, будем пользоваться упрощенным ее описанием, принятым в [2].

собой конечный ориентированный граф, удовлетворяющий требованиям: в нем имеются три выделенные вершины - вход, выход и loop; каждой из других вершин (они называются преобразова-

шины графа, кроме выхода и loop, исходят дуги в количестве, равном числу элементов в множестве X, где X = ; всякая дуга помечена элементом 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

для большей обозримости наборы не заключаются в скобки; первая компонента набора фиксиру-

На рис. 2 приведена схема общего вида, для которой построена схема с рис. 1.

Функционирование матричной схемы (далее -просто схемы) осуществляется на отображениях множества Y* (его элементы называются опера-

жения именуются функциями разметки; их множество обозначается £.

Пусть G - схема над Y, P, и ^ £ £. Выполнение схемы G на ^ представляет собой обход схемы, который начинается во входе схемы при пустой операторной цепочке и подчиняется следу-

схемы, и h - цепочка, с которой пришли в v; ес-vy h hy

из v осуществляется по дуге с меткой ^(hy); если v loop

мы прекращается, в первом случае - с результа-h

множества L в множество Y*, частичное в общем случае.

Обратимся к механизму введения отношения эквивалентности в множестве матричных схем YP

двумя параметрами - v и L, где v - это эквивалентность в Y% a L

подмножество множества £. По определению, две схемы (v, L)-эквивалемтпы, если, какой бы ни была функция разметки ^ из L, всякий раз, когда выполнение на ^ одной из схем результативно, результативно и выполнение на ^ другой схемы, и при этом

Рис. 1. Пример матричной схемы.

Рис. 2. Схема общего вида.

С введением (V, Ь)-эквивалентности в множестве схем над У, Р это множество, по определению, становится (и, Ь)-подмоделью программ.

(V, Ь)-подмодель называется частично коммутативной, если V и Ь ст

Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.

📎📎📎📎📎📎📎📎📎📎