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

На современном этапе развития программирования компьютеры всё больше начинают применяться не только на этапе кодирования программы, но и во время постановки задачи, для решения которой требуется написать программу. В пятидесятые годы 20-го века, когда только приступали к автоматизации программирования, явно выделялись две фазы программирования. Под автоматизацией первой фазы подразумевалось автоматическое получение алгоритма. Вторая фаза заключалась в получении машинной программы по сформулированному алгоритму. В течение тридцати лет автоматизировалась в основном только вторая фаза. С появлением новых разработок по искусственному интеллекту и развитием технологии программирования стала возможной и автоматизация первой фазы. В 70-е годы появилась самостоятельная область исследований — автоматический синтез программ. Под синтезом понимается получение текста программы на основе информации, описывающей эту программу.

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

— дедуктивный, при котором построение программы проводится на основе описания ее цели, заданной в виде спецификации (описания задачи). При таком подходе используется конструктивное доказательство утверждения о том, что решение задачи существует, и из него извлекается требуемая программа;

— индуктивный, при котором программа строится по примерам, непосредственно задающим ответ для некоторых исходных данных;

— трансформационный, где программа получается путем преобразования исходного описания задачи по правилам, совокупность которых представляет знания о решении задач. Трансформационный синтез позволяет получать из менее эффективных программ эквивалентные им, но более эффективные.

В данной работе мы будем рассматривать дедуктивный подход. Преимущество данного подхода в том, что для синтеза используются методы, для которых формально доказано, что они порождают программу, соответствующую спецификации. Такая программа в дальнейшем не требует верификации, поэтому актуальной является задача разработки методов и алгоритмов, позволяющих проводить дедуктивный синтез автоматически.

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

При дедуктивном подходе путь от задачи к программе выглядит так: описание задачи теорема существования решения доказательство теоремы программа.

Описание задачи содержится в спецификациикроме того, используется некоторый набор аксиом, задающих свойства предметной области. Спецификация формулирует цель программы, описывая связь между входными и выходными данными. Хорошая спецификация близка к намерениям пользователя, понятна и читаема. Спецификация рассматривается как теорема существования некоторого объекта (выхода программы). Для спецификации-теоремы строится конструктивное доказательство. Такое доказательство, утверждая о существовании объекта, должно предъявлять способ его вычисления, по которому и будет напрямую сформирован текст программы на некотором языке программирования.

Задача дедуктивного синтеза программ, таким образом, напрямую связана с задачей доказательства теорем. Если же доказательство выполняется автоматически, то автоматически будет получена программа, точно соответствующая описанию задачи. Работа человека в этом случае сводится только к корректному описанию задачи.

В дальнейшем в работе будем подразумевать под термином синтез именно дедуктивный синтез программ.

Одной из первых систем синтеза, в которой был применен такой подход, была система PROW [Lee et al., 1974] Спецификации в этой системе записываются в следующем виде:

V х (Р (х) => 3 z. R (x, z)).

Эта запись означает, что по заданному х, удовлетворяющему входному условию программы Р (х), требуется вычислить z, удовлетворяющее условию R (х, z), которое связывает вход х и выход z программы.

Доказательство теоремы строится в исчислении предикатов первого порядка на основе метода резолюций [Robinson, 1965].

Система PROW показала возможность синтеза линейных и ветвящихся программ. Для синтеза рекурсии или цикла необходимо было использовать особое правило вывода, которое опирается на метод математической индукции.

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

Выявление правил логики, лежащих в основе построения циклических и рекурсивных программ, было важным шагом в автоматизации синтеза программ. Для появления таких структур в программе требовалось проводить доказательство по индукции.

В системе ПРИЗ [Тыугу, 1984] была реализована возможность автоматического синтеза программ, содержащих циклы. В системе заранее был задан набор управляющих структур цикла для каждой возможной версии математической индукции. Построение тела цикла при этом рассматривалось как подзадача.

