Быстрые алгоритмы проверки эквивалентности программ в моделях с полугрупповой семантикой тема автореферата и диссертации по математике, 01.01.09 ВАК РФ

Московский государственный университет имени М.В. Ломоносова

Быстрые алгоритмы проверки эквивалентности программ в моделях с полугрупповой семантикой

01.01.09 - Дискретная математика и математическая кибернетика

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

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

Подымов Владислав Васильевич

25 ФЕВ 2015

005559581

Москва - 2015

005559581

Работа выполнена на кафедре математической кибернетики факультета вычислительной математики и кибернетики федерального государственного бюджетного образовательного учреждения высшего образования «Московский государственный университет имени М.В. Ломоносова».

Научный руководитель: Захаров Владимир Анатольевич,

доктор физико-математических наук, профессор кафедры математической кибернетики факультета вычислительной математики и кибернетики федерального государственного бюджетного образовательного учреждения высшего образования «Московский государственный университет имени М.В. Ломоносова»

Официальные оппоненты: Ломазова Ирина Александровна,

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

Башкин Владимир Анатольевич,

доктор физико-математических наук, доцент кафедры теоретической информатики факультета информатики и вычислительной техники федерального государственного бюджетного образовательного учреждения высшего профессионального образования «Ярославский государственный университет им. П.Г. Демидова»

Ведущая организация: Федеральное государственное бюджетное учреждение

науки Институт систем информатики им. А.П. Ершова Сибирского отделения Российской академии наук

Защита состоится 27 марта в 11 час. 00 мин. на заседании диссертационного совета Д 501.001.44 при Московском государственном университете имени М.В. Ломоносова по адресу: 119991, Москва, ГСП-1, Ленинские горы, д. 1, стр. 52, факультет ВМК, аудитория 685.

С диссертацией можно ознакомиться в Научной библиотеке Московского государственного университета имени М.В. Ломоносова по адресу: 119192, г. Москва, Ломоносовский проспект, д. 27 — а также на официальном сайте факультета ВМК МГУ http://www.cmc.msu.ru в разделе «Диссертации».

Автореферат разослан «. 4- £ » Ъ&ВРАЛЯ 2015 г.

Ученый секретарь

диссертационного совета Д 501.001.44, доктор физико-математических наук, доцент

О.В. Шестаков

Общая характеристика работы

Актуальность и степень разработанности темы исследования. Основная проблема, исследованию которой посвящена настоящая диссертация, — проблема эквивалентности программ — может быть сформулирована следующим образом: выяснить, имеют ли заданные программы 7Г1, 7Гг схожее (одинаковое, эквивалентное) поведение. Существует много строгих формулировок проблемы эквивалентности в различных моделях вычислений. Наиболее известна среди таких формулировок проблема функциональной эквивалентности: поведение программы определяется как реализуемая ей функция преобразования входных данных в выходные данные, а эквивалентность программ — как совпадение реализуемых ими функций. Исследование функциональной эквивалентности затрудняется теоремой Райса-Успенского, из которой следует неразрешимость функциональной эквивалентности в любой модели вычислений, в которой можно реализовать все функции, вычислимые по Тьюрингу. При этом сравнение функциональности программ используется во многих задачах программирования, из чего следует важность исследования функциональной эквивалентности программ. Такое исследование активно проводится в рамках теории схем программ.

В теории схем программ описываются и исследуются характерные структурные особенности программ различных языков и парадигм программирования. Проблема эквивалентности для этих моделей формулируется так, чтобы из эквивалентности схем (объектов модели) вытекала эквивалентность программ, описываемых этими схемами. В начале развития теории схем программ было получено много результатов разрешимости и неразрешимости проблемы эквивалентности в разнообразных моделях программ, например: разрешимость эквивалентности схем Ляпунова-Янова, логико-термальной эквивалентности стандартных схем, древесной эквивалентности рекурсивных схем; неразрешимость эквивалентности стандартных схем, рекурсивных схем, и разрешимость для

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

Описание быстрых алгоритмов проверки эквивалентности в моделях программ затрудняется тем, что проблема эквивалентности схем Ляпунова-Янова с бесконечной сигнатурой (бесконечным числом различных символов, которые разрешено использовать для описания примитивов программ; здесь — операторов и предикатов) со^Р-полна. При этом схемы Ляпунова-Янова считаются одной из самых простых моделей вычислений теории схем программ. Однако вклад в со-ОТ-трудность вносится только бесконечностью сигнатуры, но не структурными особенностями программ: эквивалентность схем Ляпунова-Янова с конечной сигнатурой полиномиально разрешима. В настоящей диссертации исследуется вклад структуры программ в трудность проблемы эквивалентности, то есть рассматриваются модели с конечной сигнатурой. Таким образом, быстрота разработанных в диссертации алгоритмов определяется как полино-миальность их времени работы относительно размеров программ.

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

