Прогонка для функций высших порядков

В заметках

• Что такое суперкомпиляция?

• Какой язык лучше суперкомпилировать: "строгий" или "ленивый"?

• Суперкомпиляция функций высших порядков

речь шла о том, что метавычисления являются "пародией" на обычные вычисления. А "прогонка" - простейший вариант метавычислений (без обобщений и зацикливаний). В общем случае прогонка порождает бесконечное дерево, которое можно сделать конечным, применяя "обобщение" конфигураций и "зацикливание".

Сейчас мы постараемся подробнее разобраться, как выглядит прогонка в случае "ленивого" языка с функциями высших порядков. Суперкомпилятор HOSC обрабатывает программы именно на языке такого рода: Higher Order Lazy Language (HLL).

В случае языка HLL, программа имеет следующий вид:

d₁ ... d_N e₀ where f₁ = e₁; ... f_N = e_N;

и содержит следующие части:

• d₁ ... d_N - объявления типов для данных, обрабатываемых программой. (Сейчас эта часть программы нас не очень интересует.)

• e₀ - "целевое" выражение. Считается, что исполнение программы сводится к вычислению e₀. Если e₀ содержит свободные переменные, то через них в программу передаются исходные данные.

• f₁ = e₁; ... f_N = e_N; - определения глобальных функций. Эти функции могут использоваться внутри целевого выражения e₀ .

Вот пример программы:

data Nat = Z | S Nat;

add a b

where

add = \x y -> case x of { Z -> y; S x1 -> S (add x1 y); };

Целевое выражение содержит три свободные переменные a и b, через которые в программу и передаются исходные данные, а исполнение программы сводится к тому, что в целевое выражение add a b подставляются значения переменных a и b, после чего получившееся выражение и вычисляется.

Вот в этом и состоит различие между "обычным" вычислением выражения и "прогонкой". При обычном вычислении обрабатываемое выражение не может содержать свободные переменные, а при прогонке - может.

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

Как выполняется такого рода программа, сначала рассмотрим на примере. (И, с точки зрения людей, пишущих на Фортране, такой способ исполнения программы выглядит как чистое извращение. :-) )

Допустим, на вход поступили такие данные:

a = S Z;

b = Z;

Подставляем значения a и b в add a b. Получается

add (S Z) Z

И вот тут-то и начинается самое страшное. В случае языка первого порядка (как в SPSC) мы сразу же, за один шаг, преобразовали бы это выражение в выражение

S (add Z Z)

сделав много разных дел:

1. Нашли бы определение функции add.
2. Распознали бы, какое правило из определения add применить. А для этого нужно было бы выполнить сопоставление в образцом.
3. Применили бы правило.

Но то, что было в случае "первого порядка" одним большим действием, в случае HLL разбивается на несколько более элементарных действий. Разбиение на мелкие действия хорошо с точки зрения компьютера, с точки зрения тех, кто пишет статьи о суперкомпиляторе, и даёт некоторые дополнительные возможности в процессе преобразований. Но есть и "оборотная сторона медали"! При попытке "прокрутить" какие-то примеры вручную, на бумаге, сразу же оказывается, что граф конфигураций жутко раздувается. Точнее, раздувается не сам граф, как таковой, а конфигурации, находящиеся внутри узлов графа. Что мы сейчас и увидим.

Итак, смотрим на выражение

(add (S Z) Z)

На верхнем уровне - вызов функции add. Хорошо бы его применить к аргументам. Чтобы сделать это, ищем определение функции add, и подставляем его вместо имени функции! Таков уж язык высшего порядка. В случае первого порядка, программа и данные строго разделены, но если мы объявили, что функции являются "равноправными значениями" (first-class values), различие между "программой" и "данными" рассеивается как утренний туман (или, говоря ещё более поэтично, как нежные лепестки цветка сакуры под весенним ветром). Если число можно подставить, можно и функцию подставить. Что и делаем. Получается вот такая гадость:

(\x -> (\y -> case x of { Z -> y; S x1 -> S (add x1 y); })) (S Z) Z

Концептуально - ясно и понятно. Но выписывать руками - сущее мучение.

Теперь выражение имеет вид (\v -> e₀) e₁, и понятно, что нужно сделать дальше: применить функцию к аргументу. Т.е. в e₀ заменить все вхождения v на e₁. Конкретно, (\x -> ...) применяем к S Z и получаем

(\y -> case S Z of { Z -> y; S x1 -> S (add x1 y); }) Z

Теперь (\y -> ...) применяем к Z. Получается

case S Z of { Z -> Z; S x1 -> S (add x1 Z); }

И вот теперь наступает момент, когда нужно выполнить "сопоставление с образцом". Аргумент case-выражения содержит конструктор S на верхнем уровне. Поэтому, S Z сопоставляется с образцом S x1. При этом, переменная x1 принимает значение Z. После чего, мы извлекаем из case-выражения ветвь

S x1 -> S (add x1 Z);

и подставляем в S (add x1 Z) значение переменной x1, т.е. Z. После чего обрабатываемое выражение принимает вид:

S (add Z Z)

На верхний уровень выражения (из его глубин) выполз конструктор S. Что делать дальше? В случае "строгого" языка нужно было бы продолжать вычисления, поскольку в аргументе конструктора остался вызов функции add. Нужно его вычислять, даже если результат этого вычисления не будет использован.

Но в случае "ленивого" языка, результат вычисления может выдаваться потребителю не весь сразу - а частями. В данном случае, "частичный результат" (в виде конструктора S на верхнем уровне) - налицо. Поэтому, можно считать, что вычисление "частично закончено". Но, предположим, что некий потребитель "съел" верхний конструктор, и захотел использовать значение его аргумента add Z Z. Ну что же, тогда вычисление возобновляется, и получается такая последовательность преобразований:

add Z Z

(\x -> (\y -> case x of { Z -> y; S x1 -> S (add x1 y); })) Z Z

(\y -> case Z of { Z -> y; S x1 -> S (add x1 y); }) Z

case Z of { Z -> Z; S x1 -> S (add x1 Z); }

Z

Т.е., "совсем" окончательный результат - S Z.

А теперь наступил момент, когда нужно перейти от "обычных" вычислений к "метавычислениям". Что будет, если не подавать в программу исходные данные, а оставить в целевом выражении переменные, и попытаться вычислять "прямо так"? Оказывается, что это - не так уж трудно. Начинаем с выражения add a b. И видим, что несколько первых шагов делаются точно так же, как и в случае известных исходных данных:

add a b

(\x -> (\y -> case x of { Z -> y; S x1 -> S (add x1 y); })) a b

(\y -> case a of { Z -> y; S x1 -> S (add x1 y); }) b

case a of { Z -> b; S x1 -> S (add x1 b); }

А вот теперь появляется интересная ситуация: в аргументе case-выражения - переменная a, значение которой неизвестно. Как выбрать нужную ветвь в case-выражении?

Единственный выход - действовать "разбором случаев": рассмотреть отдельно два случая: a = Z и a = S a1, где a1 - новая переменная, которая не встречалась в программе. В этот момент линейная последовательность вычислений превращается в дерево!

Итак, для случая a = Z получается

case Z of { Z -> b; S x1 -> S (add x1 b); }

b

А для случая a = S a1 получается

case S a1 of { Z -> b; S x1 -> S (add x1 b); }

S (add a1 b)

Дальше мы извлекаем из конструктора его аргумент, и начинаем изучать процесс его вычисления отдельно (как и в случае языка первого порядка). И видим, что нам повезло: изучать-то нечего, поскольку add a1 b совпадает (с точностью до имён переменных) с начальной конфигурацией add a b. Значит, можно сделать зацикливание и получить конечный граф конфигураций:

.

Суперкомплятор HOSC именно такой граф и делает: add a b.

Впрочем, этот граф виден, если рассматривать пример через FireFox, ибо для рисования графа используется svg-графика. FireFox рисует эти графы хорошо, а видно ли в других браузерах - не уверен. Кажется, нужно какие-то плагины устанавливать для отрисовки svg-графики...

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

(Но тех, кому интересно, могу порадовать тем, что в работе сейчас находится документ, в котором будут подробно описаны внутренности суперкомпилятора HOSC, в виде формул и всего прочего, что должно быть в "научных" сочинениях.)

Более интересен другой вопрос! Ну хорошо, с прогонкой "высшего порядка" всё, вроде, получается. Но ведь в суперкомпиляторе, кроме прогонки, нужно делать и кое-что ещё: сравнивать конфигурации, строить обобщения конфигураций, проверять, вкладывается ли одна конфигурация в другую или нет?

И здесь возникают кое-какие тонкости, связанные с тем, что в случае "высшего порядка", переменные в конфигурациях могут быть как свободными, так и связанными (в то время, как в случае "первого порядка", связанные переменные в конфигурациях не появлялись).

Но это - тема для отдельного разговора...

Читать дальше...

Суперкомпиляция функций высших порядков

В послании Что такое суперкомпиляция? было описано, как выглядит суперкомпиляция для случая простого функционального языка "первого порядка".

Теперь пришло время поговорить о суперкомпиляции функций "высших порядков". Что такое "высший порядок", хорошо знает любой поклонник функционального программирования (если, конечно, под "функциональными языками" подразумевать языки вроде Standard ML и Haskell). Однако, как я подозреваю, среди программистов всё ещё встречаются отсталые элементы, ещё не проникшиеся возвышенными принципами "высшей функциональности". :-)

Поэтому, во избежание всякого рода недоразумений, начну рассказ с рассмотрения вопроса, чем, собственно говоря, "высший" порядок отличается от "первого"?

Что такое "язык первого порядка"? Обычно имеют в виду, что имеется некое разделение/сегрегация/дискриминация обрабатываемых данных на данные "первого порядка" (first-order) и "высших порядков" (higher-order). Применительно к функциональным языкам это (как правило) сводится к тому, что проводится различие между "функциями" и "нефункциями". "Нефункции" - это "обычные" данные, вроде чисел, строк, деревьев, а "функции" - ну, это "функции", которые можно применять к данным "первого порядка"...

Как известно, в мире людей всякая дискриминация и сегрегация считается чем-то подозрительным и нехорошим (а на ЮАР за это даже санкции накладывали). Поэтому, и в случае программирования, язык, в котором цветёт пышным цветом дискриминация и сегрегация, выглядит как-то нехорошо. Дело усугубляется ещё и следующей патологией. Поскольку функции являются сущностями "высшего порядка", было бы естественно ожидать, что они должны обладать большими "правами и возможностями" по сравнению с сущностями "первого порядка". В мире людей дело обстоит именно так: дискриминация заключается в том, что вывешиваются таблички "только для...", и те, кого пускают - это "высшие", а кого не пускают - это "низшие". Но в мире программирования всё устроено ровно наоборот! В случае языка "первого порядка", разные ограничения "прав и свобод" имеют место как раз в отношении "высших". Например, строка может выдаваться в качестве результата функции, а функция - не может. Строка может быть элементом списка - а функция не может.

Поэтому, когда мы переходим от языка "первого порядка" к языку "высшего порядка", расширяются возможности как раз "высших сущностей", а не низших. А именно, в функциональном языке "высшего порядка", функции объявляются "полноправными значениями" (first-class values).

