Теоретическое программирование

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

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

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

) John Darlington. Acta Informatica 11 (1978), 1-30.

© by Springer-Verlag 1978

© Перевод на русский язык, «Мир», 1981

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

Этот конструктивный подход к анализу и построению алгоритмов поддерживался Дейкстрой [4] и другими. Отличие нашей работы состоит в основном в выборе более математического подхода, особенно в части математизации языка программирования, а также в попытке охватить целый класс алгоритмов. Правила, сходные с нашими правилами программных преобразований, были независимо разработаны Манной и Вал-дингером в их работе по автоматическому программированию [6], и нам принесли большую пользу контакты с ними, а также с членами группы Корделла Грина по автоматическому программированию, разработавшими систему, способную автоматически порождать некоторые алгоритмы сортировки и полностью ориентированную на управление правилами преобразований [5].

В разд. 2 на небольшом примере мы иллюстрируем нашу форму определений высокого уровня, объектный язык программирования, а также правила программных преобразований и редукции множеств. В разд. 3 мы описываем понятия, необходимые для синтеза алгоритмов сортировки. В разд. 4 кратко описывается структура процессов синтеза, а разд. 5 и 6 содержат их детальное описание.

Полное описание стиля используемого нами языка и правил программных преобразований содержится у Берстелла и Дарлингтона [1], а их приложение к синтезу программ вкратце изложено у Дарлингтона [4].

2. ОСНОВНЫЕ ПРАВИЛА И ПРИМЕР СИНТЕЗА

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

2.1. Правила программных преобразований

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

(I) Задание. Ввести новое рекурсивное уравнение, у которого левая часть не является конкретизацией какого бы то ни было предыдущего уравнения.

(II) Конкретизация. Добавить экземпляр существующего уравнения, в котором переменная заменена на некоторый терм.

(III) Развертка. Если ЕЕ и F<F суть уравнения и имеется вхождение в F некоторой конкретизации Е, то заменить его соответствующей конкретизацией Е, получив F", и добавить уравнение F F".

(IV) Свертка. Если Е Е и FF суть уравнения и имеется вхождение в F некоторой конкретизации Е, то заменить его соответствующей конкретизацией Е, получив F", и добавить уравнение F ф F".

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

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

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

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

2.2. Основные правила редукции для ТМ-выражений

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