Система автоматического синтеза функциональных программ

• Автор: Корухова, Юлия Станиславовна
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2005
• Место защиты: Москва
• Количество страниц: 124 с. : ил.

Оглавление

Введение. Существующие подходы к синтезу программ.

Дедуктивный синтез программ.

Синтез программ, содержащих цикл или рекурсию.

Автоматизированные системы доказательств

Системы автоматического синтеза с использованием планирования доказательств

Постановка задачи

Содержание работы

Глава 1. Метод дедуктивных таблиц

1.1 Основные понятия.

1.2 Свойства дедуктивных таблиц

1.3 Дедуктивные правила
1.4 Порождение программы.
1.5 Проблема комбинаторного взрыва.
Глава 2. Доказательство с использованием волновых правил.
2.1 Системы переписывания
2.2 Формирование волновых правил.
2.2.1 Основные понятия, связанные с волновыми правилами
2.2.2 Алгоритм унификации различий.
2.3 Применение волновых правил с распространением волн наружу
2.4 Применение волновых правил с распространением фронта волны внутрь
2.5 Преимущества применения волновых правил. Особенности применения волновых правил для синтеза программ.
Глава 3. Автоматизация синтеза программ в дедуктивной таблице
3.1 Эвристики, ограничивающие число применимых правил
3.1.1 Учт полярности логических выражений.
3.1.2 Учт типов термов при выводе.
3.2 Применение волновых правил для планирования доказательства в дедуктивной таблице
3.2.1 Описание метода
3.2.2 Построение волновых правил.
3.2.3 Доказательство шага индукции с помощью волновых правил.
3.2.4 Применение волновых правил для построения пути доказательства
Глава 4. Система синтеза функциональных программ АЛИСА.
4.1 Язык спецификаций
4.2 Язык синтезируемых программ
4.3 Использование встроенных механизмов языка Пролог для реализации системы
4.4 Архитектура и схема работы системы.
4.5 Внутреннее представление дедуктивных таблиц
4.6 Реализация дедуктивных правил
4.7 Стратегия применения дедуктивных правил
4.8 Реализация волновых правил.
4.9 Результаты синтеза в системе АЛИСА.
Заключение.
Литература


При возникновении подзадачи с той же теоремой, что и доказываемая, возможно построение рекурсивной процедуры. Но на практике эта возможность не используется, так как в этом случае сильно затрудняется проверка завершаемости работы построенной рекурсивной процедуры. Циклы же в системе ПРИЗ используются довольно часто. В системе ПРИЗ, таким образом, используется метод, дающий возможность синтезировать последовательность операторов, условное выражение и цикл. Кроме того, метод структурного синтеза позволяет сократить перебор предложений вычислимости, так как для каждой задачи строится вычислительная модель, а, следовательно, подбираются только подходящие аксиомы. Однако значительная часть работы для такого синтеза (описание вычислительной модели) должна быть проделана заранее. При решении задачи из другой области соответствующая дополнительная информация должна снова добавляться в систему и её становится сложно расширять. Вариант правила вывода, позволяющий получить рекурсивное обращение к функции, был предложен Манной и Валдингером в методе дедуктивных таблиц [Manna and Waldinger, , ]. Суть метода заключается в следующем: каждому шагу доказательства, проводимого на основе известных аксиом и правил вывода, соответствует определенный шаг синтеза. Лиспа [McCarthy, ], [Хювенен и Сеппянен, ]). С помощью метода дедуктивных таблиц были синтезированы, например, программы сортировки для списков [Traugott, ] и алгоритм унификации [Nardi, ], но этот синтез проводился вручную. В интерактивном варианте метод дедуктивных таблиц был реализован в системе, описанной в работе [Burback et al. Применение дедуктивного правила эта система выполняла автоматически, но выбор правила на каждом шаге доказательства делал пользователь. При проведении доказательства обычно находится несколько правил вывода, которые могут быть применены в текущей ситуации, однако далеко не многие из них ведут к успешному завершению доказательства, и возникает огромный перебор вариантов. Для сокращения перебора либо доказательство должно быть сделано интерактивным, направляемым пользователем, либо необходимо использование дополнительных эвристик. Система, реализующая такой метод, автоматически выполняет рутинные операции, а решения о порядке применения правил, построении стратегии доказательства принимает пользователь. Одной из первых таких систем была система Nqthm [Boyer and Moore, ]. Другой подход - направление доказательства с помощью дополнительной информации, задаваемой по ходу его выполнения - был использован в системе Isabelle [Paulson, ]. В ней были разработаны так называемые тактики и тактические конструкции, позволяющие управлять процессом логического вывода при автоматизированном проведении доказательства. Тактика представляет собой объединение нескольких шагов доказательства в единое целое. Применение той или иной тактики, откат доказательства на предыдущий шаг, составление цепочки доказательств из нескольких тактик с помощью тактических конструкций - задачи, которые выполняет пользователь системы. Состояние доказательства в системе представляет собой некоторую теорему. Тактики - это функции, преобразующие это состояние. Тактики резолюции, просматривая список правил, возвращают следующее состояние для каждой комбинации правила и унификатора. Тактики предположения выполняют присваивание и возвращают следующее состояние для каждой комбинации предположения и унификатора. Если применить тактику невозможно, система возвращает fail. Тактика пытается решить подцель i. Тактика резолюции, thms — это список правил, которые решают i-ю подцель. Для каждого из этих правил резолюция формирует следующее состояние, унифицируя заключение с подцелью, и подставляет конкретизированную предпосылку на место подцели. Результат применения будет ложным, если ни для одного правила не удалось создать следующее состояние. В системе предоставлена возможность комбинирования тактик с помощью специальных операторов - тактических конструкций. Основные тактические конструкции: THEN, ORELSE, REPEAT.