Синтез в системе ПРИЗ рассматривается как составление алгоритма решения задачи на так называемой вычислительной модели. Вычислительная модель представляет собой модель предметной области и формируется заранее. Она состоит из совокупности переменных, соответствующих понятиям предметной области, и отношений вычислимости. Каждое из отношений вычислимости связывает значения нескольких переменных модели и интерпретируется так: по известным значениям одних переменных (являющихся входными) можно вычислить значения других (выходных) переменных. Задача на вычислительной модели состоит в нахождении значений некоторых переменных по известным значениям других переменных на основе отношений вычислимости. Спецификация, записанная на специальном языке УТОПИСТ, состоит из двух частей: декларативной (указание значений входных переменных) и процедурной (которая представляет собой оператор задачи с перечисленными в нём выходными переменными). Дополнительно в декларативной части спецификации могут быть заданы ещё некоторые отношения между переменными.

Метод построения программы в системе ПРИЗ предполагает три этапа работы:

1. Перевод спецификации во внутреннее представление. На этом этапе, исходя из спецификации и отношений вычислимости вычислительной модели, формируется набор отношений, представляющий вычислительную модель решаемой задачи.

2. Планирование решения задачи. На этом этапе применяется либо метод «прямой волны» (при котором проводится преобразование переменных, начиная от входных, с учётом отношений вычислимости, до получения выходных переменных), либо метод «обратной волны» (при движении в обратном направлении — от выходных переменных к входным).

3. Запись алгоритма на одном из входных (целевых) языков системы.

Такой вариант метода синтеза называется структурным синтезом. При исследовании логических основ этого метода синтез на вычислительных моделях был тоже представлен как доказательство математической теоремы существования решения в теории специального вида. Формулы этой логической теории состоят из логических связок и отношений вычислимости, имеющих вид u ->f v (смысл этой записи: по и вычислимо v применением функции f). Тогда теорему существования решения задачи можно записать следующим образом: Б f. (u -«f v). Задача состоит в выводе этой теоремы из аксиом, задающих отношения вычислимости.

Стратегия поиска доказательства в случае предложений вычислимости простейшего вида u -«f v заключается в последовательном выводе на основе этого правила и аксиом (известных отношений вычислимости) всех возможных новых предложений, пока не будет выведено предложение, представляющее собой доказываемую теорему.

Ветвление появляется в программе, когда теорема существования не может быть доказана только на основе предложений простейшего вида и необходимо использовать предложения с условиями вычислимости. Для каждого такого условного предложения синтезируется ветвление, а ветви условного выражения строятся рекурсивным применением описываемого алгоритма при допущении истинности или, соответственно, ложности условия вычислимости.

В доказательство может быть включено предложение вычислимости с условием в виде теоремы существования решения другой задачи (подзадачи). Тогда в синтезируемой программе должен появиться вызов процедуры, реализующей решение этой подзадачи. При возникновении подзадачи с той же теоремой, что и доказываемая, возможно построение рекурсивной процедуры. Но на практике эта возможность не используется, так как в этом случае сильно затрудняется проверка завершаемости работы построенной рекурсивной процедуры. Циклы же в системе ПРИЗ используются довольно часто.

В системе ПРИЗ, таким образом, используется метод, дающий возможность синтезировать последовательность операторов, условное выражение и цикл. Кроме того, метод структурного синтеза позволяет сократить перебор предложений вычислимости, так как для каждой задачи строится вычислительная модель, а, следовательно, подбираются только подходящие аксиомы. Однако значительная часть работы для такого синтеза (описание вычислительной модели) должна быть проделана заранее. При решении задачи из другой области соответствующая дополнительная информация должна снова добавляться в систему и её становится сложно расширять.

Вариант правила вывода, позволяющий получить рекурсивное обращение к функции, был предложен Манной и Валдингером в методе дедуктивных таблиц [Manna and Waldinger, 1980, 1992]. Суть метода заключается в следующем: каждому шагу доказательства, проводимого на основе известных аксиом и правил вывода, соответствует определенный шаг синтеза. Применяя дедуктивные правила, можно получить три базовые конструкции функционального языка программирования: применение функции, условное выражение и рекурсию, которые напрямую переводятся в конструкции функционального языка программирования (например, Лиспа [McCarthy, 1960], [Хювенен и Сеппянен, 1990]).

С помощью метода дедуктивных таблиц были синтезированы, например, программы сортировки для списков [Traugott, 1989] и алгоритм унификации [Nardi, 1989], но этот синтез проводился вручную. В интерактивном варианте метод дедуктивных таблиц был реализован в системе, описанной в работе [Burback et al., 1990]. Применение дедуктивного правила эта система выполняла автоматически, но выбор правила на каждом шаге доказательства делал пользователь.