Кстати, не следует путать английские термины "first-order" и "first-class"! С виду - похоже, а смысл - разный. "First-class" - означает именно "полноправный", по аналогии с выражением "полноправный гражданин" ("a first-class citizen").

Итак, в чём же заключается "полноправие" функций в языке высшего порядка? А в том, что с функциями можно обращаться так же, как со значениями "первого порядка":

1. Новые функции могут порождаться динамически в процессе работы программы.

2. Функции могут передаваться внутрь других функций в качестве параметров.

3. Функции могут выдаваться в качестве результатов функций.

4. Функции могут вставляться внутрь данных "первого порядка" (например, в качестве элементов списков или аргументов конструкторов).

Итак, языки "высшего порядка" отличаются от языков "первого порядка" тем, что таблички "только для..." снимаются, и возможности функций возрастают. Но, конечно, на самом-то деле, возможности возрастают не только у функций, но и у программиста, который пишет программу. Можно делать то, что раньше делать было нельзя! Можно применять всякие трюки и приёмчики, которые в терминах языка первого порядка было невозможно даже сформулировать! При этом, однако, оказывается, что новые содержательные возможности требуют и некоторой ревизии на уровне синтаксиса языка программирования.

Рассмотрим, например, такую программу на языке первого порядка:

a1(Nil) = Nil;
a1(Cons(x, xs)) = Cons(S(x), a1(xs));
a2(xs) = a1(a1(xs));

Эта программа работает с натуральными числами, представленными в виде Z, S(Z), S(S(Z)), и списками, представленными в виде Cons(A, Cons(B, Cons(C, Nil))). Функция a1 "проходится" по элементам списка, и к каждому элементу списка прибавляет 1.

Эта функция нам понадобится в дальнейшем в качестве "подопытного кролика" для демонстрации некоторых аспектов суперкомпиляции, но в данный момент нас интересует форма, в которой она записана.

В языке первого порядка принято записывать применение функции f к аргументу x в виде f(x). До тех пор, пока функции не могут выдавать функции в качестве результата, такая запись удобна. Но, допустим, что результатом вычисления f(x) является функция, которую мы хотим применить к аргументу y. Тогда получается запись вида (f(x))(y). Выглядит уже как-то громоздко (даже если сократить её до f(x)(y)). Поэтому, в языках высшего порядка выражения вида f(x) начали записывать как f x. Преимущество такой записи особенно ясно проявляется именно в случае функций, вырабатывающих функции: вместо f(x)(y) получается f x y. При этом договорились, что "операция" применения функции а аргументу считается ассоциативной влево. Т.е. f x y z означает именно (((f x) y) z).

Извиняюсь, что трачу время и место для объяснения таких "тривиальных" вещей, но они тривиальны для тех, кто привык иметь дело с языками вроде SML или Хаскеля. А для всего остального человечества осознание того, что означает f x y z, требует некоторого "выворачивания мозгов наизнанку".

Конечно, переход к записи f x y z, кроме улучшения внешнего вида выражений, приводит и к некоторым другим последствиям. Например, в случае языков первого порядка, обычно имеются средства для определения функций от "нескольких аргументов". Например, применение функции f "от трёх аргументов" к x, y, z записывается как f(x, y, z). Что такое (x, y, z) - это в разных языках трактуется по-разному. Например, в SML считается, что все функции имеют ровно один аргумент, т.е. x, y, z нужно сначала "слепить" в одно значение (упорядоченную тройку), и подать на вход функции. А в некоторых языках, например, во входном языке специализатора Unmix или суперкомпилятора SPSC, считается, что каждая функция имеет фиксированную "арность" (arity), т.е. фиксированное количество аргументов на входе. В этом случае, запись f(x, y, z) должна восприниматься как единое целое, т.е. (x, y, z) без f отдельного смысла не имеет.

Однако, в случае языка высшего порядка, сразу же возникает "крамольная" мысль: а зачем нужны функции от нескольких аргументов. Вместо того, чтобы писать f(x, y, z) мы можем писать f x y z. При этом, конечно, требуется немного переопределить функцию f и считать, что после получения аргумента x функция f выдаёт не окончательный результат, а новую функцию (f x), которая ожидающую следующий аргумент y. Применяем эту функцию к y - и снова получаем функцию (f x y), ожидающую аргумент z. А вычислив (f x y) z получаем окончательный результат.

Что касается конструкторов для данных первого порядка (вроде конструктора Cons), то их вызовы тоже логично писать не как Cons(x, y), а как Cons x y...

Тут, правда, возникает такой вопрос: а как записать функцию, вырабатывающую функции? Для этого в языках высшего порядка предусмотрены "лямбда-выражения. Например, запись (\x -> S(x)) обозначает функцию, которая берёт x в качестве аргумента и надевает на него конструктор S. Другими словами функцию add1, надевающую S, можно определить двумя эквивалентными способами:

add1 x = S(x);

add1 = \x -> S(x);

Самое приятное свойство лямбда-выражений в том, что они, на самом деле, являются (в общем случае) не "функциональными константами", а "генераторами функций", поскольку при каждом исполнении лямбда-выражения может генерироваться новая функция! Например, если add - сложение чисел, то

addN n = \x -> add n x;

