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

Факультет Вычислительной математики и кибернетики

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

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

СИСТЕМА АВТОМАТИЧЕСКОГО СИНТЕЗА

ФУНКЦИОНАЛЬНЫХ ПРОГРАММ

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

Научный руководитель:

кандидат физико-математических наук, доцент В.Н. Пильщиков Москва Оглавление Введение. Существующие подходы к синтезу программ

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

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

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

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

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

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

Заключение

Литература

Приложение 1. Описание языка спецификаций, используемого в системе АЛИСА... Приложение 2. Встроенные знания системы АЛИСА

2.1 Набор аксиом

2.2 Встроенные преобразования термов и логических выражений

2.3 Используемый алгоритм унификации

Приложение 3. Представление выражений и термов в системе АЛИСА

Приложение 4. Синтез функции mod. Удаление скулемовской функции из доказательства

Приложение 5. Синтез функций front и last

Приложение 6. Синтез функции sort

Приложение 7. Алгоритм унификации различий.

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

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

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

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

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

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

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

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

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

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

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

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

Работа человека в этом случае сводится только к корректному описанию задачи.

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

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

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

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

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

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

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

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

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

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

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

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

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

аксиом, задающих отношения вычислимости.

Стратегия поиска доказательства в случае предложений вычислимости простейшего вида u 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_tac i resolve_tac thms i Тактика резолюции. thms – это список правил, которые решают i-ю подцель. Для каждого из этих правил резолюция формирует следующее состояние, унифицируя заключение с подцелью, и подставляет конкретизированную предпосылку на место подцели. Результат применения будет ложным, если ни для одного правила не удалось создать следующее состояние.

В системе предоставлена возможность комбинирования тактик с помощью специальных операторов – тактических конструкций. Основные тактические конструкции: THEN, ORELSE, REPEAT.

применяется tac1, затем tac2. Если применение одной из тактик возвращает fail, то происходит возврат к начальному состоянию.

tac1 ORELSE tac успешно, то tac2 не применяется, иначе же применяется tac2.

REPEAT tac Тактика tac применяется до тех пор пока не вернет fail.

Для взаимодействия с пользователем в системе использован язык Standart ML [Harper, 1989]. В нем предоставлена возможность управления контекстом доказательства. Основными из возможностей являются следующие:

Начать доказательство теоремы f.

Goal f by tac; Применить тактику tac к текущему состоянию доказательства.

undo(); Откатить состояние доказательства к предыдущему.

result(); Возвращает теорему, которая уже доказана и fail, если еще есть недоказанные подцели.

qued name Обычный путь завершения доказательства. Доказанная теорема сохраняется в базе данных Isabelle.

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

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

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

Рассмотрим системы, в которых планирование применяется для сокращения перебора при построении доказательства по индукции. Это системы автоматического доказательства Oyster/Clam и CLAM.

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

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

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

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

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

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

Ключевая тактика, применяемая в системах Сlam и Clam при доказательстве теорем по индукции, – это применение волновых правил1. В соответствии с ней, при доказательстве шага индукции надо определить различия между гипотезой и заключением индукции, а затем так их преобразовывать, чтобы разница преобразования, которые уменьшают различия, таким образом отсекается часть правил, которые, скорее всего, не приведут доказательство к успешному завершению. Это делается с помощью специальных аннотаций на формулах:

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

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

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

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

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

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

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

Постановка задачи Целями диссертации являются:

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

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

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

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

Глава 3 рассказывает о разработанном в диссертации методе синтеза программ.

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

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

Название образовано от Автоматический ЛИсп Синтезатор В работах [Manna and Waldinger, 1980, 1992] предложен метод дедуктивных таблиц, предназначенный для синтеза функциональных программ по их формальным спецификациям. Основы этого метода рассмотрены в настоящей главе.

Функциональная программа строится на основе трёх структур управления:

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

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

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

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

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

В этом случае мы используем свойство удаления выходной переменной для второй строки:

Во второй строке полученной таблицы записано утверждение, о том, что a>0, оно может быть использовано как известный факт. Также в таблице указано, что если будет доказана цель z=f(a), то в качестве результата будет выдано z.

