и {{пх2)-\-!2\!2Слияние1{{п1х1)-\-!1, f2, М)}) Развертывая с использованием 5.3.1(11) -i=ynopHd{{{nxl)-]-fl\fГ Слияние!if 1,

{n2x2) + f2, М)}) и Упоряд {{{пх2) + f2 I f2 е Слияние! {{п!х1)

+ fl, f2, N)}) Внося Упоряд внутрь объединения {{пх!) + fl\flСлияние!(f!, {n2x2)+f2, N)

и ynop{{nx!) + f!)} и {{пх2) + f2\f2 е Слияние! {(nlx!)+fl, f2, N) и ynop{{nx2) + f2)} Развертка с использованием 5.2.2(2).

Предположим, теперь, что х1 < х2. Посмотрев на вторую компоненту объединения и вспомнив, что Vn N-n < п, легко показать, что

Yf2е Слияние!{{п!х1) + , f2, N), П{пх1) f2 -пКп т. е.

не Упор{{пх2) + 12) для любой f2Слияние!{{nlxl) + fl, f2, N).

Таким образом, в этом случае вторая компонента есть Ф. Аналогично первая компонента есть Ф, если х2 < х1. К тому же

Упор {{пх!) + fl)ynop {fl) (если xl < х2)

Упор {{пх2) + f2) Упор {f2) (если х2<х1) и предыдущее можно переписать

СлияниеС {{nlxl) + fl, {п2х2) + f2, n+N)

{{nxl) + fl I e Слияние! {fl, {п2х2) + f2, N) и ynop{fl} если xl <x2 {{nx2) + f2 I f2 e Слияние! {{nlxl) + fl, f2, N) и У nop {f 2))

иначе.

6.7. Мы имеем

СлияниеС {{{Ix)}, {п2х2) + f2,n+ N)

{{nxl) + f 1\f! Слияние!{Ф, {n2x2) + f2, N) и ynop{{nx) + fl)} и {{nx2) + f2 I f2 e Слияние! {{{Ix)} + f2, N) и Упор {{nx2) + f2)} Развертка 5.3.3(8) с использованием 5.2.2(2).

Если для всех f2 Слияние!{{{Ix}}, f2N)x<x2, то найдется <пх>е f2, такая, что п<.п и х <. х2, т. е. не Упор{{пх2}+f2), и нижняя компонента объединения есть Ф. Аналогично, если х2 <: х, мы имеем не Упор{{пх}+ fl) для

всех fl Слияние! {Ф, {п2х2У-\- f2, М), и поэтому верхняя компонента есть Ф. К тому же в случае х <: х2 мы имеем

УпорЦпх) + f!)<=>ynop{f!), а в случае х2<х ynop{{nx2)-\-f2)ynop{f2). Таким образом, СлияниеС{{{\х)}, {п2х2) + f2, п+ N)

<= {{пх) -f Iе Слияние! (Ф, {п2х2) + f2, N) и Упор if!)} если X <х2 {{пх2) + f2 I f2 е Слияние! {{{!х)}, f2, М) и Упор if2)} иначе.

6.8. Мы имеем

Перест! (nlxl) + {п2х2) + f)

ч= {/, I / , S Область {{nlxl) + {п2х2) + f )Х

X06pa3{{n!x!) + {n2x2) + f) и BucKTifi, Область({п!х!) + {п2х2) + /), Образ ({nlxl) + <n2x2) + /)) и Рядом if и {nlxl) + {п2х2) -f f)}

Пусть Область if) = N, n2 + N = N, а Образ {f) = X. Тогда Область {{nlxl) + {п2х2) + f)X Образ {{nlxl) + <n2x2) + f) есть {nl + N)X{xl + x2 + X).

Раскрывая это, мы получаем

{nlxl) + {п2х2) и {п1} X X и NX {xl} {]NX {х2} UN XX, ЧТО перепишем как

{п1х1)-]-{п2х2)и{п1}ХХ [}NXixl + X)[]NX{x2 + X).

Определение Перест!, данное в 5.4.1(4) и 5.4.1(5), получается из этого выражения исключением из него {п!}ХХ, что означает, ЧТО п! может отображаться только на х! или х2- Поэтому, как и с Регуляр из предыдущего раздела, нам нет необходимости интерпретировать Рядом, вводя 5.4.1(5). Переписав 5.4.1(8) с этим сокращенным выражением, мы получим

Перест! {{nlxl) + {п2х2) + f)

<= {/,1/, S {nlxl) + п2х2) -]-NXix! + X)UNX{x2 + X) и Биект {f и nl + N, х! + х2 + Х) и Pядoм{f, {n!x!) + {n2x2) + f)}.

Мы вновь пришли к знакомой задаче произвести свертку с 5.4.1(5). Читатель уже усвоил эту технику, и потому мы будем кратки. Оба фильтра, и Биект и Рядом (с исключенным {п!}Х XX), прекрасно разлагаются, а разнообразные комбинации подмножеств (используется правило RS3) означают, что п! переходит либо в xl, либо в х2, которые объединяются с подмножествами из NXx2-\-X и NXxl + X соответственно. Таким

образом, мы имеем

Перест! {{п!х!) + {п2х2) + /)

<={{nlxl)+f,\f,NXx2 + X)

и Биект if и М, х2 + X) и Рядом if и {ti2x2)+f)} {j{{nlx2) + f2\f2SNXx! + X

и Биект (/2, N, х! + X) и Рядом if2, {п2х!) + /)}.

7. ЗАКЛЮЧЕНИЕ

Мы надеемся, что продемонстрировали практичность и полезность подхода, связанного с синтезом, и углубили понимание структуры алгоритмов сортировки. Однако мы рассматриваем это лишь как предварительную попытку к очень большой задаче, и чувствуем, что дальнейшие попытки к регуляризации или даже частичной механизации синтеза окажутся полезными. Мы не утверждаем также, что мы продемонстрировали «.ту самую» структуру этих алгоритмов сортировки. Работа, о которой сообщено у Грина и др. [5], обнаруживает интересные сходства и различия. Во многих отношениях мы усложнили себе жизнь попыткой синтезировать по пути алгоритмы перестановок. Выполненное позднее небольшое исследование, претендовавшее на синтез только из алгоритмов сортировки и использующее ненамного более богатый синтаксис, оказалось гораздо проще (Кларк и Дарлингтон [2]).

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

ЛИТЕРАТУРА

1. Burstal R. М., Darlington J. Atransformation system for developing recursive programs.- J. Assoc. Comput. Mach. 24 (1977), 44-67.

2. Clark K., Darlington J. Algorithm classification through synthesis.-• Internal Report Department of Computing and Control, Imperial College, London, 1978.

3. Darlington J, Application of program transformation to program synthesis. - Proceedings of Symposium on Proving and Improving Programs, Arc-et-Senans, France, 1975, pp. 133-144.

4. Dijkstra E. W. A discipline of programming. - Englewood Cliffs, N. j.: Prentice-Hall, 1976. [Имеется перевод: Дейкстра Э. Дисциплина программирования. - М.: Мир, 1978.]

5. Green С. С. et al. Progress report on program-understanding systems.- Stanford Memo А1Л4 240, Stanford University, Computer Science Dept., 1974.

6. Manna Z., Waldinger R, Knowledge and reasoning in program synthesis. - Artificial Intelligence, 6, No. 2, 1975.