определяет такую функцию addN, что (addN n) вырабатывает функцию, прибавляющую n к аргументу. Например, addN (S(S(Z)) - это функция (\x -> add (S(S(Z))) x), прибавляющая 2 к аргументу. Весь фокус в том, что лямбда-выражение \x -> add n x содержит "свободную" переменную n, и для разных n лямбда-выражение генерирует разные функции.

Теперь у нас есть способ переделать функцию f вызывавшуюся как f(x, y, z), таким образом, чтобы её вызов выглядел как f x y z. А именно, если исходное определение функции f имело вид

f(x, y, z) = E;

его можно переделать так:

f = \x -> (\y -> (\ z -> E));

или даже как

f = \x y z -> E;

если воспользоваться тем, что в функциональных языках "с лямбдами" обычно считается, что "надевание лямбды" ассоциативно вправо. Т.е. \x -> \y -> E эквивалентно \x -> (\y -> E). Также, для краткости, разрешается записывать вложенные "лямбды" в сокращённом виде: \x y -> E эквивалентно \x -> \y -> E.

А ещё более кратко определение f можно записать в виде

f x y z = E;

что является сокращением для f = \x y z -> E;.

Уф! Покончив со всякой мутью, связанной с системами обозначений, займёмся, наконец, суперкомпиляцией. "Вернёмся к нашему барану" в виде функции a2. Перепишем её в обозначениях "высшего порядка":

a1 Nil = Nil;
a1 (Cons x xs) = Cons (S x) (a1 xs);
a2 xs = a1(a1 xs);

Стала ли от этого программа "лучше"? Дело вкуса и привычки... Во всяком случае, скобочек и запятых в программе стало меньше. Тут, правда, есть одна тонкость: в левых частях определения функции a1 появились образцы, которые анализируют структуру аргумента. На самом-то деле, эта запись является сокращением для некоторой комбинации из лямбда-выражений и "case-выражений", но мы пока вникать в это не будем, считая, что смысл функции a1 вполне понятен на неформальном уровне.

Теперь попытаемся просуперкомпилировать выражение a1(a1 us) в духе того, как это делалось в послании Что такое суперкомпиляция? .

Получается такой граф конфигураций:

Если построить по этому графу остаточную программу, получится такое определение функции:

a2 Nil = Nil;
a2(Cons x xs) = Cons (S(S x)) (a2 xs);

Теперь становится видно "невооружённым глазом", что в результате вычисления выражения a1(a1 us)), к каждому элементу списка us прибавляется 2.

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

А теперь наступает самый интересный момент! Изобразительные средства "высшего порядка" дают нам новые возможности по структуризации программ: во многих случаях монолитную программу удаётся представить в виде "композиции" из нескольких независимых частей. Т.е., конечно, это можно делать и в случае языка "первого порядка", но в случае "высшего порядка" таких возможностей больше: практически любой кусок программы из любого определения некоторой функции f можно "вырезать", объявить отдельной функцией g, и "вытащить" g за пределы определения функции f.

Вот, например, посмотрим внимательно на определение функции a1:

a1 Nil = Nil;
a1 (Cons x xs) = Cons (S x) (a1 xs);

В этом определении свалены в одну кучу две совершенно разные вещи:

1. Применение некоей операции к каждому элементу списка.

2. Прибавление единицы к числу.

Понятно, что пункт 1 - это некоторая общая идея, которая не зависит от того, что именно совершается над каждым элементом списка. А пункт 2 - это другая идея, которая никак не связана со списками. Поэтому, определение функции a1 мы можем "обобщить", добавив второй параметр, обозначающий произвольную операцию над элементом списка. Получается "классическая" функция map, а программа принимает вид:

map f Nil = Nil;
map f (Cons x xs) = Cons (f x) (map f xs);
a1 xs = map (\x -> S x) xs;

И теперь возникает возможность обобщить и задание, предлагаемое суперкомпилятору: пусть он теперь изучит, что получается при вычислении выражения вида

map g (map f us)

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

Не возникают ли от этого какие-то ужасные новые трудности в процессе суперкомпиляции? Посмотрим! Попробуем просуперкомпилировать выражение map g (map f us). Получается такой граф конфигураций:

Видно, что граф получается конечным из-за того, что из конфигурации map g (map f us) в конце-концов получается конфигурация map g (map f u1), совпадающая с исходной с точностью до имён переменных. Картина - очень похожая на ту, что наблюдалась в случае суперкомпиляции "первого порядка"...

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

map2 g f Nil = Nil;
map2 g f (Cons x xs) = Cons (g(f x)) (map2 g f xs);

Приятно и поучительно: суперкомпилятор обнаружил такой "закон природы": если ко всем элементам списка применить операцию f, а потом - операцию g, то это - то же самое, что один раз применить ко всем элементам списка композицию операций f и g.

(А в случае "первого порядка" суперкомпилятор делал то же самое, но для частного случая, когда f и g были операцией "прибавления единицы".)

А теперь возникает следующий вопрос: на бумаге-то у нас всё хорошо получилось. Но, как гласит народная мудрость, "гладко было на бумаге, да забыли про овраги"... В качестве ответа, до некоторой степени, может служить суперкомпилятор HOSC. Можно посмотреть на него и убедиться, что с кое-какими заданиями этот суперкомпилятор справляется. В том смысле, что структура остаточной программы не совпадает со структурой исходной программы. :-)

Представляет ли HOSC "практический интерес" (или, другими словами, можно ли его применить для "решения важной народнохозяйственной задачи"), пока сказать трудно. Но штука - забавная.

Осталось сделать несколько замечаний по поводу языка, программы на котором обрабатывает HOSC. Поскольку HOSC - это изделие экспериментальное, его входной язык - "минималистский". По сути он представляет собой некоторое подмножество Хаскеля (Haskell). Этот язык (в его состоянии на данный момент) описан на странице Higher Order Lazy Language (HLL).

HLL - язык со статической типизацией (в смысли Хиндли-Милнера). Писать определения функций в виде

f x y z = E;

пока не разрешается. Нужно писать с "лямбдами" в правой части:

f = \x y z -> E;

Сопоставление с образцом можно делать с помощью case-выражений, в которых каждый образец имеет простейший вид: c x1 x2 ... xN. Поэтому, определение функции map

