7.5. ПРИМЕР АВТОМАТИЧЕСКОГО НАПИСАНИЯ ПРОГРАММЫ

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

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

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

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

имеет в качестве своего значения первый элемент списка х;

имеет в качестве своего значения ту часть списка, которая остается после удаления из него первого элемента;

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

Как следствие этих определений мы получаем, что

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

Теперь сформулируем «аксиомы», формализующие наши определения и нужное нам отношение вход — выход

Прежде всего мы определим отношение сортировки в терминах двух других отношений:

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

На самом деле определения 2—5 несколько слабее того интуитивного определения, которое мы дали выше, но они достаточны для построения доказательства

Множество предложений, соответствующих приведенным выше правильно построенным формулам 1—5, таково:

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

Рис. 7.10. Дерево опровержения для

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

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

Таким образом, здесь мы имеем до некоторой степени тривиальный результат: «Если длина списка х равна 0, то

Рис. 7.11. (см. скан) Дерево опровержения для

Сформулируем теперь предположение индукции: «Для каждого непустого списка х значение можно отсортировать». Представим себе, что у нас есть функция которая может произвести сортировку списка меньшего размера. Предположение индукции в форме предложения имеет вид

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

Для доказательства нам шонадобится следующее соотношение между

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

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

Отрицанием предположения служит

Здесь а — сколемова функция, появляющаяся, когда в предположении содержатся переменные, относящиеся к квантору всеобщности. Граф опровержения изображен на рис. 7.11. Исключая функцию а и преобразуя граф опровержения обычным способом, получаем ответное утверждение

Объединяя условное ветвление, которое мы заранее обеспечили, и элементы, созданные доказателем теорем, имеем в итоге рекурсивную программу