Для описания остальных дедуктивных правил нам потребуется понятие унификации. Подстановка называется унификатором предложений A и B, если A=B. Унификатор называется наиболее общим унификатором для предложений A и B тогда и только тогда, когда для любого другого унификатора существует такая подстановка µ, что =µ°, где ° – обозначение операции композиции подстановок. Операция композиции определяется следующим образом: подстановка µ° получается из µ ={x1 t1,…,xn tn} и ={y1 u1, …, yn um} как подстановка {x1 t1,…,xn tn,y1 u1,…, yn um}, в которой вычеркиваются xi ti, если xi= ti, и yi ui, если yi=xj при некотором j, 1jn.

Для унификации двух предложений A и B существует специальный алгоритм (описанный, например, в работе [Чень и Ли, 1983]), который либо находит наибольший общий унификатор данных выражений, либо выдает ответ о том, что выражения унифицировать невозможно.

Рассмотрим в качестве примера унификацию термов P(NIL) и P(x), где P – некоторый предикат, NIL – константа, х – переменная. Идея алгоритма состоит в следующем: предложения P(NIL) и P(x) просматриваются слева направо до нахождения первого несовпадающего символа. В данном случае это символы N и х. Начиная с этого символа, выписывается выражение (терм) из P(NIL), который не соответствует выражению (терму) из P(x). Эти термы (NIL и x) называются различием. Задача состоит в том, чтобы ликвидировать различия, если это возможно, выполнив некоторые подстановки. Если одно найденное различие состоит из переменной (в данном случае х) и некоторого терма (NIL), то после замены переменной на этот терм различие будет ликвидировано. Полученная подстановка {x NIL} выполняется в обоих выражениях, и поиск различий во вновь полученных выражениях начинается сначала. В рассматриваемом примере после выполнения подстановки выражения становятся одинаковыми, найден наибольший общий унификатор {x NIL}, алгоритм унификации останавливается. Если в процессе поиска нашлось различие, в которое не входит переменная, то процесс унификации тоже останавливается – унификация таких выражений невозможна.

Формальная запись алгоритма унификации приведена в приложении 2.

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

Правило резолюции для целей (GG-резолюция).В таблицу, содержащую строки G1 и G2, может быть добавлена строка G:

Здесь:

G1, G2 – выражения, не имеющие общих свободных переменных (если это не соответствующие переменные);

Р, Р’ – их подвыражения, не содержащие кванторов, такие что P и P' могут быть унифицированы некоторой подстановкой : Р=Р’.

Заменив все вхождения Р в G1 на false, получаем G1[false], а все вхождения P’ в G2 на true, получаем G2[true]. В таблицу добавляется новая цель, содержащая конъюнкцию G1[false] G2[true], с указанным условным выходом.

Используя аналогичные обозначения, запишем ещё три варианта правила резолюции, полученные из GG-резолюции с помощью свойства двойственности таблицы.

AG-резолюция:

AA-резолюция:

GA-резолюция:

Замечания о выходном терме :

1. Если s=t, то условный терм можно упростить следующим образом:

2. Если одна из строк (например, G2) не имеет выходного терма, то вместо условного выражения в качестве выхода новой строки записывается s – выходной терм второй строки G1.

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

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

3. Правило замены эквивалентных термов.

В таблицу, содержащую строки G1 и G2, может быть добавлена строка G:

Здесь:

G1, G2 – выражения, не имеющие общих свободных переменных (если это не так, можно, используя свойство дедуктивных таблиц, переименовать соответствующие переменные);

L=R – подвыражение цели G1, а L’ – терм, входящий в G2, который может быть унифицирован с термом L некоторой подстановкой : L=L'. Выражение L=R и терм L’ не содержат кванторов.

Заменив все вхождения (L=R) в G1 на false, получаем G1[false], и заменив некоторые (не обязательно все) вхождения L’ в G2 на R, получаем G2. Так как заменяются не все, а только некоторые вхождения L', мы используем при записи не квадратные скобки [], а угловые. В таблицу добавляется новая строка с указанным условным выходом, содержащая цель G1[false] G2. Относительно выходного терма верны те же замечания, что и в правиле резолюции.

Данное правило также позволяет ввести в синтезируемую программу условную конструкцию.

4. Правило замены эквивалентных выражений.

Это правило аналогично правилу замены эквивалентных термов, только в нём L, R, L' рассматриваются не как термы, а как выражения, и вместо равенства термов (=), рассматривается эквивалентность логических выражений 5. Индукционное правило.

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

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

Правила переписывания формируются из определений объектов, о которых ведется рассуждение, и из известных соотношений между этими объектами.

