Введение
1 Позитивная суперкомпиляция и анализ программ 19
1.1 Исторический обзор 20
1.1.1 Суперкомпиляция Рефала 20
1.1.2 Суперкомпиляция функциональных языков первого порядка 22
1.1.3 Суперкомпиляции императивных языков 27
1.1.4 Суперкомпиляция функциональных языков высшего порядка 27
1.1.5 Другие работы 29
1.2 Суперкомпиляция функционального языка первого порядка 30
1.2.1 Примеры суперкомпиляции 32
1.2.2 Синтаксис и семантика языка SLL 38
1.2.3 Обобщение и гомеоморфное вложение SLL-выражений 41
1.2.4 Построение дерева процессов 44
1.2.5 Построение частичного дерева процессов 46
1.3 Анализ состояния дел в суперкомпиляции с точки зрения трансформационного анализа программ 50
1.4 Выводы 51
2 Язык HLL: синтаксисисемантика 52
2.1 Формализация языка HLL 52
2.2 Синтаксис языка HLL 54
2.3 Подстановка 58
2.4 Семантика языка HLL 59
2.5 Типизация 62
2.6 Алгебра HLL-выражений 64
2.7 Выводы 65
3 Структура суперкомпилятора HOSC 67
3.1 Устранение локальных определений 67
3.2 Представление множеств 68
3.3 Построение частичного дерева процессов 69
3.4 Генерация остаточной программы 73
3.5 Отношение транформации HOSC 75
3.6 Выводы 76
4 Корректность суперкомпилятора HOSC 77
4.1 Операционная теория улучшений 78
4.2 Корректность отношения трансформации HOSCQ 80
4.3 Корректность отношения трансформации HOSCi/2 85
4.3.1 Пример сведения отношения HOSC\/2 к отношению
4.4 Корректность отношения трансформации HOSC 89
4.5 Типизация и корректность 89
4.6 Выводы 91
5 Схема суперкомпилятора HOSC 93
5.1 Язык HLL: вложение и обобщение 93
5.2 Параметризованный HLL суперкомпилятор 97
5.2.1 Конкретные HLL суперкомпиляторы 101
5.3 Сравнение суперкомпиляторов 102
5.4 Усиление уточненного вложения с учетом типизации . 104
5.5 Выводы 105
6 Завершаемость суперкомпилятора HOSC 106
6.1 Абстрактные преобразователи программ 107
6.2 Гомеоморфное вложение 110
6.2.1 Связанные переменные 110
6.2.2 Высший порядок и арность 111
6.3 Вполне-квазиупорядочение 113
6.3.1 Замена case-выражений на конструкторы 114
6.3.2 Замена имен переменных на индексы де Брюина 114
6.3.3 Расширенные индексы де Брюина 116
6.3.4 Проблема арности 117
6.3.5 Кодировка 124
6.4 Завершаемость суперкомпилятора SC 124
6.5 Пересмотр обработки ситуации зацикливания 127
6.6 Завершаемость остальных суперкомпиляторов 129
6.7 Выводы 130
7 Распознавание эквивалентности выражений 132
7.1 Моделирование знаний в виде программ 133
7.2 Доказательство свойств программ методами суперкомпиля-
7.3 Доказательство эквивалентности выражений 138
7.3.1 Доказательство эквивалентности выражений, основанное на равенстве 138
7.3.2 Доказательство эквивалентности выражений, основанное на нормализации 140
7.3.3 Генерация множеств эквивалентных выражений . 144
7.4 Проверка корректности реализаций монад 145
7.5 Выводы 149
8 Метод многоуровневой суперкомпиляции 150
8.1 Многоуровневая суперкомпиляция 151
8.1.1 Накапливающий параметр: базовая суперкомпиляция 153
8.1.2 Накапливающий параметр: применение леммы 154
8.1.3 Соединение суперкомпиляторов, переход к многоуровневой суперкомпиляции 155
8.1.4 Генерация множества остаточных программ 157
8.1.5 Несколько открытых вопросов 157
8.2 Корректность = эквивалентность + улучшение 159
8.2.1 Распознавание улучшающих лемм 159
8.3 Модельный двухуровневый суперкомпилятор 162
8.4 Примеры 164
8.4.1 Суперкомпиляция нелинейного выражения 164
8.4.2 Накапливающий параметр 169
8.4.3 Улучшение асимптотики программ 170
8.5 Выводы 173
Заключение 175
Список литературы 177
