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

(I) Принадлежность

RM1 {1{х)\хФ и Р{х)}

RM2 {/ (х) х е S + 5 и Р{х)) {f (s)} U {/ W х е S и Р (х)}

если P{s)

{f{x)\xS и Р{х)} иначе (s + S-это {s}\JS) RM3 {fix)\xSl{jS2 и Р{х)} {f{x)\xSl и Р(х)}

[j{f{x)\xS2 а Р{х)}.

(И) Подмножество

RS1 {!{Х)\ХФ и Р{Х)} -!={Ф} если Р(Ф)

Ф иначе

RS2 {f(Z);Ss + S и Р{Х)} {f{X)\XS и Р{Х)}

{j{f{s + X)\XS и P{s + X)} RS3 {f (I-)XsS/U52 и P{Z)}-!={f{X/UX2)Z/sS/Z2sS2H

р {XI и Аг)}.

(HI) Декартово произведение

RC1 ФХТ <=Ф

RC2 {Sl{jS2)XTSlXT{jS2XT.

Здесь Ф означает пустое множество, а Р(х)-произвольный предикат.

2.3. Синтез

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

1. Функ{8, T)<{f\fSXT и ЭтофункЦ)}

2. Этофунк(1){х1у1}1 ix2y2}f.xl = х2=у1 = у2.

Обратим внимание на стиль определения. Оно имеет вид «породить и проверить». Даже если бы это определение и можно было проинтерпретировать или запрограммировать буК вально, это привело бы к очень неэффективному вычислению, так как вначале порождается большое множество 2, а затем большинство его элементов отфильтровывается проверкой Этофунк. Наш синтез будет использовать свертку для введения этой проверки в процесс порождения, в результате чего полу-

A есл

перев.

) Нотация условных выражений у автора отличается от общепринятой: :ли Р иначе В - у автора и если Р то Л иначе В - в Алголе. - Прим.

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

3. Функ{Ф, T)<={f\f ФХТ и Этофунк(/)}

<=(!\!Ф.Этофунк{!)} Правило RC1

{Ф} если Этофунк {Ф)

Ф иначе) Правило RS1

-*={Ф} Развертка с использованием определения Этофунк.

Теперь надо рассмотреть другой основной случай, а именно Функ{{з}, Т). Достаточно очевидно, что это есть {{<sO} Т}[}{Ф}, однако мы проведем синтез рекурсии, так как это иллюстрирует технику, которой мы будем часто пользоваться в дальнейшем.

Вначале мы имеем

4. ФункЦз}, Ф) {Ф} как прежде

5. Фyнк{{s},t + T){f\f{s}Xi + T и Этофунк(!)}

{/ I / S {s} X {О U{s}XT я Этофунк (/)}

Правило RC2 <={fl{jf2\fls{s}X{t}f2{s}XT

и Этофунк ifl и f2)} Правило RS3.

Теперь исследуем, какие значения могут принимать fl и f2. fl есть или Ф, или {<sO}. Во втором случае, если только f2 не пусто, оно отображает s в некоторый элемент f е Т, такой, что t¥=t, и мы получим 1 Этофунк {fl и f2). Таким образом, мы можем переписать правую часть как

и {/2 \f2s{s}XT и Этофунк if 2)} <={{<5иФг/«к({«}, Т) Свертка с 1.

Наконец, синтезируем основную рекурсию, которую получим, представляя 5 как S1\JS2, где 5/ и 52 не пересекаются.

6. Фуик {S1 {jS2, T)<={f\f (SI \jS2)XT и Этофунк(f)}

Конкретизация (1) <={f\fSlXT[jS2XT и Этoфyнк{f)}

Правило RC2 {fl\}f2\fl SIXT f2sS2XT

и Этофунк if l\jf2)} Правило RS3.

Наша цель - получить свертку, позволяющую ввести рекурсию. Мы видим, что вид уравнения (6) почти позволяет свернуть его дважды с 1. Чтобы достигнуть этого, необходимо представить условие Этофунк{11\](2) в виде, содержащем 57-о0г/нл;( ) и Этофунк{12). В данном случае это просто, так как можно видеть, что при условии, что и /2 имеют непересекающиеся области определения, множество fl\jf2 будет функцией тогда и только тогда, когда являются функциями и f2, т.е. Этофунк{1}\]12)<Ф ЭтофункЦ}) и Этофунк{12). Таким образом, предыдущее может быть переписано как

{f/ и /21 /; = S; X Г и Этофунк {fl)

f2S2XT и Этофунк {f2)} {fl Uf2\fl{f3\f3SlXT я Этофунк (fl)}

f2{f4\f4S2XT и Этофунк{f2)} <={fl\jf2\fl0yHK{Sl,T)f20yHK{S2,T)} Свертка с(1).

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

Данный процесс (использование правил редукции для множеств, проверка, как свойства конструируемого объекта зависят от свойств каждой из его компонент, и последующая свертка) будет применяться при синтезе повсеместно под названием «продвижение фильтра».

3. ОБОЗНАЧЕНИЯ И ПРЕДСТАВЛЕНИЯ

Основные обозначения мы заимствуем из неформальной теории множеств; большинство из этих символов уже было использовано в предыдущем разделе. Дополнительно мы будем использовать и для объединения семейства множеств и - для операции вычитания множеств, т. е. X-Y - {z\z X и гфУ}. Другими употребляемыми типами данных будут последовательности и функции. Часто мы будем употреблять множества и последовательности взаимозаменяемым образом, когда контекст позволяет понять, что имеется в виду. В частности, множества, которые в нашем случае состоят из неотрицательных целых чисел с естественным порядком на них, часто будут рассматриваться как последовательности. Обратно, некоторые символы операций над множествами (е, +, Ф и т. д.) будут использоваться для обозначения эквивалентных операций над последовательностями. Имеются дополнительные операции, определенные только над последовательностями.