Например, функцию s(N), возвращающую для каждого неотрицательного целого числа N следующее за ним целое число, можно определить следующим образом:

s(0)=1, s(N)=N+1.

Из этого определения могут быть сформированы следующие правила переписывания:

s(0)==>1, s(N)==>N+1, 1==>s(0), N+1==>s(N).

Применение систем переписывания позволяет определить, является ли соотношение логическим следствием заданного набора аксиом. В качестве примера рассмотрим систему переписывания, которая позволяет получить остаток от деления на 2 суммы из 0 и 1 без применения операций деления.

Действия, которые мы можем совершать с заданным выражением, следующие:

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

Рассмотрим применение правил (2.2) – (2.5) к выражению 1+1+0+1.

Применив правило (2.3), мы преобразуем данное выражение к виду 1+1+1.

К полученному выражению можно применить только правило (2.5):

0+1.

Теперь применимо правило (2.4), которое и дает в результате 1. Больше ни одно из правил применить нельзя, результат получен.

Существуют системы, в которых переписывание можно проводить бесконечно, то есть на любом шаге существует применимое правило.

Например, при использовании системы переписывания, содержащей правила (2.6) и (2.7):

либо оба эти правила будут неприменимы, либо процесс их применения будет продолжаться бесконечно, так как к результату применения правила (2.6) применимо правило (2.7), a к его результату снова применимо (2.6):

(a+b) * c ==> a*c+b*c ==> (a+b) * c ==> … Для таких систем необходимо задать дополнительное условие окончания применения правил. Для системы, содержащей правила переписывания (2.6) и (2.7), таким условием может быть завершение работы при получении выражения, которое не содержит скобок. Это условие запрещает применение правила (2.7) к результату, полученному после применения (2.6), и зацикливания не происходит.

2.2 Формирование волновых правил 2.2.1 Основные понятия, связанные с волновыми правилами Волновые правила формируются из правил переписывания добавлением аннотаций. Некоторые (не обязательно все) одинаковые предложения левой и правой частей правила переписывания объявляются основой. Остальные фрагменты образуют волновой фронт и отмечаются для дальнейшего преобразования. Если один или несколько фрагментов, выделенных как основа, оказываются внутри волнового фронта, то они образуют волновую дыру.

Рассмотрим правило переписывания (X+Y)+Z ==> X+Y+Z Из него может быть получено, например, следующее волновое правило:

( X +Y ) +Z ==> (X+Y+Z) Здесь подчеркнутые фрагменты – это фронты волн (границы фронта волны обозначены подчеркнутыми скобками); терм Y в левой части правила переписывания и терм Y+Z в правой части находятся в волновых дырах.

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

Основа Y+Z левой части правила переписывания совпадает с основой правой части.

Другой вариант волнового правила, который может быть получен из правила переписывания (2.8):

( X + Y) +Z ==> (X+Y+Z) Основа левой и правой частей этого правила – X+Z. Заметим, что хотя все три переменные X, Y и Z входят и в левую, и в правую часть правила переписывания, они все одновременно не могут быть основой. Основа должна являться синтаксически правильным предложением, поэтому вместе с X, Y, Z в нее вошли бы и все знаки операций, содержащиеся в выражении, из-за чего волновой фронт оказался бы пустым (скобки не считаются операцией, это способ задания порядка вычислений, поэтому волновой фронт, содержащий только (), не рассматривается), то есть исходное правило переписывания осталось бы в неизмененном виде. Поэтому при формировании волновых правил из правила переписывания (2.8) необходимо, чтобы хотя бы одна переменная вошла в волновой фронт.

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

2.2.2 Алгоритм унификации различий Для расстановки в двух предложениях волновых фронтов применяется метод унификации различий (difference unification) [Basin and Walsh, 1993]. Его основная идея состоит в том, что общие части сопоставляемых предложений считаются входящими в основу, а различия записываются в волновой фронт.

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

Существуют следующие варианты удаления различий:

1. Функция может быть "спрятана" в волновой фронт (правило HIDE).

Например, если различие состоит из предложения х (но не переменной) и некоторой функции f(y), то функцию f можно записать в волновой фронт и рассматривать различие х и y. В случае если y=x, x окажется в волновой дыре, получим f(x).