над конечными алфавитами операторов и логических условий. Содержательно, логическое условие может пониматься как набор значений всех предикатов программы. Чтобы определить поведение пропозициональной программы, необходимо придать значение всем используемым в ней операторам и логическим условиям. Для этих целей в пропозициональных моделях вводится понятие интерпретации, совпадающее с понятием детерминированной динамической модели в динамической логике. Интерпретация состоит из (детерминированной динамической) шкалы и оценки логических условий. Шкалой определяются: множество состояний данных, над которыми программа производит вычисление; состояние данных, с которого начинается вычисление; значение каждого оператора — функция преобразования состояний данных. Оценка логических условий сопоставляет каждому состоянию данных истинное в нём логическое условие. В каждой интерпретации определяется результат вычисления пропозициональной программы. Программы объявляются эквивалентными в интерпретации, если результаты их вычислений в этой интерпретации совпадают. В настоящей диссертации исследуется проблема эквивалентности программ на шкалах: программы эквивалентны на шкале, если они эквивалентны в каждой интерпретации, включающей в себя эту шкалу. Если состояния данных шкалы являются моноидом на множестве операторов, то такая шкала называется полугрупповой. Если состояния данных шкалы частично упорядочены относительно действия операторов, то такая шкала называется упорядоченной. Примером упорядоченной полугрупповой шкалы является свободная шкала: состояния данных такой шкалы являются свободным моноидом. Другой пример — это шкала, состояния данных которой являются моноидом, определяемым произвольным набором соотношений коммутативности (аЬ = Ьа, где а и Ь — операторы) и подавления (аЬ — Ь, где а и Ь — операторы). Такая шкала далее называется шкалой с коммутативностью и подавлением. Содержательно, соотношение аЬ = Ьа означает, что порядок выполнения подряд идущих операторов о, Ь не влияет на результат вычисления, а соотношение аЬ = Ъ — что опера-

тор а оказывается фиктивным, если сразу после него выполняется оператор Ь. Такие соотношения можно легко получить, анализируя переменные, используемые операторами реальной программы.

При исследовании модели рекурсивных программ в настоящей диссертации внимание уделяется классам линейных и металинейных унарных рекурсивных программ. Рекурсивная программа называется унарной, если все её функции, кроме функции ветвления (if х then у else z), зависят ровно от одного аргумента. Унарная рекурсивная программа называется линейной, если каждый функциональный терм, использованный в её описании, содержит не более одного вхождения символов, определяемых программой, и металинейной, если последнее требование распространяется на все термы, кроме терма, с которого начинается вычисление программы. Анализ проблемы эквивалентности оказывается затруднительным даже для таких скромных по выразительным возможностям классов рекурсивных программ.

Цель работы — разработка быстрых алгоритмов решения проблемы эквивалентности в пропозициональных моделях последовательных и рекурсивных программ.

Основные результаты работы следующие.

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

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

3. Разработаны полиномиальные алгоритмы проверки эквивалентности металинейных унарных рекурсивных программ на свободных шкалах.

4

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

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

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

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

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

пользованы в решении практических задач программирования: оптимизации, реорганизации (рефакторинга), обфускации, верификации программ, задачах поиска вредоносного кода и многих других.

Степень достоверности, апробация, список публикаций. Основные результаты диссертации сформулированы в виде теорем о полиномиальной разрешимости проблемы эквивалентности в рассматриваемых моделях программ. Доказательством теорем является описание решающих алгоритмов с обоснованием корректности и оценкой времени работы этих алгоритмов. Результаты представлены на конференции "Интеллектуальные системы и компьютерные науки" (2011 год), семинаре "Дискретная математика и её приложения" (2012 год), конференции "Проблемы теоретической кибернетики" (2014 год) и опубликованы в работах [1-7], четыре из них — в журналах из перечня ВАК [1-4]. В работе [1] В.В. Подымову принадлежат формулировка и техника обоснования основного результата статьи. В работе [4] В.В. Подымову принадлежат формулировка и обоснование основного результата статьи.

Структура и объём диссертации. Диссертация состоит из восьми глав, включая введение (первая глава) и заключение (восьмая глава), и следующего за заключением списка литературы. Общий объём рукописи составляет 164 страницы и включает 5 рисунков. Список литературы содержит 115 наименований.

Основное содержание работы

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

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

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

Если А — алфавит, то записью А* будет обозначаться множество всех слов в этом алфавите. Символом А обозначается пустое слово.