map f Nil = Nil;
map f (Cons x xs) = Cons (f x) (map f xs);

на самом деле, должно быть записано так:

map = \f us -> case us of {
  Nil -> Nil;
  Cons x xs -> Cons (f x) (map f xs);
};

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

map2 g f Nil = Nil;
map2 g f (Cons x xs) = Cons (g(f x)) (map2 g f xs);

можно переписать так:

map2 = \g f us ->
  letrec loop = \us -> case us of {
    Nil -> Nil;
    Cons x xs -> Cons (g (f x)) (loop xs);
  } in loop us;

HOSC активно использует letrec-и при генерации остаточной программы.

Вот пример полного задания на суперкомпиляцию:

data List a = Nil | Cons a (List a);
data Nat = Z | S Nat;

mapN (S(S(S Z))) f xs

where

map = \f us -> case us of {
  Nil -> Nil;
  Cons x xs -> Cons (f x) (map f xs);
};

mapN = \n f us -> case n of {
  Z -> us;
  S n1 -> map f (mapN n1 f us);
};

Здесь сначала идут объявления типов данных, используемых в программе. Потом - выражение, которое вычисляет программа (и которое становится начальной конфигурацией при суперкомпиляции). Через свободные переменные этого выражения в программу передаются начальные данные при запуске. Затем идёт ключевое слово where, за которым следуют объявления функций. Засовываем эту программу в HOSC (задание mapN n f xs), и получаем такой результат:

data List a = Nil | Cons a (List a);
data Nat = Z | S Nat;
(letrec g=(\x4-> case x4 of {
    Nil -> Nil;
    Cons s2 z1 -> (Cons (f (f (f s2))) (g z1)); })
  in (g xs))

Результат неплохой. Функция mapN применяет функцию f ко всем элементам списка xs, повторяя эту процедуру n раз. В данном случае в начальном выражении задаётся, что n=3. И в остаточной программе получается однопроходный алгоритм, который применяет f к каждому элементу списка xs три раза.

Читать дальше...

С чем едят "гомеоморфное вложение"

При "прогонке" (символическом/обобщённом исполнении программы) в общем случае получается бесконечное дерево конфигураций. Задача суперкомпиляции - превратить это дерево в конечный граф.

В заметке Что такое суперкомпиляция? был рассмотрено такое простейшее "правило зацикливания". Допустим, в дереве встретился такой узел, который содержит конфигурацию X2, и при этому среди предков этого узла в дереве есть конфигурация X1, такая, что X1 и X2 совпадают (с точностью до переименования переменных). Понятно, что при таких условиях нет смысла строить поддерево для X2, поскольку оно будет выглядеть точно так же, как и поддерево, подвешенное к X1.

Поэтому выполнялась следующая операция. К графу добавлялась обратная стрелка из X2 в X1, а поддерево, подвешенное к X2 удалялось из графа. Точнее, оно не удалялось, а вообще не строилось!

Вот так и получался конечный граф. Правда, только для некоторых "особенно хороших" исходных программ.

В заметке Обобщение конфигураций при суперкомпиляции рассматривалось более сложное "правило зацикливания". Допустим, что X2 и X1 - действительно разные (X1 нельзя превратить в X2 простым переименованием переменных), но X2 является "частным случаем" X1. В том смысле, что применив к переменным в X1 некоторую подстановку, можно превратить X1 в X2. Тогда можно преобразовать X2 таким образом, чтобы она совпала с X1 (с точностью до переименования переменных). Это делается так: выдумываем новые, уникальные имена переменных v1, ..., vk и X2 приводится к виду

let v1 = E1,..., vk = Ek in E0

где E0 уже совпадает с X1 (с точностью до переименования переменных). На следующем шаге, let-выражение разбирается на части E0, E1,..., Ek, каждая из которых обрабатывается отдельно. При этом уже можно добавить к графу обратную стрелку из E0 в X1.

Переход от X2 к let-выражению, содержащему E0, называется "обобщением", поскольку X2 является "частным случаем" E0.

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

И способ борьбы с разрастанием дерева - понятен. Если встретилась конфигурация, которая является частным случаем уже рассмотренной конфигурации - сводим более специфическую конфигурацию к более общей. Возникает вопрос: достаточно ли этого правила, чтобы получить конечный граф конфигураций для любой исходной программы? Ответ на это - отрицательный... (Видимо, Судьба так распорядилась, чтобы авторам суперкомпиляторов жизнь мёдом не казалась. :-) )

Рассмотрим следующих (простой - но коварный) пример программы. Определим функцию умножения mult через уже нам известную функция сложения add.

add(Z, y) = y;
add(S(x), y) = S(add(x, y));
mult(Z, y) = Z;
mult(S(x), y) = add(mult(x, y), y);

При этом, натуральные числа 0, 1, 2, 3 представлены в виде Z, S(Z), S(S(Z)), S(S(S(Z))),... , а определения функций основаны на следующих свойствах натуральных чисел:

0+y = y
(x+1)+y = (x+y)+1
0*y = 0
(x+1)*y =x*y+y

Возьмём начальную конфигурацию mult(a, b) и попробуем построить из неё граф конфигураций. Получается такое дерево:

Видно, что если пойти по правой ветви этого дерева, то получается такая последовательность конфигураций:

mult(a, b)
add(mult(a1, b), b)
add(add(mult(a2, b), b), b)
add(add(add(mult(a3, b), b), b), b)

Получается так, что ни одна из конфигураций не является "частным случаем" какой-либо из предыдущих конфигураций! Так получается из-за того, что с каждым шагом снаружи добавляется новый вызов функции add.