2. Переменная, образующая различие, может быть удалена (правило ELIMINATE). Если различие состоит из переменной X и терма y, причем терм y не содержит X, то в рассматриваемых предложениях можно выполнить подстановку {X y} и продолжить унификацию различий дальше.

3. Переменная, образующая различие, может быть заменена на некоторую функцию (правило IMITATE). Если различие состоит из переменной X и функции f(y), то переменная X может быть заменена на ту же функцию f от некоторой новой переменной f(Xnew). В унифицируемых выражениях проводится подстановка {X f(Xnew)}, а новое различие образуют Xnew и y.

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

В качестве примера рассмотрим унификацию различий термов f(Х,a) и f(g(a),Х), где Х – переменная, а - константа. Первое различие встречается, начиная с 3-ей позиции, различающиеся термы – X и g(a). Применим к ним правило HIDE: функция g будет "спрятана" в волновой фронт. Следующее различие (между Х и а) ликвидируется применением правила ELIMINATE:

выполним подстановку {X a}. Получим термы f(a,a) и f(g(a),a).

Больше различий в основах этих термов нет, в итоге выражения аннотированы следующим образом: f(Х,a) и f(g(a),Х).

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

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

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

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

будем явно отмечать все вложенные фронты, обозначая их одним общим:

(x +f( y )) + z.

Рассмотрим представление выражения в виде дерева и припишем каждой вершине «вес» - количество волновых фронтов, в которые входит находящееся в вершине предложение. Если в вершине записан знак операции, то вес – это количество волновых фронтов, включающих в себя все выражение, заданное поддеревом с корнем в рассматриваемой вершине. Например, представление выражения (x+f( y ))+z выглядит следующим образом:

Если волновые фронты распространяются только наружу, то мерой такого выражения будем считать список из сумм весов на каждом уровне от листьев к корню дерева: [2,1,0]. Мера выражения, содержащего направленный внутрь волновой фронт, определяется аналогичным образом, только суммы весов рассматриваются в противоположном порядке (от корня к листьям дерева).

лексикографический порядок.

расстановку волновых фронтов, получим:

Единственный возможный вариант расстановки направления распространения волн в данном случае (X+Y)+Z X+(Y+Z), так как тогда мера правой части – [0, 1] – будет меньше меры левой – [1,0].

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

Общими условиями применимости волновых правил на произвольном этапе доказательства являются следующие:

1. Цель содержит фронт волны.

2. Существует волновое правило, левая часть которого может быть сопоставлена с подвыражением или внутренним термом цели, содержащим фронт волны.

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

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

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

Рассмотрим в качестве примера доказательство свойства ассоциативности операции сложения для натуральных чисел: t+(Y+Z)=(t+Y)+Z. Индукцию будем вести по переменной t. Шаг индукции этого доказательства запишем следующим образом:

t+(Y+Z)=(t+Y)+Z Здесь s(t) – функция, выдающая t+1 в качестве результата для неотрицательного целого числа t. В рассматриваемом примере волны распространяются наружу (это обозначено стрелками).

На основе свойств операции сложения s(T) +L = s(T+L), s(X)=s(Y)) (X=Y) можно сформулировать следующие волновые правила:

Используя эти волновые правила, преобразуем заключение индукции:

s(t) +(y+z)=(s(t) +y)+z ==> {используем правило 2.11} {используем правило 2.11} {используем правило 2.12} ==> t+(y+z) = (t+y)+z Получено выражение, в точности совпадающее с гипотезой индукции, доказательство успешно завершено.

На практике иногда возникают ситуации, когда ни одно из волновых правил применить нельзя и при этом пример предположения в цели не получен, но получен пример некоторой части предположения. Если предположение имеет вид H1=H2, а после проведении преобразований цель содержит предложение Н1 – пример H1, то для доказательства цели можно воспользоваться предположением как правилом переписывания Н1==>Н2. Аналогично, если цель содержит Н2, то предположением можно воспользоваться как правилом переписывания Н2==>Н1.

Вернемся к рассмотренному примеру доказательства свойства ассоциативности сложения неотрицательных целых чисел. Предположим, что правило (2.12) не известно. Тогда доказательство остановится после преобразования заключения к виду s(t+(y+z)) = s((t+y)+z) Правило (W*) неприменимо, пример гипотезы индукции t+(Y+Z)=(t+Y)+Z в заключении не получен, но получен пример ее левой части, поэтому воспользовавшись гипотезой как правилом переписывания t+(Y+Z)==>(t+Y)+Z, преобразуем заключение к виду s((t+y)+z)) = s((t+y)+z) Полученное выражение истинно, так как слева и справа от операции = стоят одинаковые термы. Истинность заключения индукции доказана, доказательство на этом успешно завершается.