Автомат 21 определяется: входным алфавитом 21. А; конечным множеством состояний 21.<3; множеством меток состояний 21 .Ь\ инициальным состоянием 21.д € 21.(3; функцией переходов 21Т : 21.(5 х 21.Л —>• 21.(3; разметкой состояний 2l.il/ : 21.(3 —> 21.1/. На вход автомату 21 подаются слова в алфавите 21.А. Стандартным образом определяется то, как автомат изменяет свои состояния при прочтении символов входного слова. Результатом работы автомата 21 на слове К объявляется метка состояния, в которое автомат переводится этим словом.

Моноид с конечным множеством образующих А, определяемый соотношениями Т вида = /12, где Н^Ьъ € А*, может быть описан следующим образом. Элементами моноида являются множества слов в алфавите А. Элемент (/г), образованный словом Н, состоит из всех слов, которые могут быть получены конечным числом применений соотношений множества Т к слову И. Применение соотношения д\ = 52 состоит в замене в слове К подслова, совпдающего с gi, на (г € {1,2}). Соотношение коммутативности имеет вид аЬ = Ьа, а соотношение подавления — аЬ = Ъ, где а,Ъ е А. Моноид, определяемый произвольным набором соотношений коммутативности и подавления, далее называется моноидом с коммутативностью и подавлением.

В третьей главе приводятся основные определения, относящиеся к рассматриваемым в диссертации моделям программ: пропозициональным моделям последовательных программ (раздел 3.1) и рекурсивных программ (раздел 3.2).

\уЫ1е(х != у) {

1£(х > у) х = х - у; еЬе у = у - х;

}

(а) Алгоритм Эвклида

(Ь) Пропозициональная последовательная програм-

ма

Рис. 1. Пример построения пропозициональной последовательной программы

В сигнатуру этих моделей входят конечные алфавиты операторов О и логических условий £.

Пропозициональная последовательная программа 7Г состоит из: конечного множества состояний управления тт.Ц входа ж.еп б тт.Ь] выхода тт.ех £ 7Г.Ь\ функции переходов -к.Т : Ь \ {п.ех} х £ —► Ь\ функции привязки тт.В : Ь О. Для соотношения ж.Т{1\, а) = ¡2 используется запись 1\ 12. Объединение отношений по всем логическим условиям а обозначается записью —Определение программы поясняется рисунком 1, на котором приведены фрагмент программы в синтаксисе языка Си (рисунок 1(а)) и пропозициональная последовательная программа, описывающая структуру этого фрагмента (рисунок 1(Ь)). Состояния управления изображены кругами и прямоугольниками, и в них вписаны операторы согласно функции привязки. Двойным прямоугольником изображён вход, одинарным — выход. Операторы ах, ау отвечают выполнению инструкций "х = х - у" и "у = у - х", два других оператора введены для обозначения начала и конца вычисления. Дугами изображена функция переходов программы. Логические условия сть <72> о"з содержательно описываются соотношениями х<у,х = укх>у.

Pow :: Integer -> Integer

Pow 0 = 1

D(Pow, <Ti) = err D(Pow, o<i) = one D(Pow, cr3) = dec Pow dup

Pow x | x>0 = 2*Pow(x—1)

(а) Функция вычисления степени двойки

(Ь) Описание тел функций унарной рекурсив-

ной программы

Рис. 2. Пример построения унарной рекурсивной программы

В описании унарной рекурсивной программы помимо алфавитов операторов и логических условий рассматривается также счётно-бесконечный алфавит функциональных символов Описание программы и её поведения основывается на понятии терма. Термом называется слово в алфавите D U Множество термов обозначается записью Terms. Унарная рекурсивная программа тт состоит из: конечного множества заголовков тг.Н с описания тел функций 7t.D : тс.Н х £ —>■ Terms; запроса ir.q б Terms. Введённое определение поясняется рисунком 2, на котором приведены функция вычисления степени числа 2 в синтаксисе языка Haskell (рисунок 2(a)) и описание тел функций соответствующей унарной рекурсивной программы (рисунок 2(b)). Программа содержит единственный заголовок Pow. Логические условия <J\, <72, содержательно описываются соотношениями 1<0,а; = 0иа;>0. Операторами one, dec, dup и err описываются соответственно функции 1, х — 1, 2х и функция, безусловно возвращающая ошибочное значение.

Семантика программ в обеих рассматриваемых моделях определяется на основе шкал и интерпретаций (в терминах динамической логики — (детерминированных) динамических шкал и (детерминированных) динамических моделей соответственно). Шкалой Т определяются: множество состояний данных J°.S, над которым программа производит вычисление; начальное состояние данных J-.s е J-.S\ функция переходов T.R : S х D S. Интерпретация I включает в себя шкалу I.F и разметку состояний данных логическими условиями : S -» £. Содержательно, шкала придаёт каждому оператору а

значение функции преобразования данных а: а(в) = Р.В.(в, а), а интерпретация, помимо этого, придаёт значение логическим условиям. Состояние данных .. Щ^.в)...)) обозначаетя записью [[а*... (ц]. Для состояний данных ¿1, 52 записью ¿1 -< 52 обозначается следующий факт: существует непустая последовательность (или цепочка) операторов а\... а,к, такая что = Щ(...Щ(вх)...). Записью обозначается рефлексивное замыкание отношения -<. Интерпретация, включающая в себя шкалу Т, называется ^-интерпретацией. Шкала называется полугрупповой, если существует моноид с множеством образующих О, такой что: состояния данных шкалы суть элементы моноида; начальное состояние данных есть нейтральный элемент моноида; функция переходов согласована с операцией моноида. Если при этом моноид определяется произвольным набором соотношений коммутативности и подавления, то такая шкала называется шкалой с коммутативностью и подавлением. Шкала называется упорядоченной, если для любых цепочек операторов /г, д из равенства \кд\ = [Л] следует равенство д = А.

Трассой последовательной программы тг является всякая последовательность её состояний управления вида п.еп /х 7Гг —• ■ ■ • Если трасса программы 7г оканчивается в выходе, то она объявляется вычислением этой программы. Для простоты вводится обобщение функции привязки п.В с состояний данных на трассы: ж.В(1\ ->т Iг —...) = п.В(1\) тг.В{12)... . Трасса 11 —¿2 -»я- • • • реализуется в интерпретации X, если соотношение 1{ верно для любой пары соседних состояний /¿+г

этой трассы. Результатом конечного вычисления ср программы ж на шкале 7-и в интерпретациях, содержащих эту шкалу, объявляется состояние данных 1тг. В (ср)}. Бесконечным вычислениям присваивается особый результат ±, не являющийся состоянием данных.

Каждый терм £ может быть представлен в виде £ = Ь.ф Ь.г, где: — наибольший по длине префикс терма являющийся цепочкой операторов; t.ф 6 5 и {Л}. Запись £ где тг — унарная рекурсивная программа

и <7 е £, используется для задания терма £' = t.l TT.D(t.tp, a) t.г. Записью t -^тг il обозначается следующий факт: существует логическое условие ст, такое что t t'. Трассой программы 7Г является всякая последовательность термов вида n.q t\ Ц —>т ■ Вычислением программы 7г объявляется всякая трасса, которую нельзя продолжить. Трасса t\ —¿2 • • • реализуется в интерпретации X, если соотношение ti+i выполнено для любых соседних термов f*, ¿¿+i этой трассы. Если вычисление оканчивается цепочкой операторов h, то его результатом на шкале Т ив любой ^-интерпретации объявляется состояние данных Остальные вычисления имеют результат _L, не являющийся состоянием данных.

Программы объявляются эквивалентными в интерпретации, если результаты их вычислений в этой интерпретации совпадают, и эквивалентными на шкале Т, или ^-эквивалентными, если они эквивалентны в любой интерпретации, включающей в себя эту шкалу. Трассы объявляются совместными на шкале J-, или ^-совместными, если существует ^-интерпретация, в которой реализуются обе эти трассы. Таким образом, программы ^"-эквивалентны в том и только в том случае, если результаты любых их ^-совместных вычислений совпадают.

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

Заголовки унарных рекурсивных программ классифицируются по возможности построения из них конечных вычислений. Например, если программа я-', получаемая из я- заменой запроса на функциональный символ /, имеет хотя бы одно конечное вычисление, то символ / называется завершаемым в программе 7г. Также для единообразия завершаемым считается пустое слово.

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

Также в главе 3 сформулированы известные утверждения, не являющиеся заслугой автора настоящей диссертации. Два из них относятся к модели последовательных программ. Первое утверждение формулируется так: для любой трассы программы и любой упорядоченной шкалы Т существует ^-интерпретация, в которой реализуется эта трасса. Второе утверждение предоставляет простой способ проверки ^-совместности трасс программ для упорядоченной шкалы Т, используемый в дальнейших рассуждениях наряду с основным определением совместности. Аналогичные утверждения формулируются для нормализованных унарных рекурсивных программ. Кроме того, для унарных рекурсивных программ приведены утверждения, позволяющие при исследовании проблемы эквивалентности без ограничения общности рассматривать только нормализованные программы.

В четвёртой главе обсуждаются полученные в диссертации результаты (раздел 4-1) и подход, с помощью которого эти результаты получены (раздел 4-2). Согласно этому подходу — методу совместных вычислений — для проверки ^-эквивалентности программ тгх, 7Гг вводится и исследуется граф совместных вычислений Г = Г(7Т1,7Г2,Р), описывающий пары вычислительных конфигураг ций программ, которые могут быть достигнуты при совместном выполнении этих программ.

Вычислительной конфигурацией рекурсивной программы является терм, а последовательной — состояние данных и состояние управления, достигнутые в процессе вычисления. Совместное выполнение программ в заданной интерпретации начинается во входах (для последовательных программ) или запросах

(для рекурсивных программ). Шаг совместного выполнения состоит следующем. По текущей паре конфигураций определяются активные программы: одна, обе или ни одной. Конфигурации активных программ преобразуются согласно построению вычислений: трасса последовательной программы продолжается на одно состояние управления, а рекурсивной — на один терм. Активность программ задаётся стратегией совместного выполнения. Эта стратегия зависит от выбранной модели программ и от шкалы и для каждой пары конфигураций определяет, какие из программ активны.

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

Вершинами графа Г объявляются всевозможные различия пар вычислительных конфигураций. Дугами в графе Г соединяются различия, являющиеся соседними хотя бы в одном совместном выполнении программ. Корнем графа Г объявляется различие инициальных конфигураций программ (для последовательной программы — вход и состояние данных, в которое приводит выполнение оператора, приписанного входу; для рекурсивной программы — запрос). В графе Г выделяются опровергающие маршруты — маршруты, отвечающие построению совместных вычислений программ с различными результатми. Таким образом, проверка эквивалентности программ сводится к проверке отсутствия опровергающих маршрутов в графе совместных вычислений. Граф Г, вообще говоря, бесконечен, поэтому из такого сведения не следует разрешимости, а тем более полиномиальной разрешимости ^"-эквивалентности программ. Алгоритмы проверки ^-эквивалентности программ, разработанные в диссертации, за полиномиальное относительно размеров программ время обходят ограничен-

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

В пятой главе обосновывается полиномиальная разрешимость проблемы эквивалентности пропозициональных последовательных программ на произвольных упорядоченных шкалах с коммутативностью и подавлением. Для этого в разделах 5.1-5.3 проводится исследование свойств моноидов с коммутативностью и подавлением, в разделах 5.4-5.6 описывается и исследуется граф совместных вычислений, а в разделе 5.7 — алгоритм проверки эквивалентности, основанный на обходе этого графа. Символом Т далее обозначается произвольная упорядоченная шкала с коммутативностью и подавлением.

В разделе 5.1 устанавливается критерий упорядоченности моноида с коммутативностью и подавлением.

Теорема 5.1.1. Пусть С, А С О х О и М — моноид, образованный множеством О и определяемый соотношениями {аЬ = Ъа \ (а, Ь) € С} и {аЬ — Ъ | (а, Ь) е Л}. Тогда моноид М упорядочен в том и только в том случае, если С* П Л+ = 0, где С* — рефлексивно-симметричное замыкание отношения С, а Л+ — транзитивное замыкание отношения Л.

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

В разделе 5.3 описан автомат, распознающий подавление. Предполагается заданным упорядоченный моноид М. с коммутативностью и подавлением. Автомат, распознающий подавление, обладает следующими свойствами. На вход автомату подаются слова в алфавите образующих моноида М. Метками автомата являются множества образующих. Результатом работы автомата на слове к является множество образующих а, для которых верно равенство ((аЛ)-) = (Н~) (минусом в верхнем индексе здесь обозначен зеркальный образ слова). Кроме

того, если верно равенство (/г-) = (д~), то слова ¡гид приводят автомат в одно и то же состояние.

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

Автомат, распознающий подавление, используется в разделе 5.5 при построении автомата, распознающего эффекты подавлений.

В разделе 5-4 приводится описание графа совместных вычислений Г = Г(тг1,7Г2, и доказывается сводимость проверки ^-эквивалентности к проверке отсуствия опровергающих маршрутов в графе Г. Структура графа Г определяется выбором стратегии совместного выполнения и различия конфигураций, приведённых далее. Пусть при совместном выполнении программами 7Гх,7Гг получены состояния данных 5х, ¿2 соответственно. Если вх = зг, то активны обе программы. Если 52 -< вх, то активна только программа 7Гг. Иначе активна только программа 7Гх. При этом если активная программа завершила построение вычисления, то она становится неактивной. В различии пары конфигураций в явном виде сохранены текущие состояния управления программ, а текущие состояния данных вх, вг преобразуются следующим образом: состояния данных Ях, ¿2 представляются в виде вх = з о в'х, 5г = й о й'2; выбирается состояние данных в, такое что кратчайшая приводящая в него цепочка операторов имеет наибольшую возможную длину; в различии сохраняются состояния данных й'х, ¿2. Корректность такого определения различия основывается на свойствах моноидов с коммутативностью и подавлением, исследованных в разделах 5.1-5.3.

Опровергающие маршруты графа Г могут быть описаны в терминах совместного выполнения следующим образом. Случай 1: в результате совместного выполнения программами построены конечные вычисления с различными результатами. Случай 2: совместное выполнение бесконечно, программа 7Г» почти всегда (то есть всегда, кроме быть может, конечного числа шагов) неактивна, при этом её трасса может быть достроена до конечного вычисления (г £ {1,2}).

Теорема 5.4.1. Пусть Т — упорядоченная шкала с коммутативностью и подавлением и jti, 7Гг — пропозициональные последовательные программы. Тогда эти программы J--эквивалентны в том и только в том случае, если граф Г не содержит опровергающих маршрутов.

В разделе 5.5 вводится аппарат эффектов подавлений, необходимый для ограничения числа вершин графа Г, которые достаточно исследовать для ответа на вопрос об ^-эквивалентности программ 7Ti, 7Гг. Эффект подавления эе3, индуцированный состоянием данных s, — это функция преобразования состояний данных следующего вида: se^sj) = S2, если sios = S20S и при этом состояние s2 выбрано так, что наименьшая длина принадлежащих этому состоянию цепочек операторов имеет максимально возможное значение. В разделе формулируются и обосновываются свойства эффектов подавлений, включая конечность множества всевозможных эффектов подавления и его частичную упорядоченность относительно преобразования состояний данных операторами. Кроме того, в разделе доказано существование и приводится явное описание автомата, распознающего эффекты подавления: на вход автомату подаются цепочки операторов; эффекты подавления ae^j, эеу совпадают тогда и только тогда, когда совпадают результаты работы автомата на цепочках Л, д\ если = f<?J, то цепочки h, д приводят автомат в одно состояние данных. Описание автомата, распознающего эффекты подавления, основано на описании автомата, распознающего подавление операторов.

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

распознающим эффекты подавления, позволяют разбить вершины графа Г на полиномиальное относительно размеров программ число групп так, что по накоплении полиномиального числа вершин в группе при обходе графа Г можно либо констатировать существование в этом графе опровергающего маршрута (и следовательно, неэквивалентность программ), либо игнорировать остальные вершины группы в дальнейшем обходе. Такое разбиение обеспечивается леммами, сформулированными в разделе 5.6. Алгоритм проверки ^-эквивалентности программ описан в разделе 5.7 и состоит в обходе графа совместных вычислений: обход начинается в корне графа; если в одной из групп исследовано достаточно много вершин, то в зависимости от свойств этой группы либо констатируется неэквивалентность программ, либо остальные вершины группы игнорируются в дальнейшем обходе; если граф совместных вычислений полностью построен, то эквивалентность программ определяется отсутствием в нём опровергающих маршрутов. Корректность и полиномиальность алгоритма строго обосновываются, что позволяет считать доказанной основную теорему главы 5, которой завершаются раздел и глава.

Теорема 5.7.1. Пусть Т — упорядоченная шкала с коммутативностью и подавлением. Тогда проблема Т-эквивалентности пропозициональных последовательных программ разрешима за время, полиномиальное относительно размеров программ.

В шестой главе исследуется проблема эквивалентности линейных унарных рекурсивных программ на упорядоченных полугрупповых шкалах. Результаты исследования следующие. Устанавливается набор требований к упорядоченной полугрупповой шкале Т7, достаточных для описания графа совместных вычислений Г = Г(7Г1,7Г2,^") линейных унарных рекурсивных программ 7Гх, тг2 и полиномиального алгоритма проверки ^"-эквивалентности программ щ, П2, основанного на обходе этого графа. В предположении о том, что шкала Т удовлетворяет установленным требованиям, обосновываются корректность и сложность алгоритма проверки эквивалентности.

Одно из требований, предъявляемых к шкале Т7, приведено в разделе 6.1 и состоит в наличии критериальной системы для этой шкалы. На основе критериальной системы вводится удобное для исследования различие пар линейных термов. Критериальная система может быть определена так. Рассмотрим линейные термы ¿х, ¿2- Опустим символы .ф, Щ — они в явном виде сохраняются в различии термов. Оставшиеся цепочки операторов и.1, и.г заменим состояниями данных = [¿¡.¿I, е- = Выберем моноид и, элементы моноида объявим различиями состояний данных. Отобразим состояния вх, йг в моноид и гомоморфизмом <р : Р.Б х р.Б II. То же сделаем для элементов з'2. Расширим моноид 17 до моноида V/ (далее он называется критериальным), добавив элементы, отмечающие начало и конец совместной работы программ: и>+ и IV* соответственно. Пусть о — операция моноида \У. Помимо символов ^.ф, Н2 в различии термов сохраняются элементы 1и+ о йг) и 1р(з[, з'2) ° т*. Моноид У/ с выделенными элементами т*, подмоноидом II и гомоморфизмом <р образуют критериальную систему.

Символом е обозначается нейтральный элемент критериального моноида. На критериальную систему для шкалы Т налагаются следующие требования:

1. равенство ы+о(р(зг, 5г) охи*.— е верно тогда и только тогда, когда = ;

2. любой элемент класса смежности ги+ о и имеет не более одного правого обратного элемента в классе смежности II о ги*\

3. любой элемент класса смежности II о ю* имеет не более одного левого обратного элемента в классе смежности ги+ о и.

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

Г = Г(7Г1,7Т2, Т) для определения ^-эквивалентности программ тт\, 7г2. Описание графа совместных вычислений приводится в разделе 6-2 и основывается на приведённом выше понятии различия линейных термов и на следующей стратегии совместного выполнения, Пусть при совместном выполнении программами 7Г1, 7Г2 получены соответственно термы ¿1, ¿2- Если [¿¿.¿1 -< Ii3-i.il, то активна только программа щ. Иначе активны обе программы. При этом если активная программа завершила построение вычисления, то она объявляется неактивной.

Опровергающие маршруты графа совместных вычислений могут быть описаны в терминах совместного выполнения следующим образом. Случай 1: в результате совместного выполнения программами построены конечные вычисления с различными результатами. Случай 2: совместное выполнение бесконечно, программа щ почти всегда неактивна, при этом символы Ь.ф всех получаемых ей термов I завершаемы (г 6 {1,2}). В разделе 6.2 формулируется и обосновывается утверждение, позволяющее свести проверку ^-эквивалентности нормализованных линейных унарных рекурсивных программ 7Г1,7г2 к проверке отсутствия опровергающих маршрутов в графе Г. В формулировке утверждения предполагается наличие критериальной системы для шкалы Т, то есть возможность описания графа Г.

Теорема 6.2.1. Программы 1- -эквивалентны тогда и только тогда, когда в графе Г отсутствуют опровергающие маршруты.

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

грамм определяется отсутствием в нём опровергающих маршрутов. В своём описании алгоритм использует два дополнительных предположения. Предположение 1: предоставлен алгоритм, принимающий на вход цепочки операторов Лх, /гг и проверяющий соотношение [/11] -< |/1г1- Предположение 2: предоставлен алгоритм, проверяющий равенство элементов критериального моноида в классах смежности го+ о и, V о ю* и о и о и;*; на вход алгоритму подаются цепочки операторов кг, Лг, и ими описывается элемент ^([[/м], моноида II. Задачи, сформулированные в последних двух предположениях, далее называются соответственно задачей достижимости и задачей равенства. Основной результат раздела 6.3 может быть сформулирован следующим образом.

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

Из утверждений раздела 6.3 следует в худшем случае экспоненциальная относительно размеров программ оценка числа исследуемых вершин графа совместных вычислений. Эта оценка снижается до полиномиальной утверждениями, сформулированными и доказанными в разделе 6.4 и использующими дополнительное предположение о том, что критериальный моноид является группой. В разделе 6.4 предложен полиномиальный алгоритм проверки ^"-эквивалентности линейных унарных рекурсивных программ. Этот алгоритм может быть получен из алгоритма в разделе 6.3 следующими изменениями. В задачу равенства добавляется следующая подзадача: проверить равенство элементов ги^1 о щ^1 — ш^1 о и)11, где Ш1 и №3 - элементы класса ш+ о [/, а №2, и)4 — элементы класса 1} о гу*; способ задания элементов классов смежности остаётся тем же, что и ранее в задаче равенства. Кроме того, предполагается полиномиальная разрешимость задач достижимости и равенства. Корректность и полиномиальность алгоритма строго обосновываются, что позволяет считать доказанной основную теорему главы 6, которой завершаются раздел и глава.

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

В седьмой главе доказывается полиномиальная разрешимость проблемы эквивалентности металинейных унарных рекурсивных программ на свободной шкале. Далее рассматриваются свободная шкала Т и металинейные унарные рекурсивные программы 7Г1, яг- Без ограничения общности эти программы считаются нормализованными. Конечное вычисление нормализованной программы обязательно оканчивается цепочкой операторов.

В разделе 7.1 вводится понятие веса ||тг||4 терма t в программе 7г: рассматриваются все вычисления программы тг', получаемой из 7Г заменой запроса на терм если все такие вычисления бесконечны, то вес бесконечен; иначе выбирается вычисление, оканчивающееся наименьшей по длине цепочкой операторов, и весом объявляется длина этой цепочки. Также в разделе приводятся и обосновываются утверждения, позволяющие считать, что запросы исследуемых программ не содержат тупикового символа и имеют одинаковый вес (в своих программах).

В разделе 7.2 описывается граф совместных вычислений Г = Г(7Г1,7Г2,Т7) нормализованных металинейных унарных рекурсивных программ тгх, 7Г2. Различия пар термов, а также стратегия совместного выполнения описываются следующим образом. Пусть в процессе совместного выполнения программами получены термы ¿1, ¿2.

Случай 1: = и ни один из термов <1, не содержит вхождений тупикового символа. Различие термов ¿1, ¿2 схематично изображено на рисунке 3. Левым прямоугольником изображается символ и.ф, овалом — цепочка операторов и.гЛ, правым прямоугольником — последовательность заголовков ¿¿.г.г.

ь-. цц^о! I ¿1: ^а и-. \-101-1

¿2:1 ПС^ЕЗ ¿г:| ЮЕПР 1Ш»П

Рис. 3. Различие термов. Случай 1

и I 1€1П и и: Г~101-1

¿3-«: ДИ "1 ¿3-«: I ¿з-;: <Щ |

Рис. 4. Различие термов. Случай 2

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

Случай 2: -< и ни один из термов £2 не содержит вхождений тупикового символа. Различие термов г2 схематично изображено на рисунке 4. Овалом для ¿з_г изображается цепочка операторов из которой вычерк-

нут префикс длины \и.1\, а прямоугольником — терм ¿3^.ф £3_,т. В остальном смысл изображений и требование равенства белых частей овалов те же, что и в случае 1. В этом случае активна только программа щ.

Случай 3: ¿1 = ¿2 € О*. Таким термам сопоставляется особое различие, означающее, что программами построены конечные вычисления с равными результатами. Обе программы неактивны.

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

Случай 5: ни одно из условий предыдущих случаев не выполнено. Таким термам сопоставляется различие, выраженное особой вершиной графа Г, на-

зываемой далее опровергающей. Смысл этой вершины пояснён далее. Обе программы неактивны.

Опровергающими объявляются маршруты графа Г, начинающиеся в корне и оканчивающиеся в опровергающей вершине. В разделе 7.2 формулируется и обосновывается утверждение, позволяющее свести проверку ^-эквивалентности нормализованных металинейных унарных рекурсивных программ к проверке наличия опровергающих маршрутов в графе Г.

Теорема 7.2.1. Нормализованные метпалинейные унарные рекурсивные программы тг1, т?2 эквивалентны на свободной шкале Т тогда и только тогда, когда в графе Г(7Т1,7Г2,из корня не достижима опровергающая вершина.

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

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

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

Список публикаций

1. Захаров В. А., Подымов В. В. Об одной полугрупповой модели программ, определяемой при помощи двухленточных автоматов // Научные ведомости Белгородского государственного университета. Серия История, экономика, политология, информатика. — 2010. — Т. 14, № 7. — С. 94-101.

2. Подымов В. В. Алгоритм проверки эквивалентности линейных унарных рекурсивных программ на упорядоченных полугрупповых шкалах // Вестник Московского университета. Серия 15. Вычислительная математика и кибернетика. - 2012. - № 4. - С. 37-43.

3. Подымов В. В. О проверке сильной эквивалентности металинейных унарных рекурсивных программ // Вестник Московского университета. Серия 15. Вычислительная математика и кибернетика. — 2013. — № 1. — С. 21-27.

4. Подымов В. В., Захаров В. А. Полиномиальный алгоритм проверки эквивалентности в модели программ с перестановочными и подавляемыми операторами // Труды Института системного программирования РАН. — 2014. — Т. 26, вып. 3. - С. 145-166.

5. Захаров В. А., Подымов В. В. Об эквивалентности металинейных унарных рекурсивных программ // Материалы XI Международного семинара "Дискретная математика и ее приложения", посвященного 80-летию со дня рождения академика О. Б. Лупанова. — 2012. — С. 157-159.

6. Подымов В. В. О проверке эквивалентности последовательных и рекурсивных программ на упорядоченных полугрупповых шкалах // Материалы X Международной конференции "Интеллектуальные системы и компьютерные науки". - 2011. - С. 295-298.

7. Подымов В. В. Быстрый алгоритм проверки эквивалентности программ с коммутативными и подавляемыми операторами // Материалы XVII международной конференции "Проблемы теоретической кибернетики" — 2014. — С. 234-237.

Напечатано с готового оригинал-макета

Подписано в печать 20.01.2015 г. Формат 60x90 1/16. Усл.печл. 1,0. Тираж 100 экз. Заказ 008.

Издательство ООО "МАКС Пресс" Лицензия ИД N 00510 от 01.12.99 г. 119992, ГСП-2, Москва, Ленинские горы, МГУ им. М.В. Ломоносова, 2-й учебный корпус, 527 к. Тел. 8(495)939-3890/91. Тел./факс 8(495)939-3891.