автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Система автоматического синтеза функциональных программ

Московский государственный университет имени М.В.Ломоносова

На правах рукописи

Корухова Юлия Станиславовна

СИСТЕМА АВТОМАТИЧЕСКОГО СИНТЕЗА ФУНКЦИОНАЛЬНЫХ ПРОГРАММ

Специальность 05.13.11 - математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

Автореферат

диссертации на соискание ученой степени кандидата физико-математических наук

Москва 2005

Работа выполнена на кафедре алгоритмических языков факультета вычислительной математики и кибернетики Московского государственного университета им. М.В. Ломоносова.

Научный руководитель: кандидат физико-математических наук,

доцент

Пильщиков Владимир Николаевич.

Официальные оппоненты; доктор физико-математических наук

Подловченко Римма Ивановна;

кандидат физико-математических наук Ефимкин Кирилл Николаевич.

Ведущая организация: Институт системного анализа РАН

Защита диссертации состоится " 23 " декабря 2005 г. в 11 часов на заседании диссертационного совета Д 501.001.44 в Московском государственном университете им. М.В. Ломоносова по адресу: 119992, ГСП-2, Москва, Ленинские горы, МГУ, 2-й учебный корпус, факультет ВМиК, аудитория 685.

С диссертацией можно ознакомиться в библиотеке факультета ВМиК МГУ.

Автореферат разослан "_"_2005 г.

Ученый секретарь диссертационного совета

профессор I. Н.П. Трифонов

¿№>6 А-#¿0

Общая характеристика работы

Актуальность темы

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

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

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

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

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

Цель работы

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

Научная новизна

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

' Manna, Z., Waldinger, R. Fundamentals of Deductive Program Synthesis // IEEE Transactions on Software Engineering, vol.18(8), 1992, p. 674-704

Практическая ценность

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

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

Методы исследования

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

Апробация работы и публикации

Содержание и результаты диссертационной работы отражены в пяти публикациях [1-5]. Результаты работы докладывались на международных конференциях: "Интеллектуализация обработки информации (ИОИ-2002)" (Украина, 2002 г.), "Recent Advances in Soft Computing RASC-2004" (Великобритания, 2004 г.), "ESSLLI Student Session - 2005" (Великобритания, 2005 г.), на научном семинаре Международного центра по вычислительной логике (ICCL) Дрезденского университета (Германия, 2005 г.), на

конференциях Ломоносовские чтения (2005 г.) и Тихоновские чтения (2005 г.) в МГУ, на научно-исследовательском семинаре программистских кафедр факультета ВМК МГУ, на семинаре "Теоретические проблемы программирования" (ВМК МГУ), на семинаре в ИПМ им. М.В. Келдыша РАН.

Структура и объём диссертации

Диссертация состоит из введения, четырех глав, заключения, библиографии и семи приложений. Общий объём диссертации - 124 страницы. Библиография включает 47 наименований.

Краткое содержание работы

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

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

(А! ЛА2 л... лАп) ->(С1 УС2 v ... v Ст) и имеет вид

Assertions Goals Output

А,

Ап

G, ti

Gm tn.

где Аь ..., Ап - известные аксиомы, a G1;..., Gm - доказываемые цели.

Дедуктивная таблица состоит из колонки утверждений (assertions), в которой записываются известные аксиомы, колонки целей (goals), в которой записаны цели для доказательства, и выходной колонки, в которой

б

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

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

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

эквивалентна таблице

Таблица

G

G s

GX s\

Если в подстановке X присутствует замена (1:) для переменной х, входящей в б, то в выходной колонке появится обращение к функции £. Обычно это правило используется для построения нерекурсивных ветвей функций.

Правило резолюции. В таблицу, содержащую строки 01 и 02, может быть добавлена строка в с условным выходом:

G,[P] S

G2[P') t

G]X[ false] л G2X[true] if PX then t\ else sX

G1: G2: G:

Здесь Р и Р' - подвыражения в Gi и G^, причем Pl=P' X. В строке G все вхождения РХ в выражение G:A заменены на false, а все вхождения Р'Л в

Gz\ заменены на true Данное правило вводит в синтезируемую функцию разветвление.

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

G:

А:

Здесь f - имя синтезируемой функции, <wf - wf-отношение (well-founded), то есть такое отношение, для которого в рассматриваемой теории нельзя построить бесконечно убывающую последовательность X!, х2, х3,..., такую, что X2<„fX1( x3<wfx2,... В качестве примера wf-отношения можно привести отношение < для натуральных чисел.

Метод дедуктивных таблиц дает набор правил для построения основных конструкций функциональных программ, однако порядок применения правил в методе недетерминирован. На практике даже для простых задач возникает огромный перебор вариантов (например, рассматривается около 30000 вариантов применений правил для задач, решение которых может быть получено за 20-30 шагов), синтез же более сложных программ оказывается невозможным. Для осуществления на практике автоматического синтеза требуются дополнительные эвристики. Особенно они важны при доказательстве шага индукции, на которое приходится ббльшая часть перебора.

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

JBundy, A., Stevens, A., van Harmelen, F., Ireland, A. and Smaill, A., Rippling: A Heuristic for Guiding Inductive Proofs. Artificial Intelligence, vol. 62, 1993, p. 185-253

Assertions Goals №

Q[a,z] z

if x<wfa then Q[x,f(x)]

переписывании (основу) и те, которые требуется преобразовать (волновой фронт). В аннотации также фиксируется направление преобразований.

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

Волновые правила формируются из правил переписывания добавлением аннотаций: одинаковые предложения левой и правой частей правила объявляются основой, остальные фрагменты образуют волновой фронт. Например, из правила переписывания (х+у)+г ==> х+у+г могут быть получены волновые правила

( х +у )1 +2 ==> (х+у+г)т и ( х + у) ==> 1х+у+г1т

Здесь подчеркнутые фрагменты - это фронты волн (границы фронта волны обозначены подчеркнутыми скобками); терм У в левой части первого правила переписывания и терм У+2 в его правой части находятся в волновых дырах (это части основы, окруженные волновым фронтом). Основой является предложение (логическое выражение или терм), которое образуется из всех фрагментов, не входящих в волновой фронт, в том числе в основу входят и волновые дыры. Стрелками задано направление преобразований.

Расстановка волновых фронтов в паре выражений (или термов) производится в соответствии с алгоритмом унификации различий. Согласно этому алгоритму выражения просматриваются слева направо до нахождения позиции, начиная с которой они различаются. Далее различие обрабатывается по одному из правил:

1. Функция может быть "спрятана" в волновой фронт. Пример х и f (х). 2 Переменная, образующая различие, может быть удалена. Выполняется подстановка вместо неё терма, с которым она сопоставляется. 3. Переменная, образующая различие, может быть заменена на некоторую функцию от новой переменной. Пример: вместо f(x)n Y рассматриваем f (х) и f (Yi), ищем различия х и Yx.

Если одновременно несколько правил применимы - возникает несколько вариантов аннотации. Поиск различий продолжается до тех пор, пока основы рассматриваемых предложений не станут одинаковыми.

В волновом правиле задается также направление преобразований (наружу t 1

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

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

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

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

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

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

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

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

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

5 Например, I. Kraan, D. Basin, A. Bundy Middle-Out Reasoning for Synthesis and Induction // Journal of Automated Reasoning, vol.16,1996, p.113-145

подвыражения, имеющие отрицательную полярность, а на true - только те, полярность которых положительна. Если это условие не выполняется, то в конъюнкции строки, добавляемой в дедуктивную таблицу, будет содержаться false или not (true). Такая цель является ложной, и содержащая её строка не дает ничего для доказательства.

Другая эвристика состоит в том, что вместе с каждым термом, встречающимся в дедуктивной таблице, хранится его тип, и этот тип учитывается при синтезе. В работе рассматриваются термы двух типов - списки и целые числа. Тип терма определяется по контексту и на основе ограничений, заданных в спецификации. Учёт типов позволяет избежать появления бессмысленных конструкций. Например, предикат emptylist (х), проверяющий, является ли список х пустым, не должен иметь в качестве аргумента целое число, поэтому ветвь доказательства, содержащая конструкцию emptylist (2+3) отбрасывается. Кроме этого, введена иерархия типов, позволяющая упорядочить проверку условий во вложенных условных конструкциях выходного терма и отбросить некоторые некорректные проверки. Например, при вычислении выражения (Ь=1/а) л (а>0) необходимо, чтобы сначала было проверено условие (а>0) и лишь после него (Ь=1 /а), поскольку конструкция if (b=l/a) then if (a>0) then Q является ошибочной при a=0. Таким образом, использование информации о типах аргументов и иерархии типов позволяет отсечь некоторые бесполезные для синтеза ветви доказательства и тем самым сократить перебор.

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

12

индукции, аннотирование заключения индукции. Если доказательство шага индукции с помощью волновых правил успешно завершено, то мы запоминаем его "путь" последовательность номеров аксиом и дедуктивных правил, соответствующих примененным волновым правилам Затем доказательство воспроизводится в дедуктивной таблице согласно найденному пути, чтобы одновременно с ним синтезировать в выходной колонке таблицы рекурсивную ветвь функции.

Волновые правила формируются из известных аксиом, содержащихся в дедуктивной таблице, причем формируются один раз - при записи аксиомы в таблицу. Для одной аксиомы возможно получение нескольких правил. Сначала для каждой аксиомы выписывается набор соответствующих ей правил переписывания, затем в них расставляются аннотации с помощью алгоритма унификации различий и задаются направления преобразований, чтобы происходило уменьшение меры. При формировании правила переписывания фиксируется то дедуктивное правило, которое будет использовано вместо данного волнового правила при воспроизведении доказательства. Так, например, аксиоме вида if A. then В, соответствуют правило переписывания В==>А и дедуктивное правило резолюции. В диссертации приведен полный алгоритм формирования волновых правил.

Конкретный вариант шага индукции получается при выборе одного из известных wf-отношений в дедуктивной таблице. Эти отношения описываются аксиомами, например, обычное отношение "меньше" для неотрицательных целых чисел задается аксиомой if iaO then i-l<wf i, которой соответствует известная схема индукции Пеано. В настоящей версии системы используются четыре wf-отношения, но их набор может быть легко расширен добавлением подходящих аксиом в дедуктивную таблицу.

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

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

Отметим, что применение перечисленных эвристик не приводит к потере решения: если с помощью метода дедуктивных таблиц синтез функции возможен, то она будет синтезирована и с использованием эвристик, которые, в худшем случае, окажутся просто неприменимыми. Если же применить эвристики удается, то возможно сокращение перебора вариантов при синтезе на два порядка.

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

Синтез осуществляется на основе заданной формальной спецификации программы, которая записывается на языке логики предикатов первого порядка. Например, спецификация функции сортировки заданного списка может быть записана следующим образом: ?

<sort(b)><=for list (b) find <z> such that perm(b,z) л ord(z) В ней указано, что аргумент функции sort является списком и что её результатом должен быть такой список z, который является перестановкой исходного списка и является упорядоченным. В диссертации приведено подробное описание языка спецификаций, а также языка, на котором записываются синтезированные программы - это "чистый" Лисп, сохраняющий функциональный стиль программирования.

Система АЛИСА реализована на языке Пролог. Этот язык имеет встроенные механизмы сопоставления и поиска с возвратом, которые используются при работе с дедуктивной таблицей. Структура системы представлена на рис. 1.

Волновые правила Рис. 1 Структура системы АЛИСА.

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

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

Перевод спецификаций и

выражений во внутреннее представление

системная информация

управляющий модуль

приложение для \Veb-cepBepa

интерфейс

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

Задача модуля, реализующего стратегию автоматического синтеза, состоит в проверке состояния дедуктивной таблицы: построена программа или нет, он же задает следующий этап выполнения доказательства, если программа еще не построена. Общая стратегия доказательства состоит в следующем: сначала производится попытка синтезировать нерекурсивную программу, используя несколько проходов по всем применимым правилам. Если такой синтез не был успешным, подбирается подходящее ■«^-отношение и строится доказательство шага индукции. Нерекурсивная ветвь в таком случае, как правило, формируется при доказательстве условий \у:Г-отношения. Отметим, что в диссертации не ставилась задача анализа эффективности полученной программы или поиска различных вариантов программ, соответствующих заданной спецификации. Система прекращает работу, как только ей удается построить первую программу, соответствующую заданной спецификации.

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

Далее в диссертации приведены результаты работы системы АЛИСА. Некоторые примеры синтезированных функций содержатся в таблице 1. На простых примерах видно, что использование эвристик позволяет сократить перебор при проведении доказательства на два порядка. Проведение автоматического дедуктивного синтеза более сложных программ, например, программы сортировки, за приемлемое время было невозможным без

использования эвристик.

Спецификации и синтезированные функции Количество правил 1 2 3

<div(i,j),mod(i j)x=for number© л number(j) find <y,z> such that if (i>0) л (j>0) then (i=y*j+z) л (zSiO) a (z<j) Вычисление результата деления нацело и остатка (DEFUN div(i,j) (COND ((and (NUMBERP i) (NUMBERP j)) (COND ((<= j i)(+ (div (- i j) j) 1))(T 0))))) (DEFUN mod(ij) (COND ((and (NUMBERP i)(NUMBERP j)) (COND ((<=ji) (mod (-ij)j))(Ti))))) 30300 39 20

<sqrt(b)><=for number(b) find <z> such that if b >0 then (sqr(z)<=b) and (b<sqr(z+l)) and (z >0) Целочисленный квадратный корень (DEFUN sqrt(b) (COND ((NUMBERP b) (COND ((< b 1) 0) (T (COND ((<= (sqr (+ (sqrt (+ b -1)) 1» b)(+ (sqrt (t b -1)) 1)) (T (sqrt (+ b -1))))))))) 31000 76 19

<sort(b)> <= for list(b) find <z> such that perm(b,z) and ord(z) Сортировка заданного списка (DEFUN sort(b) (COND ((LISTP b) (COND ((NULL b) b) (T (COND ((NULL (sort (CDR b))) b) (T (COND ((<= (CAR (sort (CDR b))) (CAR b)) (CONS (CAR (sort (CDR b))) (sort (CONS (CAR b) (CDR (sort (CDR b))))))) (T (COND ((NULL (CDR b)) b) (T (CONS (CAR b) (sort (CDR b)))))))))))))) > 1000000 4947 56

Таблица 1. Некоторые результаты синтеза. Указано количество применённых правил: 1 - при полном переборе, 2 - при синтезе с использованием эвристик, 3 - в кратчайшем пути.

В заключении сформулированы основные результаты диссертации.

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

17

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

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

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

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

Представленные результаты изложены в следующих работах:

1. Корухова Ю.С., Пильщиков В.Н. Система дедуктивного синтеза программ // Искусственный интеллект - Донецк, 2002, № 2, с. 451-459

2. Корухова Ю.С., Пильщиков В Н. Система дедуктивного синтеза программ // Международная научная конференция "Интеллектуализация обработки информации" (ИОИ-2002). Тезисы докладов - Симферополь, 2002, с. 124-125

3. Korukhova Y.S. Planning Proof in the Deductive Tableau Using Rippling // Proceedings of the 5th International Conference on Recent Advances in Soft Computing (RASC2004) - Nottingham Trent University, 2004, p. 384-390.

4. Korukhova Y.S. Automation of Program Synthesis from Logic-Based Specifications in the Deductive Tableau. ICCL Workshop on Logic-Based Knowledge Representation. TU Dresden, 2005

www.computational-logic.org/content/events/iccl-ss-2005/talks/YuliaKorukhova.pdf

5. Korukhova Y.S. An Approach to Automation of Program Synthesis in the Deductive Tableau // Proceedings of the 10th ESSLLI Student Session -Heriot-Watt University, Edinburgh, 2005, p. 122-133 http7/www.sissa.it/%7Egervain/ProceedingsFinalVersion.pdf

Напечатано с готового оригинал-макета

Издательство ООО "МАКС Пресс" Лицензия HflN 00510 от 01.12.99 г. Подписано к печати 16.11.2005 г. Формат 60x90 1/16. Усл.печл. 1,25. Тираж 100 экз. Заказ 782. Тел. 939-3890. Тел./факс 939-3891. 119992, ГСП-2, Москва, Ленинские горы, МГУ им. М.В. Ломоносова, 2-й учебный корпус, 627 к.

06-96 0

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

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

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

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

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

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

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

Глава 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 Результаты синтеза в системе АЛИСА.

На современном этапе развития программирования компьютеры всё больше начинают применяться не только на этапе кодирования программы, но и во время постановки задачи, для решения которой требуется написать программу. В пятидесятые годы 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 Название образовано от Автоматический ЛИсп Синтезатор

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

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

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

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

Заключение

1. Братко, 1990. Братко И. Программирование на языке Пролог для искусственного интеллекта, М.: Мир, 1990.

2. Кахро и др., 1981. Кахро М.И., Калья А.П., Тыугу Э.Х. Инструментальная система программирования ЕС ЭВМ (ПРИЗ). М.: Финансы и статистика, 1981.

3. Тыугу, 1984. Тыугу Э.Х. Концептуальное программирование. М.: Наука, 1984.

4. Хювенен и Сеппянен, 1990. Хювенен Э., Сеппянен Й. Мир Лиспа. В 2 томах. -М.: Мир, 1990-т. 1-2.

5. Чень и Ли, 1983. Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. -М.: Наука, 1983.

6. Юэ и Оппен, 1991. Юэ Ж., Оппен Д. Равенства и правила переписывания. Обзор.// В сборнике статей: «Математическая логика в программировании» перевод с англ. (ред. М.В.Захарьящев и Ю.И.Янов) М.: Мир, 1991, с. 176 — 232.

7. Armando et al., 1999. Armando, A. Smaill, A., Green, I.: Automatic Synthesis of Recursive Programs: The Proof-Planning Paradigm. // Automated Software Engineering, vol.6, 1999, p. 329-356.

8. Basin and Walsh, 1992. Basin D., Walsh T. Difference Matching. //Lecture Notes in Computer Science, vol.607, Springer, 1992, p. 295-309

9. Basin and Walsh, 1993. Basin D., Walsh T. Difference Unification // Ruzena Bajcsy (Ed.): Proceedings of the 13th International Joint Conference on Artificial Intelligence, Morgan Kaufmann, 1993, p. 116-122

10. Basin and Walsh, 1996. Basin, D., Walsh, Т.: A Calculus for and Termination of Rippling.// Journal of Automated Reasoning, vol. 16 (1996) 147-180 Boyer and Moore, 1979] Boyer R.S., Moore J.S. A Computational Logic. ~ New York: Academic Press, 1979.

11. Bundy et al., 1990. Bundy, A., van Hamerlen, F., Horn C., Smaill, A. The Oyster-Clam system. // Lecture Notes in Computer Science, vol. 449, Springer, 1990, p. 647648.

12. Bundy et al., 1993. Bundy, A., Stevens, A., van Harmelen, F., Ireland, A. and Smaill, A. Rippling: A Heuristic for Guiding Inductive Proofs.// Artificial Intelligence, vol. 62, 1993, p. 185-253.

13. Bundy, 1999. Bundy A. A Survey of Automated Deduction. // Lecture Notes in Computer Science, vol.1600, Springer, 1999, pages 153-174.

14. Dershowitz and Jouannaud, 1990. Dershowitz N., Jouannaud J.-P. Rewrite Systems. In Handbook of Theoretical Computer Science, Volume B: Formal Methods and Semantics. North-Holland Amsterdam, 1990.

15. Manna and Waldinger, 1980. Manna, Z., Waldinger R. A deductive approach to program synthesis.// ACM Transactions. Programming languages and systems 2(1), 1980, p. 91-121.

16. Manna and Waldinger, 1992. Manna, Z., Waldinger, R. Fundamentals of Deductive Program Synthesis.// IEEE Transactions on Software Engineering, vol. 18(8), 1992, p. 674-704.

17. Manna and Waldinger, 1993. Manna, Z., Waldinger, R. Deductive Foundations of Computer Programming. Addison-Wesley, 1993.

18. McCarthy, 1960. McCarthy, J. Recursive Functions of Symbolic Expressions and Their Computation by Machine.// Communications of ACM, Vol.3, N 4, 1960, p. 184-193

19. Traugott, 1989. Traugott, J.: Deductive Synthesis of Sorting Programs. // Journal of Symbolic Computation, vol.7, 1989, p. 533-572

20. Waldinger and Lee, 1969. Waldinger, R., Lee, R. PROW: A step towards automatic program writing. //1st International Joint Conference on Artificial intelligence, Morgan Kaufman, 1969, p.241-252.

21. Корухова и Пильщиков, 2002. Корухова Ю.С., Пильщиков В.Н. Система дедуктивного синтеза программ. // Научно-теоретический журнал искусственный интеллект, № 2 (ISSN 1561-5359), Донецк, Наука i освгга, 2002, с. 451-459.

22. Корухова и Пильщиков, 2002а. Корухова Ю.С., Пильщиков В.Н. Система дедуктивного синтеза программ. // Международная научная конференция "Интеллектуализация обработки информации" ИОИ-2002, тезисы докладов, Симферополь, 2002, с. 124-125.