При проведении доказательства обычно находится несколько правил вывода, которые могут быть применены в текущей ситуации, однако далеко не многие из них ведут к успешному завершению доказательства, и возникает огромный перебор вариантов. Для сокращения перебора либо доказательство должно быть сделано интерактивным, направляемым пользователем, либо необходимо использование дополнительных эвристик.

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

Один из методов, позволяющих сократить перебор вариантов применения правил вывода при построении доказательства, подразумевает направление этого доказательства человеком. Система, реализующая такой метод, автоматически выполняет рутинные операции, а решения о порядке применения правил, построении стратегии доказательства принимает пользователь. Одной из первых таких систем была система Nqthm [Boyer and Moore, 1979]. Часть работы при построении доказательств в этой системе выполняется автоматически с помощью метода резолюций, некоторых методов преобразования равенств и эвристик для структурной индукции, но взаимодействие с человеком требуется при поиске вывода, так как системе нужно явно указывать некоторые промежуточные утверждения, используемые при доказательстве как вспомогательные леммы.

Другой подход — направление доказательства с помощью дополнительной информации, задаваемой по ходу его выполнения — был использован в системе Isabelle [Paulson, 1988]. В ней были разработаны так называемые тактики и тактические конструкции, позволяющие управлять процессом логического вывода при автоматизированном проведении доказательства. Тактика представляет собой объединение нескольких шагов доказательства в единое целое. Применение той или иной тактики, откат доказательства на предыдущий шаг, составление цепочки доказательств из нескольких тактик с помощью тактических конструкций — задачи, которые выполняет пользователь системы.

Состояние доказательства в системе представляет собой некоторую теорему. Тактики — это функции, преобразующие это состояние. Тактики резолюции, просматривая список правил, возвращают следующее состояние для каждой комбинации правила и унификатора. Тактики предположения выполняют присваивание и возвращают следующее состояние для каждой комбинации предположения и унификатора. Если применить тактику невозможно, система возвращает fail.

Примеры тактик: assume tас i Тактика пытается решить подцель i. resolvetac thms i Тактика резолюции, thms — это список правил, которые решают i-ю подцель. Для каждого из этих правил резолюция формирует следующее состояние, унифицируя заключение с подцелью, и подставляет конкретизированную предпосылку на место подцели. Результат применения будет ложным, если ни для одного правила не удалось создать следующее состояние.

В системе предоставлена возможность комбинирования тактик с помощью специальных операторов — тактических конструкций. Основные тактические конструкции: THEN, ORELSE, REPEAT. tacl THEN tac2 Конструкция последовательного применения: применяется tacl, затем tac2. Если применение одной из тактик возвращает fail, то происходит возврат к начальному состоянию. tacl ORELSE tac2 Применяется taclесли применение прошло успешно, то tас2 не применяется, иначе же применяется tac2. REPEAT tac Тактика tac применяется до тех пор пока не вернет fail. Для взаимодействия с пользователем в системе использован язык Standart ML [Harper, 1989]. В нем предоставлена возможность управления контекстом доказательства. Основными из возможностей являются следующие: Goal f Начать доказательство теоремы f. by tacПрименить тактику tac к текущему состоянию доказательства, undo () — Откатить состояние доказательства к предыдущему, result () — Возвращает теорему, которая уже доказана и fail, если еще есть недоказанные подцели. qued name Обычный путь завершения доказательства. Доказанная теорема сохраняется в базе данных Isabelle.

В основе системы Isabelle лежит металогика, в которой объектные логики (например, логика первого порядка, теория множеств) могут быть представлены как её частные случаи. В металогике имеется набор аксиом, которые, будучи конкретизированными для объектной логики, становятся правилами вывода. Они и используются для проведения доказательств утверждений рассматриваемой объектной логики.

В работе [Ayari and Basin, 2001] описана реализация метода дедуктивных таблиц с помощью логики высшего порядка в системе Isabelle, таким образом, система может быть использована для синтеза программ. Вместо перебора вариантов применения правил перебор происходит на более высоком уровнепри выборе тактики доказательства. Недостатком такого подхода, на наш взгляд, является тот факт, что для многих примеров надо придумывать свою тактику доказательства, какой-либо универсальной тактики нет.

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