2.4 Применение волновых правил с распространением фронта волны внутрь Распространение фронта волны наружу – лишь один из способов применения волновых правил. Фронт волны может распространяться и внутрь выражения, в направлении к свободной переменной. Идея таких преобразований состоит в том, что свободной переменной может быть сопоставлен произвольный терм, в том числе и содержащий волновой фронт. После такого сопоставления волновой фронт будет “поглощен” свободной переменной.

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

Рассмотрим выражение N:nat.M:nat.Q(N,M), обозначающее, что для двух натуральных чисел M и N справедливо соотношение Q(N,M). Если в качестве индукционной переменной будет выбрана N, то шаг индукции может быть записан следующим образом:

N:nat.[M:nat.Q(N,M)M :nat.Q(N+1,M)] Перед доказательством кванторы необходимо вынести из внутренних выражений:

N:nat.[(M:nat.Q(N,M))(m:nat.Q(N+1,M))] N:nat.[M:nat.¬Q(N,M)K :nat.Q(N+1,K)] N:nat.M:nat.K :nat. ¬Q(N,M) Q(N+1,K) Таким образом, первое вхождение переменной M, которая была связана квантором всеобщности и не являлась индукционной переменной, может быть заменено на некоторый терм, и, вообще говоря, оно не связано со вторым вхождением, которое остается переменной, связанной квантором всеобщности.

В рассмотренном примере это переменная K. Такая переменная называется стоком и обозначается K.

Если фронт волны целиком окажется на месте стока, он будет сопоставлен с f(N), а в полученном выражении будет пример индукционной гипотезы.

Рассмотрим в качестве примера функцию rotate(n,l), которая удаляет n элементов из начала списка и добавляет их в конец (то есть осуществляет циклический сдвиг списка на n элементов влево). Докажем её свойство l:list().k:list().rotate(length(l), lk) = kl, где length(l) – функция, возвращающая длину списка l, – операция конкатенации списков. Это свойство означает, что если взять length(l) элементов списка lk и поставить их в конец списка, то будет получен список kl. Действия функций определим с помощью следующих правил переписывания:

length(nil) 0 (nil – терм, обозначающий пустой список) length(H::T) length(T) + (H::T – операция добавления элемента H в начало списка T) rotate(N+1,nil) nil rotate(N+1,H::T) rotate(N,T(H::nil)) (H::T) L H ::(T L) Для доказательства может быть использован следующий вариант построения индукции:

базовый случай: rotate(length(nil),nilk)=knil, гипотеза индукции:

h:.l:list().rotate(length(l),lK)=Kl заключение:

rotate(length(h::l),h::lk)=kh::l Применим волновые правила rotate(s(N), (H::T)) rotate(N,(T (H::nil)) ) L(H::T) ( L(H::nil) ) T и приведенные выше правила переписывания к заключению индукции:

rotate(length(h::l),(h::l)k)=k (h::l) rotate( ( length(l)+1),(h::lk))=k(h::l) rotate(length(l),(lk(h::nil)))=k(h::l) rotate(length(l),l k(h::nil))= k(h::nil)l rotate(length(l),lk(h::nil))=k(h::nil) l После выполнения подстановки {Кk(h::nil)} заключение индукции будет сведено к гипотезе. Утверждение доказано.

2.5 Преимущества применения волновых правил. Особенности применения волновых правил для синтеза программ По сравнению с применением обычных правил переписывания, применение волновых правил дает существенные преимущества.

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

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

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

Разработанный в диссертации новый метод объединяет преимущества этих двух методов.

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

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

Отметим, что применение указанных эвристик не приводит к потере решения.

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

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

Как показывает практика, использование ограничений на применение дедуктивных правил позволяет сократить перебор в среднем в 2-6 раз, а при планировании доказательства с использованием волновых правил - на порядка. Именно это и позволило за приемлемое время автоматически синтезировать некоторые программы, дедуктивный синтез которых ранее удавалось провести лишь вручную.

3.1 Эвристики, ограничивающие число применимых правил 3.1.1 Учёт полярности логических выражений Эта эвристика была предложена в работе [Manna and Waldinger, 1992].