Что делать? Здравый смысл подсказывает, что у всех этих конфигураций всё же есть общая часть: подвыражение вида mult(ak, b). В частности, можно свести add(mult(a1, b), b) к mult(a, b) с помощью "обобщения", использовав конструкцию let:

let v1 = mult(a1, b), v2 = b in add(v1, v2)

после чего уже можно добавить к графу обратную стрелку от mult(a1, b) к mult(a, b). В результате получается такой (незаконченный) граф конфигураций:

Cуперкомпилятор SPSC действительно разделывается с этой программой именно так: mult(a,b)! Правда, результат суперкомпиляции какой-то неинтересный: остаточная программа, по существу, совпадает с исходной... Ну так ведь и программа такова, что непонятно, что можно было бы сделать с ней интересного? Вот если бы начальная конфигурация была не mult(a, b), а какого-то более специального вида... Но об этом - позже.

А сейчас попытаемся сформулировать "правило зацикливания", которое было бы обобщением правила, описанного в заметке Обобщение конфигураций при суперкомпиляции. Там мы просто проверяли, является ли X2 "частным случаем" X1. А только что мы столкнулись с ситуацией, когда X2 не является частным случаем X1, но внутри X2 "зарыто" подвыражение Y, которое является-таки частным случаем выражения X1. Тогда можно, с помощью конструкции let "вытащить" Y из X2 "на поверхность":

let v = Y in E

где E{v:=Y} = X2. После этого можно разобрать let на части и добавить обратную стрелку от Y к X1.

Всегда ли это помогает? Как и следовало ожидать - не всегда. Рассмотрим опять фунцию сложения add и попробуем просуперкомпилировать конфигурацию начальную add(a, a). Когда мы суперкомпилировали add(a, b), всё получалось хорошо. Но в случае add(a, a) различие заключается в том, что переменная a повторяется 2 раза! Казалось бы, ну чего в этом плохого? А вот сейчас и увидим!

В результате прогонки получается такое дерево:

Видно, что порождается такая последовательность конфигураций:

add(a, a)
add(a1, S(a1))
add(a2, S(S(a2)))
add(a3, S(S(S(a3))))

Плохо дело! Конфигурации всё раздуваются и раздуваются! И ни одна из них не является частным случаем предыдущий. Попробуем, например, найти подстановку, такую, чтобы add(a, a) совпало c add(a1, S(a1)). По сути, надо решить уравнение

add(a, a) = add(a1, S(a1))

подобрав для a такую подстановку, чтобы левая часть совпала с правой. Такого значения для a подобрать невозможно. (В этом месте я написал длинное и нудное объяснение, почему невозможно, но потом его вымарал. Как известно, очевидные вещи гораздо труднее объяснять, чем неочевидные. :-))

Чтобы получился конечный граф, нужно сделать обобщение (с помощью всё той же конструкции let). В данном случае, беда произошла из-за того, что переменная a входит в add(a, a) два раза. Так сделаем из одной переменной две разные:

let v1 = a, v2 = a in add(v1, v2)

теперь конфигурация add(a, a) превратилась в add(v1, v2). А как суперкомпилируется такая конфигурация - мы уже разбирали в заметке Что такое суперкомпиляция?: получается конечное дерево конфигураций.

Сразу следует отметить одну тонкость. До сих пор мы делали обобщение таким способом: сравнивали "верхнюю" конфигурацию X1 с "нижней" конфигурацией X2 и "обобщали" X2 таким образом, чтобы она совпала с X1 (с точностью до имён переменных). Например, сравнивали add(a, b) и add(a1, S(b)) и обобщали add(a1, S(b)) до add(v1, v2). При этом, "прогресс" при построении графа конфигураций был непрерывным и "поступательным": к уже существующим узлам пристраивались дополнительные узлы и стрелки.

Но при сравнении add(a, a) и add(a1, S(a1)) мы столкнулись с принципиально другим случаем! add(a1, S(a1)) невозможно обобщить до add(a, a)! Конечно, можно преобразовать add(a1, S(a1)) следующим образом:

let v1 = a1, v2 = S(a1) in add(v1, v2)

При этом, получается, что add(a1, S(a1)) - это частный случай add(v1, v2). Но беда в том, что add(v1, v2) не является частным случаем add(a, a) (чего нам хотелось бы добиться). Совсем наоборот! add(a, a) - это частный случай add(v1, v2), поскольку существует такая подстановка {v1:=a, v2:= a}, что

add(v1, v2){v1:=a, v2:= a} = add(a, a)

Вот так-то! Абстрактно говоря, сначала встретилась конфигурация X1, а потом - конфигурация X2. Попробовали обобщить X2 до X1, но выяснилось, что это невозможно. Единственно, чего можно добиться, так это найти такую конфигурацию Y, которая является обобщением как по отношению к X1, так и по отношению к X2. В данном случае:

add(v1, v2){v1:=a, v2:= a} = add(a, a)
add(v1, v2){v1:=a1, v2:=S(b)} = add(a1, S(b))

Как должен действовать суперкомпилятор в подобных случаях? Наверное, возможны разные варианты... Но, наверное, самое простое решение проблемы таково.

Как мы помним, граф конфигураций - это дерево плюс обратные стрелки. X2 находится в поддереве, подвешенном под X1. Пусть Y - обобщение по отношению к X1 и X2. Тогда суперкомпилятор уничтожает всё поддерево, подвешенное к X1 (в том числе - и X2), а узел X1 заменяет на узел вида

let v1 = E1,..., vk = Ek in Y

После чего суперкомпиляция продолжается. Суперкомпилятор SPSC именно так и поступает: add(a, a)!

