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

• Автор: Ключников, Илья Григорьевич
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2010
• Место защиты: Москва
• Количество страниц: 189 с. : ил.

Оглавление
Введение

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 Выводы
Заключение
Список литературы


Вместе с первым приемом это позволяет приводить одинаковые по смыслу, но текстуально разные программы к одной и той же синтаксической форме. В отличие от других работ, где сунеркомпилятор рассматривается как фиксированная монолитная конструкция, в данной работе вначале определяется структура суперкомпилятора НОБС в виде отношения трансформации НОБС, - фиксируются методы (без деталей реализации) построения частичного дерева процессов и преобразования частичного дерева процессов в остаточную программу, доказывается корректность отношения трансформации НОБС. То есть доказывается корректность не конкретного алгоритма, а мнооюества алгоритмов, удовлетворяющих отношению трансформации НОБС. Доказательство корректности отношения трансформации НОЗС опирается на операционную теорию улучшений Дэвида Сэндса. Стандартных'! Сэндса). В работе показана корректность, трансформации HOSC в общем случае -включая те случаи, когда остаточная. Сэндса) исходной программы. Все определенные далее алгоритмы суперкомпиляции удовлетворяют отношению трансформации HOSC и, следовательно, корректны. Язык Haskell является функциональным языком высшего порядка. На момент начала диссертационной работы методы и алгоритмы супсрком-пиляции для языков высшего порядка были слабо разработаны, - в существовавших работах использовались алгоритмы суперкомпиляции для языка первого порядка, адаптированные для языков высшего порядка, не учитывающие всех синтаксических и семантических особенностей языков высших порядков. Сделана ревизия обработки ситуации зацикливания, - использование A-абстракций и функций как данных позволяет писать рекурсивные “функции” без явного использования рекурсии. Как результат во время построения дерева процессов необходимо чаще делать проверку на возможное зацикливание. В выражениях присутствуют связанные переменные: сделаны ревизии гомеоморфного вложения и обобщения, учитывающие свойства связанных переменных. Классическое гомеоморфное вложение является вполне-квазиупорядо-чением на всем множестве выражений языка при использовании конечного числа конструкторов и функций. Уточненное гомеоморфное вложение не является вполне-квазиупорядочением на всем множестве выражений языка. Однако, как показано в работе, уточненное гомеоморфное вложение является вполне-квазиупорядочением множестве выражений, возникающих при построепии дерева процессов, что достаточно для доказательства завершаемости алгоритмов су пер компилятора HOSC. В результате обобщения в дереве процессов появляются лишние трассы и как результат в остаточной программе появляется недостижимый код, который, как правило, затрудняет анализ остаточной программы. Чем меньше в остаточной программе недостижимого кода, тем легче опа поддается анализу. Цель предложенного метода многоуровневой суперкомпиляции - получить в результате су пер компиляции программу с как можно меньшим объемом недостижимого кода. Средство достижения цели - избежать (или как минимум отложить) обобщения конфигураций (“уход из под свистка”) с помощью замены конфигурации, вынуждающей суперкомпилятор сделать обобщение на эквивалентную ей, которая позволяет продвинуться дальше без обобщений. Эквивалентные конфигурации (для замены) распознаются методом нормализацией через суперкомпиляцию. Корректность многоуровневой суиеркомпиляции обеспечивается тем, что конфигурация может заменяться только на “улучшение” (в терминологии Сэндса). Предложен алгоритм распознавания улучшающих лемм, основанный на аннотировании остаточной программы дополнительной информацией о том, насколько быстро исполнялась исходная программа. В результате задача распознавания улучшающих лемм сводится к простому синтаксическому сравнению двух остаточных программ. Диссертационная работа дает положительный ответ па вопрос о возможности использования суперкомпиляции для трансформационного анализа программ. Па основе разработанных алгоритмов и методов создан экспериментальный суперкомпнлятор HOSC для ядра языка Haskell. Показано, что распознавание эквивалентных выражений методом нормализации суперкомниляцией может происходить в полностью автоматическом режиме.