Теперь, так как хХ, YczX и из \fysY-y<,x следует F< < X - У, то правую часть можно переписать как

<J= Y такое что Y cz X и Yy у <х <J= Фильтр] {х, X) Свертка с (11).

Другие нужные нам случаи

13. Фильтр (Ф)-?=Ф Конкретизация (10) и правило RSI

14. Фильтр! {х, Ф)-Ф Конкретизация (И) и правило RS1

15. Фильтр! (х, х! -\- Х)<=х1 -Фильтр! {х, X) если х1 <х

Фильтр! {х, X) иначе Правило RS2 и свертка с (И).

Таким образом, мы получаем алгоритм S! {Быстрая Сортировка)

S1 Сорт{Х)Сорт1 ([X], X) СортЦФ, Ф)-{Ф} СортЩп}, {п})<={{{пх)]] Сорт! (N, X)<={f! \]f2\fl Сорт! {N\ Y)

f2 e Сорт! (Nk, X - Y)) где k = Card(Y)

где Y = Фильтр {X)

Фильтр (Ф) Ф

Фильтр (x-jr Х)<= Фильтр! (х, X) Фильтр! {х, Ф)Ф

Фильтр! {х, х! + X)-jc/ + Фильтр! (х, X) если х1 <х

Фильтр! (х, X) иначе

Конечно, этот алгоритм можно улучшить многими способами; например, вычисление X-F можно произвести совместно с вычислением Y= Фильтр (Х), однако мы надеемся, что по крайней мере выявили суть алгоритма.

5.2.3. Сортировка Выбором из Р1. Сортировка Выбором выводится непосредственно. Ее можно получить «горизонтально» из 5/, всегда выбирая в качестве Y одноэлементное множество. Мы решили выводить ее из Р1 таким образом, чтобы вынести моменты принятия решений при синтезе на как можно более высокий уровень. Итак, мы имеем

1. Перест! {N, Х) [] {f! [jf2\fle Перест! (N\ Y)

f2 Перест! (Nu X-Y)} <= U{fWf2 \fl e Перест! {{nepe{N)], {y})

f2 Перест! (ост(N), х- {у})} и {{пере (N), у) -(- / I / е Перест! (ост (N),

Х-{у})}.

Таким образом, мы получаем алгоритм перестановок Р1

Р1 Перест{Х)Перест!{[Х], X) Перест! (Ф, Ф) {Ф} Перест! т, {х}) {{{пх)}}

Перест! {N, Х) \] {{пере{Щ, y).f\f Перест! {ост (N),

V - {у})}

Снова определим

2. Сорт{Х)Упоряд{Перест{Х))

Упоряд {Перест! {\Х], X))

и пусть

3. Сорт!{Ы, Х)-=Упоряд{Перест! {N, X))

4. Сорт! (Ф, Ф)(Ф) Развертка с использованием Р1 и 5.2.2(2).

5. Сорт!{М, X) Упоряд{Перест! {N, X)).

Поместив фильтр У«оря(5 внутрь (6.3), мы получаем

6. Сорт!{М, X)<={{nepe{N), у) + f \f Перест!{ост{N), Х-{у})

и ynop{f)} для некоторого у такого что у X и \/хХ-{у}-у<х {{пере {N), y) + f\f Сорт! {ост {N), {X - {у})} для некоторого у такого что г/ е X и У/хХ-{у}-у<х

Свертка с 5.2.2(2) и (3).

Определим

7. Младший {Х)<=у такой что уХ и Yxe X - {у} • у < х. Тогда

8. Сорт1{Ы, X){{nepe{N), у) + f\ f Сорт! {ост{N), X - {у})}

где у = Младший{Х) Свертка (6) с (7).

9. Младший{{х})<=х Конкретизация (7) и редукция.

10. Младший{х! + X)

<-х1 если Мх X • х1 < X

у такой что уХ и хХ - {у}- у <х иначе

Конкретизация (7) и правило RM!,

Но так как из условия х1 < у!, где г/i е X и У/хе X - {у!} • у < < X, следует УхХх!<х, то правую часть можно

переписать как

х1 если х1 < у где уХ и х X - {у} • у < х у такое что уХ и У/х X - {у} • у <х иначе

х/ если х1 < Младший (X) Младший{Х) иначе Свертка с (7).

Так мы получаем алгоритм S2 (Сортировка Выбором)

S2 Сорт (Х) <= Сорт! ([X], X) Сорт!{Ф, Ф){Ф}

Сорт! {N, X) {{пере {N), г/> + / / е Сорт! (ост (N), X - {у})}

где у = Младший{Х)

Младший {{х}) <= X

Младший (х! -\- Х)х! если х! < Младший (Х) Младший{Х) иначе

5.3. Сортировка Слиянием и Сортировка Вставками из Р 5.3.1.Р2 из Р. Повторяя определение из Р, имеем

1. nepecT{X){f\fs[X]XX и Биект(f, [X], X), откуда немедленно можем вывести

2. Перест {Ф)={Ф} Конкретизация (1), правила RC1, RS1 и

3. Перест {{x})i={{{!x)}} Развертка.

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

4. Перест (Х! []X2)<={f\f [X! U Х2] X {X! U Х2)

и Биект if, [X! U Х2],

X! и Х2)}.

Догадка, без которой мы не обойдемся, состоит в том, что из определения Перест и Биект мы знаем, что для всяких е Перест{Х!) и f2 Перест{Х2) ОбразЦ!) = X!, а Образ (f 2)= Х2, откуда имеем, что Перест {XI \j Х2) = Перест {06-pa3{f!)\j06pa3{f2)). Поэтому предыдущее можно перефразировать и получить алгоритм вида Перест{Х!, Х2) = f {f!, f2) для всех f! Перест{X!), f2 е Перест{Х2), где / забывает структуру f! я f2 и вычисляет Перест снова через Образ{f!) и 06pa3{f2). Чтобы привести алгоритм к более привычному виду, определим /, вычисляющую некоторое подмножество Перест, а именно перестановки, достижимые из f! и f2 без использования внутреннего порядка и f2. Эту / назовем Слияние!-