Однако, новизна ситуации в том, что вместо поступательного построения дерева получается некоторая последовательность попыток: строим поддерево, "разочаровываемся" в нём, уничтожаем его, обобщаем конфигурацию, из которой оно выросло, строим поддерево заново и т.д. Какая-то подозрительная ситуация! А вдруг, этот процесс будет продолжаться бесконечно? Как ни странно, оказывается, если всё делать аккуратно, процесс завершается. Кто сомневается, может проштудировать обстоятельную статью Сёренсена, в которой всё что надо научно доказываются:

Sørensen, M. B. 2000. Convergence of program transformers in the metric space of trees. Sci. Comput. Program. 37, 1-3 (May. 2000), 163-205. DOI= http://dx.doi.org/10.1016/S0167-6423(99)00026-X

Итак, если мы решили, что две конфигурации X1 и X2 - "похожи", то можно либо обобщить X2 до X1, либо, на худой конец, построить конфигурацию Y, являющуюся обобщением по отношению как к X1, так и к X2. Вопрос только в том, как формализовать само понятие "похожи"? Можно было бы рассматривать некоторое симметричное отношение "похожести" для конфигураций, но нам нужно не это. Суперкомпиляция - это имитация "обычных" вычислений. Тем самым, процесс суперкомпиляции имеет некоторое направление! Поэтому, при сравнении конфигураций нужно учитывать, какая из конфигураций появилсь раньше, а какая - позже.

А само сравнение конфигураций делается для того, чтобы процесс построения дерева конфигураций (с обратными стрелками, превращающими его в граф) завершался за конечное время.

Вот, допустим, под конфигурацией X1 в дереве висит конфигурация X2. Нам нужно решить, нужно ли обобщать X2 (или даже X2 вместе с X1), или же дела идут хорошо, и можно продолжать процесс, приделывая, с помощью прогонки, к X2 новое поддерево.

Здесь возникает конфликт интересов. С одной стороны, суперкомпиляция делается для того, чтобы проанализировать поведение программы "в общем виде". Каждая конфигурация описывает некоторое множество возможных состояний вычислительного процесса. Если конфигураций в дереве конфигураций много, это означает, что суперкомпилятор разбивает множество состояний на много частей, рассматривает много частных случаев. Стало быть, анализ процесса вычислений - утончённый и глубокий. А если конфигураций мало - это означает, что суперкомпилятор работает "топорно", и ничего интересного с помощью суперкомпиляции не получается (например, на выходе суперкомпилятора просто вываливается исходная программа).

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

Таким образом, если не обобщать - дерево конфигураций может получиться бесконечным. А если слишком ретиво обобщать - дерево получится конечным, но неинтересным.

Итак, разумным представляется такой подход: сравниваем X1 и X2. Если X2 на X1 "непохожа", то не обобщаем X2 и X1. А если X2 "похожа" на X1, то надо изучить ситуацию подробнее. Если X2 - "меньше по размерам", чем X1, то разумно X2 не обобщать, поскольку количество конфигураций, которые "меньше", чем X1 - конечно, и мы можем себе позволить их все перебрать не рискуя тем, что дерево конфигураций получится бесконечным. (Разумеется, это верно, если понятие "меньше" определено надлежащим образом.) А вот если X1 и X2 похожи, и при этом X2 - "больше", чем X1, то ситуация - опасная, нужно обощать! Введем для ситуации, когда X1 и X2 "похожи", но при этом X2 - "больше", чем X1, такое обозначение:

X1 <| X2

Как определить такое отношение, разные умные люди думали. Но первыми придумали Хигман (Higman) и Крускал (Kruskal). (Кстати, именно "КрУскал", а не "КрускАль", поскольку Kruskal - не француз. Был бы француз, его фамилия писалась бы как "Crouscal".)

Хигман и Крускал догадались, что определить отношение <| можно гениально простым способом! А именно, пусть считается, что X1 <| X2, если X2 можно превратить в X1 стерев в X2 некоторые его части. Сразу убивается два зайца:

• Если X2 можно превратить в X1, кое-что стирая в X2, то кто же усомнится, что X1 и X2 - "похожи"?

• Если X2 можно превратить в X1, кое-что стирая в X2, то это и означает, что X2 - "толще" или "больше", чем X1.

Хигман применил эту идею к линейным строкам, а Крускал - обобщил для деревьев (термов, составленных из n-арных конструкторов). А отношение <| научно назвали "отношением гомеоморфного вложения", так что, X1 <| X2 читается так: "X1 гомеоморфно вложено в X2". Ну да, можно считать, что X1 полностью присутствует в X2, но в "разбавленном" виде. Например, если у нас есть 50 граммов коньяка, и мы доливаем в него 150 граммов водки, можно считать, что в получившейся смеси 50 граммов коньяка "вложены" в 200 граммов получившейся смеси. При этом, исходные 50 граммов коняка можно получить обратно, отпив из стакана 150 граммов водки.

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

Leuschel, M. 2002. Homeomorphic embedding for online termination of symbolic methods. In the Essence of Computation: Complexity, Analysis, Transformation, T. Æ. Mogensen, D. A. Schmidt, and I. H. Sudborough, Eds. Springer-Verlag New York, New York, NY, 379-403.

Рассмотрим, например add(a, b) и add(a1, S(b)). Верно ли, что

add(a, b) <| add(a1, S(b))

? Верно! Подтираем в add(a1, S(b)) конструктор S и получаем add(a1, b). А это выражение совпадает с add(a, b) с точностью до имён переменных.

Рассмотрим mult(a, b) и add(mult(a1, b), b). Верно ли, что

mult(a, b) <| add(mult(a1, b), b)

? Верно! Подтираем в add(mult(a1, b), b) вызов функции add с её вторым аргументом, и получаем mult(a1, b), что совпадает с mult(a, b) с точностью до имён переменных.