Для сокращения перебора в некоторых системах применяется планирование доказательства. Суть его заключается в следующем: сначала составляется план — схема доказательства, записанная на более высоком уровне абстракции, а затем по нему строится уже само доказательство, в котором строго доказываются шаги, оставшиеся недоказанными при построении плана. Во многих системах план доказательства строится, исходя из знаний о предметной области, в которой проводятся рассуждения. При дедуктивном синтезе программ, содержащих рекурсию, возникает доказательство по индукции. Рассмотрим системы, в которых планирование применяется для сокращения перебора при построении доказательства по индукции. Это системы автоматического доказательства Oyster/Clam и A.CLAM.

Oyster/Clam [Bundy et al., 1990] представляет собой объединение двух систем, Clam — планировщик доказательств, он строит подходящую тактику, которая потом выполняется системой Oyster.

Oyster — интерактивный редактор для построения доказательства, реализованный на Прологе. Он основан на логике высшего порядка, включающей индукцию. Система содержит определения основных конструкций и библиотеку теорем.

Тактики системы Oyster записаны на Прологе. Предикаты, описывающие свойства проводимого доказательства, доступны пользователю. Примитивные шаги доказательства выполняются с помощью применения только правил доказательства. Тактики можно комбинировать, используя специальные тактические конструкции. Встроенные механизмы Пролога (автоматическое сопоставление и поиск с возвратом) помогают автоматизировать поиск доказательства. Система Oyster используется как для доказательства теорем, так и для синтеза программ.

Система Clam позволила сделать из интерактивной системы Oyster систему автоматического доказательства теорем. Для каждой тактики из системы Oyster записывается спецификация для Clam. Эти спецификации называются методами. Метод состоит из предусловия, входной формулы, выходной формулы и постусловия. Метод может быть применен к некоторой формуле, если она может быть сопоставлена с входной формулой и предусловие выполнено. Предусловия, сформулированные на языке металогики, описывают некоторые синтаксические свойства входной формулы. Используя предусловие и входную формулу, Clam определяет, можно ли применить тактику, до её непосредственного применения в Oyster. Выходная формула дает примерный шаблон получаемого в результате применения тактики результата, а постусловие описывает синтаксические свойства входной формулы. Метод представляет собой некоторый эвристический оператор, который описывает необходимые свойства тактики, не вдаваясь в детальные вычисления, требующие значительного времени.

План доказательства система Clam строит следующим образом. На каждом шаге по внешнему виду входной формулы с учётом предусловия система определяет, какой метод может быть применён. В результате его применения получается выходная формула и постусловие. Данная выходная формула является входной для следующего шага доказательства. Этот процесс продолжается до тех пор, пока все формулы не будут доказаны. Так как в некоторых ситуациях несколько методов могут оказаться применимыми, возникает дерево доказательства. На практике при использовании стратегии поиска вглубь по дереву доказательства результат получается за приемлемое время. По рассматриваемому пути доказательства для каждого метода Clam, выполняется соответствующая тактика Oyster.

Система автоматического синтеза программ XClam [Lacey et al., 2000] расширение системы Clam. Система A-Clam была реализована на языке^Prolog, который позволяет решать задачи на языке логики более высокого порядка, что упрощает, например, работу с кванторами. В то же время, используя AProlog в качестве металогики, система может решать и задачи в области логики предикатов первого порядка.

Ключевая тактика, применяемая в системах Clam и^Clam при доказательстве теорем по индукции, — это применение волновых правил1. В соответствии с ней, при доказательстве шага индукции надо определить различия между гипотезой и заключением индукции, а затем так их преобразовывать, чтобы разница между ними уменьшилась. Для этого применяются только правила преобразования, которые уменьшают различия, таким образом отсекается часть правил, которые, скорее всего, не приведут доказательство к успешному завершению. Это делается с помощью специальных аннотаций на формулах: отмечаются части формул, которые могут быть изменены, и направление изменений. Метод может быть применен не только при выполнении шага индукции, но и при других преобразованиях одной формулы (гипотезы) к другой (цели). Цель преобразуется так, чтобы она содержала пример гипотезы как подвыражение. Тогда мы сможем воспользоваться истинностью гипотезы, что поможет доказать цель. Существенным достоинством такого подхода является значительное сокращение перебора при доказательстве, но использование волновых правил для синтеза осложняется тем, что обычно используемые правила преобразования формируются из определений участвующих в доказательстве объектов, а синтезируемая функция ещё не известна и для неё правила преобразования не могут быть выписаны.

