ПРОГРАММИРОВАНИЕ, 2010, No 3, с. 3-18
ТЕОРЕТИЧЕСКИЕ ВОПРОСЫ ПРОГРАММИРОВАНИЯ
УДК 681.3.06
ПОЛНЫЕ СИСТЕМЫ ЭКВИВАЛЕНТНЫХ ПРЕОБРАЗОВАНИЙ В УРАВНОВЕШЕННЫХ ПОЛУГРУППОВЫХ МОДЕЛЯХ ПРОГРАММ С ЛЕВЫМ СОКРАЩЕНИЕМ
© 2010 г. Р. И. Подловченко
НИВЦ МГУ 119992 Москва, Воробьевы горы
E-mail: rip@vvv.srcc.msu.su Поступила в редакцию 13.11.2009 г.
Рассматриваемые в данной статье модели программ относятся к алгебраическим, введенным в [1] и достаточно широко изучаемым в теоретическом программировании. Как и прочие модели программ, алгебраические предназначены для исследования семантических свойств программ, взятых в определенной формализации.
При таком исследовании основными являются следующие вопросы:
- как установить, что две программы функционально эквивалентны, т.е. реализуют одну и ту же функцию;
- какими преобразованиями программа переводится в любую ей эквивалентную.
Привлекательность алгебраических моделей программ обусловлена следующими их характеристиками:
- модели построены для формализованных программ, которые, по существу, совпадают с разделами операторов в реальных программах, записанных на алгоритмических языках типа Паскаль; этим они пригодны для изучения семантических свойств реальных последовательных программ;
- структуры объектов модели, называемых схемами программ, берутся совпадающими со структурами моделируемых программ;
поэтому всякое структурное преобразование схемы программ одновременно является структурным преобразованием программы, для которой построена эта схема;
- имеются удобные достаточные признаки того, что выбранная алгебраическая модель программ является аппроксимирующей, т.е. существует класс программ такой, что из эквивалентности схем программ, принадлежащих модели, следует функциональная эквивалентность программ из этого класса, моделируемых данными схемами; для аппроксимирующей модели всякое эквивалентное преобразование структуры ее схемы является эквивалентным преобразованием структуры моделируемой схемой программы из аппроксимируемого класса программ.
В проблематике теории алгебраических моделей основными считаются две проблемы:
- проблема эквивалентности схем в модели;
- проблема эквивалентных преобразований (э.п.) в модели.
Первая состоит в поиске алгоритма, который, получив на свой вход две произвольные схемы из модели, устанавливает, эквивалентны они или нет.
Вторая проблема заключается в построении системы э.п., полной в модели, т.е. обладающей свойством: какими бы ни были две эквивалентные схемы из модели, существует конечная цепочка преобразований, принадлежащих системе, транслирующая первую схему во вторую.
Проблема э.п. в модели обсуждается в случае, когда в модели разрешима проблема эквивалентности схем.
В данной статье рассматриваются алгебраические модели программ, названные уравновешенными полугрупповыми моделями программ с левым сокращением. Их выбор обусловлен двумя факторами: они являются аппроксимирующими, и в них разрешима проблема эквивалентности.
Основная задача статьи состоит в решении для рассматриваемых моделей проблемы э.п., т.е. в построении для них полных систем э.п.
Решение проблемы э.п. ищется в заранее очерченном множестве так называемых фрагмент-ных преобразований схем. Для этого вводится понятие фрагмента схемы, определяется отношение эквивалентности фрагментов и описывается операция подстановки в схеме вместо принадлежащего ей фрагмента другого согласованного с ним фрагмента. Операция подстановки при ее выполнении осуществляет преобразование схемы, называемое фрагментным. Оно является обратимым и называется эквивалентным, если эквивалентны участвующие в операции фрагменты.
Допустимыми при решении проблемы э.п. объявляются системы фрагментных э.п., заданные конечным числом множеств, которые состоят из пар эквивалентных фрагментов. Эти множества обязаны быть разрешимыми, т.е. сопровождаемыми алгоритмами, устанавливающими принадлежность множеству той или иной пары фрагментов. Множества именуются аксиомами.
Доказательство полноты системы в модели проводится традиционным способом, а именно: описывается алгоритм, который, получив на свой вход две эквивалентные схемы из модели, транслирует их к общему виду, т.е. в изоморфные схемы; выполняемые этим алгоритмом фрагментные преобразования схем подсказывают введение необходимых аксиом.
Основным результатом статьи является построение систем фрагментных э.п. схем, полных в рассматриваемых моделях программ, для каждой модели - своей системы.
Статья состоит из шести разделов и приложения.
Первый раздел посвящен описанию рассматриваемых нами моделей программ, для чего используется определение общего вида алгебраической модели программ.
Во втором разделе дается строгая постановка решаемой нами задачи и описываются фраг-ментные преобразования схем.
Стратегия преобразований двух эквивалентных схем к общему виду использует алгоритм, установивший их эквивалентность, и предписывает четыре этапа преобразований.
Согласно этому алгоритму сначала каждая из исходных схем трансформируется в эквивалентную ей схему матричного вида (она называется и-схемой). Это - первый этап стратегии; он излагается в третьем разделе статьи. Осуществляемые на нем преобразования задаются пятью аксиомами.
Затем схема матричного вида преобразуется в эквивалентную ей схему, называемую чистой, что составляет второй этап стратегии. Он описывается в четвертом разделе статьи и поддерживается уже введенными аксиомами.
Полученные для исходных две чистые схемы, будучи эквивалентными, обладают свойствами, выявленными в них алгоритмом, который установил эквивалентность схем. Описанию этих свойств посвящен пятый раздел статьи.
Использование выявленных свойств чистых эквивалентных схем позволяет трансформировать их в такие эквивалентные им чистые схемы, которые функционируют фактически как обычные конечные автоматы; последнее фиксируется отношением строгой эквивалентности схем. Это - третий этап стратегии, достаточно емкий и потребовавший введения новых двух аксиом.
Поскольку строгая эквивалентность полученных чистых схем позволяет воспринимать их как обычные конечные автоматы, то, минимизируя их, строятся изоморфные схемы. Этот этап стратегии, четвертый по счету, не потребовал введения новых аксиом.
Оба последних этапа стратегии рассматриваются в шестом разделе статьи. Он заключается теоремой о построении системы э.п. схем, определяемой семью аксиомами и полной в выбранной алгебраической модели программ.
Существенной особенностью построенной системы является наличие в ней преобразований, позволяющих склеивать в схеме те ее вершины, в которых начинаются эквивалентные подсхемы. Заметим, что поиск таких вершин отпадает, так как все они выявлены алгоритмом, установившим эквивалентность исходных схем. Другое дело - склейка вершин, в которых начинаются строго эквивалентные подсхемы (преобразование четвертого этапа). Их приходится отыскивать, применяя алгоритм, распознающий эквивалентность конечных автоматов.
В приложении дан пример использования основного результата статьи. Здесь берутся две конкретные схемы, принадлежащие одной из рассматриваемых в статье моделей. Эта модель называется коммутативной. Демонстрируется преобразование выбранных схем к общему виду.
В заключение отметим, что построенные в статье полные системы э.п. существенно расширяют известные ранее в теории схем программ. В частности, к рассматриваемым здесь моделям программ относятся так называемые уравновешенные полугрупповые модели программ с левым и правым сокращением. Эти модели исследованы в [2, 3]. Полученным в данной статье основным результатом исправлены те неточности, что допущены в [3] при построении полных систем э.п.
1. РАССМАТРИВАЕМЫЕ НАМИ АЛГЕБРАИЧЕСКИЕ МОДЕЛИ ПРОГРАММ
Начнем с определения общего вида алгебраической модели программ. Она введена в [1] как обобщение существовавших к тому времени моделей программ двух типов: предложенных А.А. Ляпуновым и Ю.И. Яновым в [4, 5] и В.М. Глушковым и А.А. Летичевским в [6].
Каждая алгебраическая модель программ строится над двумя конечными и непересекающимися алфавитами - У и Р. Элементы У на-
зываются операторными символами, элементы Р - логическими переменными. Каждая логическая переменная принимает значения из множества {0,1}. Далее алфавиты У и Р остаются неизменными и поэтому не упоминаются в наименованиях зависящих от них понятий и конструкций.
Объектами модели являются схемы программ. Схема задается конечным ориентированным графом. В нем выделены две вершины: вход -вершина без входящих в нее дуг и с единственной исходящей другой и выход - вершина без исходящих дуг. Остальные вершины графа, если таковые имеются, по своему типу делятся на преобразователи и распознаватели. Из каждого преобразователя исходит одна дуга, и ему сопоставлен символ из У. Из каждого распознавателя исходят две дуги, несущие метки 0 и 1 соответственно, и ему сопоставлена логическая переменная из Р.
Пример схемы приведен на рис. 1. Здесь полыми кружочками без пометок обозначены вход и выход схемы, символы у\, у2 принадлежат алфавиту У, переменные р\, р2 - алфавиту Р.
Функциональное описание схемы связано с процессом ее выполнения, которое осуществляется на так называемой функции разметки. Определим ее.
Введем множество X, X = {х\х : Р ^{0,1}}, элементы которого будем называть наборами значений всех логических переменных, или просто наборами. Введем множество У*, элементы которого - слова в алфавите У, называемые далее операторными цепочками.
По определению, функция разметки - это отображение множества У * в множество X. Множество всех функций разметки над У и Р обозначим Ь.
Опишем выполнение схемы на функции разметки.
Пусть О - схема над У и Р, ц - функция из Ь. Процесс выполнения О на ц состоит в обходе схемы О, сопровождаемом накоплением операторной цепочки. Обход схемы осуществляется детерминированным образом по следующим правилам. Он начинается во входе схемы О при пустой операторной цепочке и идет в направлении дуги, исходящей из посещаемой вершины схемы. В случае, когда это - вход или преобразователь, исходящая дуга е
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.