Полярность подвыражения, находящегося в колонке целей дедуктивной таблицы, считается положительной, если это подвыражение находится в области действия чётного числа отрицаний, и отрицательной, если число отрицаний нечётно. В отличие от определения полярности для термов (введенного в главе 1) здесь мы рассматриваем полярность логических выражений. Так, например, полярность подвыражения A в выражении A and B положительна, а в выражении not(A) and B – отрицательна. Некоторые подвыражения могут иметь и двойную полярность, как, например, D и E в выражении DE; это объясняется тем, что DE эквивалентно выражению (¬DE)(D¬E), содержащему вхождения D и E с положительной полярностью и с отрицательной.

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

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

Для пояснения этой эвристики рассмотрим в качестве примера применение правила резолюции к строкам В утверждении А выражение a=NIL имеет отрицательную полярность (обозначена символом –), в цель G входит такое же выражение, но его полярность положительна (обозначена +). Перенесем А в колонку целей:

Для строк G и AG есть несколько вариантов применения правила резолюции. В первом варианте, выражение a=NIL цели АG будет заменено на false, а соответствующее выражение в цели G – на true. Получим новую цель not(false) and true and (z=1), которая после упрощения добавляется в таблицу:

Второй вариант предполагает замену выражения a=NIL цели G на false, a соответствующего выражения в цели AG – на true. При этом получаем цель преобразуется в false. Добавлять в таблицу такую строку не имеет смысла, так как она является бесполезной для дальнейшего доказательства. Применение стратегии полярности исключает варианты применения правил, подобные второму.

3.1.2 Учёт типов термов при выводе Рассмотрим еще одну эвристику, которая состоит в том, что вместе с каждым термом, встречающимся в дедуктивной таблице, хранится его тип, и этот тип учитывается при синтезе. Это позволяет избежать появления бессмысленных конструкций. Например, предикат emptylist(х), проверяющий, является ли список х пустым, не должен иметь в качестве аргумента целое число, поэтому ветвь доказательства, содержащая конструкцию emptylist(2+3) отбрасывается.

Кроме введения типов, задается их иерархия, которая позволяет упорядочить проверку условий во вложенных условных конструкциях выходного терма и отбросить некоторые некорректные проверки. Например, при вычислении выражения (b=1/a) (a>0) необходимо, чтобы сначала было проверено условие (a>0) и лишь после него (b=1/a), поскольку конструкция if (b=1/a) then if (a>0) then Q является ошибочной при a=0.

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

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

list_(0) – произвольный список, list_(1) – список, содержащий хотя бы 1 элемент, list_(2) - список, содержащий как минимум 2 элемента, и т.д.

Для целых чисел выделена следующая иерархия типов (перечислены в порядке убывания):

int_(0) – произвольное целое число, int_(1) – целое число, не равное нулю, int_(2) – положительное целое, и т.д.

В системе АЛИСА, реализованной в диссертации типы термов определяются следующим образом.

Во-первых, в спецификацию синтезируемой функции добавлена специальная конструкция с ключевым словом for, с помощью которой задаются типы входных параметров функции. Так, например, в спецификации =0) and (j>0) then (i=y*j+z) and (z>=0) and (z0) Применив правило резолюции к строкам G2 и G1 для общего подвыражения (a>0), а затем правило резолюции к полученной строке и к G3, мы добавим в таблицу новую строку с тождественно истинной целью и условным выходом:

Формально правило резолюции применимо к таким строкам, но в результате получена строка, выходной терм которой не может быть вычислен при а=0.

Учитывая информацию о типе переменной а в строке G1, получим, что выражение (a>0), в котором a имеет тип int_(0) (целое число), не может быть заменено на true или false раньше, чем выражение ¬(b=1/a), тип переменной а в котором – это int_(1) (целое число, не равное нулю).

Поэтому правило резолюции к строкам G1 и G2 оказывается неприменимо. Но это правило применимо к строкам G1 и G3 для общего подвыражения (b=1/a), а затем к полученной строке и G2. В этом случае в таблицу будет добавлена новая строка с тождественно истинной целью и условным выходом, который может быть вычислен и при а=0:

Дадим обоснование предложенной эвристики. При применении дедуктивных правил выражение, заменяемое на true или false, в общем случае появляется в выходной колонке в качестве условия в условном терме. При появлении вложенных условных термов их условия должны проверяться в такой последовательности, чтобы сначала были проверены самые "общие" условия (содержащие элементы максимальных типов, т.е. int_(0) или list_(0)), и только потом проверялись те, которые от этих условий зависят, так как при невыполнении "общих" условий вычисление остальных может оказаться невозможным. Например, чтобы проверить какое-либо условие, касающееся "хвоста" списка (tail), надо знать, что список непустой, иначе вычисление функции tail будет возвращать ошибку. Таким образом, нужно применять дедуктивные правила так, чтобы сначала в выходной колонке появлялись выражения с аргументами минимального типа, затем бльшего и т.д.

Отметим, что не все типы упорядочены, например, сравнение типов int_(i) и list_(j) невозможно, так как они входят в разные иерархии. В таком случае при применении дедуктивного правила возможно несколько вариантов:

любое из подвыражений может рассматриваться в качестве выражения, содержащего минимальный тип (при условии, что в выражение не входит рассматриваемый терм типа int_(i1), где i1>i, и типа list_(j1), где j1>j). Тип unknown_, по определению, считается бльшим, чем любой другой тип.

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

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

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

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

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

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

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

приложение 7).

Формирование правил переписывания происходит следующим образом.

1. Аксиоме вида if A then B соответствует правило переписывания B==>A. Мы учитываем, что доказательство с помощью волновых правил ведется в "обратном" направлении: от заключения индукции к гипотезе, поэтому и правила переписывания ориентированы в противоположном направлении по отношению к операции логического следствия. В качестве соответствующего дедуктивного правила записывается правило резолюции.

Обоснование выбора правила резолюции следующее. На практике мы работаем с выражениями, которые приведены к специальному виду (к конъюнкции выражений, если это утверждение, и к дизъюнкции выражений, если это цель), а первыми применяются дедуктивные правила расщепления. После этого остальные правила применяются к целям, имеющим вид (соответственно, к утверждениям вида E1…En), полученным в результате применения правил расщепления. Таким образом, при применении правила резолюции к цели A и G для общего подвыражения B:

мы получим строку в которой B будет заменено на А, что соответствует применению правила переписывания (заметим, что в общем случае мы ищем в цели G подвыражение B1, которое можно унифицировать с B и в результирующей строке потребуется выполнение подстановки, которая является унификатором B и B1).

Для аксиомы if A then B также могут быть сформированы те же правила, что и для аксиомы B, но с добавлением условия А, проверяемого при применении правил.

2. Аксиома, содержащая операцию эквивалентности A B, рассматривается как две аксиомы: if A then B и if B then A, волновые правила для которых формируются так же, как описано в предыдущем пункте, только в качестве соответствующего дедуктивного правила записывается правило эквивалентной замены логических выражений (а не правило резолюции).

3. Аксиома, содержащая операцию равенства A=B, порождает два правила переписывания: A==>B и B==>A. Соответствующее им дедуктивное правило – правило замены эквивалентных термов.

4. Аксиома, представляющая собой конъюнкцию A1 … An, рассматривается как n аксиом A1,…,An, для каждой из которых строятся волновые правила.

5. Аксиома, содержащая дизъюнкцию целей, преобразуется в условное выражение с помощью правил ¬AB = if A then B, но с учетом информации о типах термов, входящих в A и B: если терм х входит в А и в В, то тип его вхождения в B должен быть не больше, чем тип вхождения в А.

6. Если аксиома A является отношением (предикатом от двух аргументов, записанным в префиксной или инфиксной форме, то есть A=rel(L,R) или A= L rel R), и отношение отлично от =, то формируются два правила переписывания L==>R и R==>L с пустым условием и с отрицательной и положительной (относительно rel) полярностями соответственно. В качестве соответствующего дедуктивного правила записывается правило замены аргументов в отношениях.

Пример. Согласно сказанному, для аксиомы (a+b)*c = a*c + b*c будут получены следующие волновые правила Все эти правила рассматриваются с пустым условием, они применимы для термов любой полярности, а в качестве соответствующего дедуктивного правила записано правило замены эквивалентных термов.

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

Конкретный вариант гипотезы индукции получается при выборе конкретного wf-отношения. Эти отношения заранее заданы и записаны в дедуктивной таблице в виде аксиом. Выбор подходящего отношения осуществляется с учетом типа переменной, по которой ведется индукция. Например, для