Рассмотрим add(a, a) и add(a1, S(a1)). Верно ли, что

add(a, a) <| add(a1, S(a1))

? Верно! Стираем в add(a1, S(a1)) конструктор S и получаем add(a1, a1), что совпадает с add(a, a) с точностью до имён переменных.

Можно дать и формальное определение гомеоморфного вложения с помощью индуктивного определения в виде трёх правил:

1. x <| y для любых переменных x и y.

2. X <| f(E1,...,Ek), если f - имя конструктора или функции, и для некоторого i выполнено X <| Ei.

3. f(X1,...,Xk) <| f(Y1,...,Yk), если f - имя конструктора или функции, и для всех i выполнено Xi <| Yi.

Правило 2 называется правилом "ныряния" (левое выражение "ныряет" в один из аргументов правого), а привило 3 - правилом "сочетания" (аргументы конструктора/функции с двух сторон "сочетаются браком" друг с другом).

Интересно, что отношение гомеоморфного вложения нашло первое применение не в суперкомпиляции, а в системах переписывания термов:

Dershowitz, N. and Jouannaud, J. 1990. Rewrite systems. In Handbook of theoretical Computer Science (Vol. B): Formal Models and Semantics, J. van Leeuwen, Ed. MIT Press, Cambridge, MA, 243-320.

Некоторое время спустя, Мортен Сёренсен и Роберт Глюк задумчиво сидели в DIKU (что означает Факультет Информатики Копенгагенского Университета) и ломали голову над проблемой сравнения конфигураций. И тут к ним в комнату вошёл Нил Джоунс с какой-то статьёй в руках и спросил "А не это ли вы ищете?". А в статье было описано отношение гомеоморфного вложения. Оказалось, что именно это и искали... После чего, Сёренсен и Глюк и написали вот эту статью:

M. H. Sørensen and R. Glück. An algorithm of generalization in positive super-compilation. In J. W. Lloyd, editor, Proceedings of ILPS'95, the International Logic Programming Symposium, pages 465-479, Portland, USA, December 1995. MIT Press.

Интересно, что отношение <| хорошо работает также в случаях, когда у суперкомпилятора появляется возможность выполнить какие-то вычисления над известными частями данных во время суперкомпиляции. Например, вспомним функцию addAcc, которая выполняет сложение с помощью накапливающего параметра (аккумулятора):

addAcc(Z, y) = y;
addAcc(S(x), y) = addAcc(x, S(y));

Попробуем просуперкомпилировать выражение addAcc(S(S(a)), b). Как с ним разделывается суперкомпилятор SPSC? А вот так: addAcc(S(S(a)), b). На одной из ветвей дерева получается такая последовательность конфигураций:

1. addAcc(S(S(a)), b)
2. addAcc(S(a), S(b))
3. addAcc(a, S(S(b)))
4. addAcc(a1, S(S(S(b))))

Видно, что второй аргумент всё время угрожающе раздувается. Но суперкомпилятор не пугается! Второй аргумент раздувается, но зато первый аргумент уменьшается. Поэтому конфигурация 1 не вложена в конфигурации 2, 3 и 4, а конфигурация 2 - в конфигурации 3 и 4. А вот конфигурация 3 вложена в конфигурацию 4! И при этом 4 является частным случаем 3. Поэтому, 4 обобщается до 3 и в дереве конфигураций создаётся обратная стрелка на конфигурацию 3.

Возникает такой вопрос: а не может ли получиться так, что в процессе прогонки у нас всё время будут получаться всё время разные конфигурации, которые не буду вкладываться друг в друга. Оказывается, это не так! Для любой бесконечной последовательности конфигураций X1, X2, X3,... обязательно найдутся такие i и j, что i < j и

Xi <| Xj

Соответствующую теорему доказали Хигман и Крускал. Крускал - для случая, когда выражения составлены только из конструкторов. При этом принципиальным является то, что все конструкторы принадлежат конечному множеству. Однако, в суперкомпиляторе SPSC, например, выражения могут содержать ещё и вызовы функций, и переменные. Однако, теорема всё равно применима, поскольку вызовы функций, с синтаксической точки зрения - то же, что и конструкторы (а смысл термов для гомеоморфного вложения безразличен). При этом, в конфигурациях могут появляться только те конструкторы и имена функций, которые присутствуют в исходной программе. Некоторую проблему представляют переменные, ибо переменные-то могут появляться в конфигурациях в неограниченном количестве: суперкомпилятор их генерирует по мере надобности. Как быть? Простейшее решение, свалить все переменных в одну кучу и не различать их между собой. Т.е. считать, что

x <| y

для любых переменных x и y. Вот и получается, что с точки зрения <| переменная как бы одна-единственная, и её можно воспринимать как нуль-арный конструктор.

Тут следует упомянуть, что Турчиным был предложен и другой подход к организации обобщения и зацикливания в суперкомпиляторе, не основанный на гомеоморфном вложении конфигураций:

Turchin, V., The Algorithm of Generalization in the Supercompiler, in: Proceedings of the IFIP TC2 Workshop on Partial Evaluation and Mixed Computation, 1988, pp. 531--549. PDF

Но об этом надо будет написать отдельно...

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

Можно посмотреть, как всё это реализовано в специализаторе суперкомпиляторе SPSC, написанном на языке Scala (который, по сути, можно рассматривать как некий синтез Standard ML и Java). Для "учебных" целей был изготовлен "облегчённый" вариант SPSC, SPSC Light, исходные тексты которого выставлены там же. SPSC Light полностью работоспособен: в нём присутствуют все "принципиально важные" элементы суперкомпилятора, но опущены некоторые неинтересные части (вроде проверки разных контекстных ограничений на входные программы).

Читать дальше...