Ви є тут

Выявление и доказательство свойств функциональных программ методами суперкомпиляции

Автор: 
Ключников Илья Григорьевич
Тип роботи: 
кандидатская
Рік: 
2010
Артикул:
572548
179 грн
Додати в кошик

Вміст

Оглавление
Введение
1 Позитивная суперкомпиляция и анализ программ
1.1 Исторический обзор.
1.1.1 Суперкомпиляция Рефала.
1.1.2 Суперкомпиляция функциональных языков первого
порядка
1.1.3 Суперкомпиляции императивных языков
1.1.4 Суперкомииляция функциональных языков высшего порядка
1.1.5 Другие работы
1.2 Суперкомпиляция функционального языка первого порядка
1.2.1 Примеры су пер компиляции
1.2.2 Синтаксис и семантика языка ЭЬЬ
1.2.3 Обобщение и гомеоморфное вложение ЗЬЬвыражений
1.2.4 Построение дерева процессов.
1.2.5 Построение частичного дерева процессов
1.3 Анализ состояния дел в суперкомпиляции с точки зрения
трансформационного анализа программ
1.4 Выводы.
2 Язык НЬЬ синтаксис и семантика
2.1 Формализация языка НЬЬ.
2.2 Синтаксис языка НЬЬ
2.3 Подстановка1
2.4 Семантика языка НЬЬ
2.5 Типизация
2.6 Алгебра НЫгвыражсний.
2.7 Выводы.
3 Структура су пер компилятора НО в С
3.1 Устранение локальных определений.
3.2 Представление множеств.
3.3 Построение частичного дерева процессов
3.4 Генерация остаточной программы
3.5 Отношение трансформации ЫОйС.
3.6 Выводы.
4 Корректность суперкомпилятора НОвС
4.1 Операционная теория улучшений
4.2 Корректность отношения трансформации НО в Со.
4.3 Корректность отношения трансформации НОЗС2.
4.3.1 Пример сведения отношения НОБСх2 к отношению НОБСо.
4.4 Корректность отношения трансформации ЯС
4.5 Типизация и корректность.
4.6 Выводы.
5 Схема суперкомпилятора НОЭС
5.1 Язык НЫ. вложение и обобщение.
5.2 Параметризованный НЬЬ суперкомпплятор.
5.2.1 Конкретные НЬЬ суперкомпиляторы.
5.3 Сравнение суперкомпиляторов
5.4 Усиление уточненного вложения с учетом типизации
5.5 Выводы.
6 Завершасмость суперкомпилятора НОЭС
6.1 Абстрактные преобразователи программ.
6.2 Гомеоморфное вложение
6.2.1 Связанные переменные
6.2.2 Высший порядок и арность.
6.3 Вполнеквазиупорядочеиие .
6.3.1 Замена сазевыражений на конструкторы
6.3.2 Замена имен перехмеиыых на индексы де Брюина . . .
6.3.3 Расширенные индексы де Брюина
6.3.4 Проблема арности.
6.3.5 Кодировка
6.4 Завершаемость суперкомпилятора БС .
6.5 Пересмотр обработки ситуации зацикливания
6.6 Завершаемость остальных суперкомпиляторов.
6.7 Выводы
7 Распознавание эквивалентности выражений
7.1 Моделирование знаний в виде программ
7.2 Доказательство свойств программ методами су пер компиляции .
7.3 Доказательство эквивалентности выражений
7.3.1 Доказательство эквивалентности выражений, основанное на равенстве
7.3.2 Доказательство эквивалентности выражений, основанное на нормализации.
7.3.3 Генерация множеств эквивалентных выражений . . .
7.4 Проверка корректности реализаций монад .
7.5 Выводы
8 Метод многоуровневой суперкомпиляции
8.1 Многоуровневая суперкомпиляция
8.1.1 Накапливающий параметр базовая суперкомпиляция
8.1.2 Накапливающий параметр применение леммы
8.1.3 Соединение суперкомпиляторов, переход к многоуровневой суперкомпиляции
8.1.4 Генерация множества остаточных программ
8.1.5 Несколько открытых вопросов
8.2 Корректность эквивалентность 4 улучшение.
8.2.1 Распознавание улучшающих лемм
8.3 Модельный двухуровневый суперкомпилятор.
8.4 Примеры.
8.4.1 Суперкомпиляция нелинейного выражения
8.4.2 Накапливающий параметр.
8.4.3 Улучшение асимптотики программ.
8.5 Выводы
Заключение
Список литературы