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

• Автор: Подымов, Владислав Васильевич
• Шифр специальности: 01.01.09
• Научная степень: Кандидатская
• Год защиты: 2014
• Место защиты: Москва
• Количество страниц: 164 с. : ил.

Оглавление

Глава 1. Введение

1.1. Проблема эквивалентности программ

1.2. Теория схем программ

1.3. Быстрые алгоритмы проверки эквивалентности

1.4. Результаты исследования

1.5. Новизна полученных результатов

1.5.1. Последовательные программы

1.5.2. Унарные рекурсивные программы

1.6. Структура работы

Глава 2. Общие понятия и обозначения
2.1. Последовательности, слова
2.2. Порядки
2.3. Автоматы
2.4. Моноиды
2.5. Коммутативность и подавление
Глава 3. Модели программ
3.1. Пропозициональные последовательные программы
3.1.1. Синтаксис
3.1.2. Интерпретации
3.1.3. Реализуемость трасс в интерпретации
3.1.4. Эквивалентность и совместность
3.1.5. Утверждения
3.2. Унарные рекурсивные программы
3.2.1. Синтаксис
3.2.2. Реализуемость трасс в интерпретации
3.2.3. 3 Эквивалентность и совместность
3.2.4. Линейность и металинейность
3.2.5. Классификация заголовков
3.2.6. Нормальная форма
3.2.7. Утверждения
Глава 4. Формулировка результатов и методология исследования программ
4.1. Формулировка результатов
4.2. Метод совместных вычислений
Глава 5. Эквивалентность пропозициональных последовательных программ на шкалах с коммутативностью и подавлением
5.1. Упорядоченность моноидов с коммутативностью и подавлением .
5.2. Основные свойства упорядоченных моноидов с коммутативно-
стью и подавлением
5.3. Распознавание подавления операторов
5.4. Граф совместных вычислений
5.5. Эффекты подавления
5.6. Ограничение числа вершин графа совместных вычислений
5.7. Полиномиальная разрешимость проблемы эквивалентности
Глава 6. Эквивалентность линейных унарных рекурсивных программ на упорядоченных полугрупповых шкалах
G.I. Критериальные системы
6.2. Граф совместных вычислений
6.3. Разрешимость проблемы эквивалентности
6.4. Полиномиальная разрешимость проблемы эквивалентности
Глава 7. Сильная эквивалентность металинейных унарных ре-

курсивных программ
7.1. Вспомогательные понятия и утверждения
7.2. Граф совместных вычислений
7.3. Ограничение числа вершин графа совместных вычислений
7.4. Полиномиальная разрешимость проблемы эквивалентности . . .
Глава 8. Заключение
Список литературы

Таким образом, шкала X придаст каждому оператору а значение функции преобразования состояний данных, а интерпретациях, помимо этого, оценивает истинность логических условий в каждом состоянии данных:
ô(s) = T.R{s,a), p(s) = (р G Z.Ç(s)).
Далее будут рассматриваться только шкалы над алфавитом операторов D и интерпретации над алфавитами операторов £) и логических условий £, поэтому упоминание этих алфавитов при задании шкал и интерпретаций будет опускаться. Интерпретации, включающие в себя шкалу X, будем называть основанными на шкале X, а также Е-интерпретациями.
Рассмотрим шкалу X. Обобщим функцию X.R с множества Ù на множество £)*:
E.R*{s, А) = 5,
E.R*(s, ha) — X.X(X.X*(s, h) ,а) , где а G О и h G D*. Содержательно, значением E.R*(s,g) является состояние данных шкалы X, в которое приводит выполнение цепочки g из состояния s. Если контекстом однозначно определяется шкала X, то вместо X. R*{J-.s, д) будем писать
Существует множество ограничений на структуру шкал. В рамках диссертации представляют интерес следующие ограничения:
• шкала X является полугрупповой, если существует копечнопорожденный моноид A4 — (Е, о) над алфавитом О (далее называемый определяющим моноидом), такой что Х.5 = Е, X.s = (Л) и X.i?(s, о) = s о (а);
• шкала X является упорядоченной, если для любых цепочек h G £>*, g G D+ верно: {kg} ^ [/1].
Содержательно, состояния данных полугрупповой шкалы образуют полугруппу, а состояния данных упорядоченной шкалы, достижимые из начального, частично упорядочены относительно функции преобразования данных.