Синтез логических программ с использованием волновых правил был реализован в системе Periwinkle [Kraan et al., 1996]. При синтезе спецификация рассматривается как терема существования объекта (программы), которую надо доказать. Доказываемые свойства заданы в спецификации, а сам объектсинтезируемая программа — обозначается метапеременной и получает свое значение в процессе проведения доказательства. В этой системе заранее задан набор различных схем индукции и схем соответствующих им программ. Задача состоит в выборе подходящей схемы на основе анализа рекурсии. Ограниченный набор схем программ ограничивает и набор задач, которые.

1 Эта тактика в англоязычной литературе называется rippling. может решить система. В частности, система не смогла синтезировать функции сортировки списка и разделения списка на части.

Расширение идеи волновых правил было реализовано в системах INKA [Hutter and Sengler, 1996] и NuPRL [Pientka and Kreitz, 1999]. В системе INKA дополнительно к аннотации различий формул и направлению проведения преобразований задается еще «цвет» аннотации, что вводит новые ограничения. В системе NuPRL особое внимание уделено применению волновых правил для выражений, содержащих метапеременные, поиск значений которых проводится при проведении доказательства двух направлениях: от заключения индукции к гипотезе и, наоборот, от гипотезы в сторону заключения (обратный rippling).

В рассмотренных системах проводилось доказательство, при котором могла быть построена логическая программа. Логическая программа представляет собой некоторую формулировку задачи, а не детальный способ описания её решения. Тогда как на функциональном языке программирования (например, на Лиспе) описывается именно способ решения.

Мы будем использовать волновые правила при синтезе функциональных программ. Эта идея частично была рассмотрена в [Armando et al., 1999], но в этой работе синтез был лишь частично автоматизирован, за счёт того, что автоматически выполнялись некоторые этапы доказательств, а ведущая, направляющая роль — определение последовательности выполнения этих этапов — отводилась человеку. В данной диссертации предлагается подход, который объединяет преимущества нескольких методов синтеза: метода дедуктивных таблиц, позволяющего синтезировать все базовые конструкции функциональной программы и формировать структуру программы в процессе доказательства, а также преимущества применения волновых правил, которые позволяют существенно сократить перебор при доказательстве.

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

Целями диссертации являются:

• разработка нового метода дедуктивного синтеза функциональных программ, позволяющего расширить (по сравнению с известными методами) класс программ, автоматическое построение которых можно осуществлять за приемлемое время;

• разработка и реализация на основе данного метода системы автоматического синтеза программ, которая осуществляет построение функциональных программ на языке Лисп по их формальным спецификациям и заданным аксиомам.

Основой нового метода является метод дедуктивных таблиц, который требуется дополнить рядом эвристик, в том числе волновыми правилами, чтобы сократить перебор вариантов при синтезе.

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

Работа состоит из четырёх глав. В первой главе рассмотрены основы метода дедуктивных таблиц, который является базовым для разработанного в диссертации метода. Во второй главе приведены основные понятия теории применения волновых правил при построении доказательств по индукции. Глава 3 рассказывает о разработанном в диссертации методе синтеза программ. В главе 4 описана реализация системы АЛИСА и результаты экспериментов с ней. Основные выводы работы сформулированы в заключении.

В приложениях содержится полное описание языка спецификаций, по которым осуществляется синтез в системе АЛИСА, информация о встроенных знаниях системы, описание используемого в ней внутреннего представления выражений и термов, примеры синтеза некоторых функций, а также приведён алгоритм унификации различий.

2 Название образовано от Автоматический ЛИсп Синтезатор

Основные результаты диссертационной работы состоят в следующем:

• Предложен новый метод синтеза функциональных программ по их формальным спецификациям, позволивший расширить возможности автоматического синтеза программ за счёт существенного сокращения перебора.

• На основе предложенного метода разработана и реализована программная система автоматического синтеза функциональных программ.

Эксперименты с системой продемонстрировали достоинства предложенного метода и возможность синтеза за приемлемое время функциональных программ, дедуктивный синтез которых до этого удавалось реализовать только вручную.

Заключение

.