Сергей Романенко
29 января 2010 г.
В послании
обсуждалась возможность записывать явные рекурсивные определения данных. А нельзя ли вообще без них обойтись?
Как известно, в “чистом, классическом” λ-исчислении нет ничего, кроме λ-термов и явные рекурсивные определения писать нельзя. Тем не менее, с помощью некоторых трюков (вроде “оператора неподвижной точки”) рекурсивные определения всё же удаётся записать.
Возникает два интересных вопроса:
Начнём с первой проблемы.
HLL - язык со статической типизацией (по Хиндли-Милнеру). А насколько суровы ограничения, накладываемые такой типизацией? Что они не разрешают делать?
Рассмотрим выражение
\x -> x x
знакомое всем, кто интересовался теорией бестипового λ-исчисления. Для этого знаменитого выражения даже существует традиционное обозначение: буква омега. Итак, пусть
omega = \x -> x x
Чем же это выражение интересно? Да тем, что с его помощью конструируется “самовоспроизводящееся” выражение. А именно,
omega omega ⟹ (\x -> x x) omega ⟹ omega omega
А можно ли написать в HLL-программе \x -> x x? Нельзя! Не разрешает
типизация по Хиндли-Милнеру применять функцию саму к себе.
Действительно, какой тип должна иметь переменная x? Раз написано x x,
значит, x применяется к аргументу x. Стало быть, тип переменной x должен
иметь вид a -> b, где a - тип аргумента. Но аргументом является x. Стало
быть, получается, что a = a -> b. Попробуем решить это уравнение. Получается
a = a -> b = (a -> b) -> b = ((a -> b) -> b) -> b = ...
т.е. тип переменной x - бесконечное типовое выражение. Но по правилам
игры, установленным Хиндли и Милнером все типы должны изображаться
конечными выражениями, т.е. считается, что уравнение a = a -> b решений
не имеет. Стало быть, omega не является типизируемым!
Однако, как известно (в некоторых случаях) строгость законов уравновешивается необязательностью их исполнения. Ну, или тем, что в законах оставлены лазейки, позволяющие их нарушать, формально как бы и не нарушая. А именно, оказывается, что лазейку предоставляют типы данных, определяемые в программе.
Уравнение a = a -> a решений не имеет, но зато, как показывает пример
не запрещено определять типы данных вроде:
data D = F (D -> D);
Добавили конструктор F - и вот уже D “почти” равно D -> D (с точностью
до надевания конструктора F). Было нельзя - и вдруг стало можно! Но,
конечно, прямо так напрямую написать x x - нельзя. Если объявить, что
типом переменной x является D - то получится, что x - не функция, а
функция, на которую надет конструктор F, ибо D = F (D -> D). Но это - не
страшно, конструктор ведь можно и снять. И для этого можно определить
функцию apply:
apply = \x y -> case x of { F f -> f y; };
Идея функции проста: при вычислении apply e1 e2, e1 должно выдать
результат вида F f, где f - функция. Снимаем тег F и вычисляем f e2.
Причём, если присмотреться к определению функции apply, видно, что это
определение можно ещё немного упростить: оставить только снятие тега F,
чтобы выражение apply e1 выдавало функцию, которую уже можно к чему-то
применить. Тогда получается такое определение:
apply = \x -> case x of { F f -> f; };
Теперь всё это собираем в одно задание на суперкомпиляцию
data D = F (D -> D);
apply omega omega
where
apply = \x -> case x of { F f -> f; };
omega = F (\x -> apply x x);
и получаем такую приятную остаточную программу
data D = F (D->D); (letrec f=f in f)
из которой видно, что суперкомпилятор правильно распознал, что при
вычислении apply omega omega какого-либо результата сколько ни жди - не
дождёшься…
Теперь, чтобы окончательно убедиться в том, что “невозможное -
возможно”, изобразим средствами HLL что-нибудь нетривиальное из
нетипизированного λ-исчисления. А именно, определим “оператор
неподвижной точки” fix не используя явную рекурсию. Классическое
рекурсивное определение функции fix выглядит так:
fix = \f -> f (fix f);
Но, как учат нас учебники по λ-исчислению, без рекурсии можно
обойтись, определив fix, например, так:
fix = \f -> (\x -> f (x x))(\x -> f (x x))
Приглядевшись, в этом выражении можно узнать слегка
“усовершенствованное” выражение omega omega. Но в HLL прямо так
определить fix нельзя: нужно использовать тот же трюк, который мы
применяли к omega omega. Что и сделано в примере
Получается такая программа
data D = F (D -> D);
fix
where
apply = \x -> case x of { F f -> f; };
fix = \f -> apply (F (\x -> f (apply x x)))(F (\x -> f (apply x x)));
Просуперкомпилировав её, получаем
data D = F (D->D); \f -> (letrec g = f g in g)
Легко видеть, что \f -> (letrec g = f g in g) - это то же самое, что
fix = \f -> f (fix f);
хотя и записано немного по другому. Разница в том, что fix вынужден
таскать с собой аргумент f в процессе вычисления, а если использовать
letreс, то f может быть свободной переменной по отношению к letrec. Т.е.
получается, что g - вроде как бы даже и не “функция”, а “структура
данных” (раз у неё нет аргумента). Молодец, HOSC! Нетривиальное
преобразование сумел выполнить.
Однако, нужно заметить, что fix мы закодировали без использования
рекурсии только, так сказать, из “спортивного интереса”, чтобы
посмотреть, испугается ли такого задания HOSC или нет. Не испугался! А
на самом деле, Хиндли-Милнер, как это ни странно, разрешает нам
определить fix прямо через рекурсию следующим образом:
fix = \f -> f (fix f);
Несмотря на то, что fix f подсовывается под f в качестве аргумента! Как
же так? Разве можно функцию f подсовывать самой себе (не используя
теги)? Оказывается, что можно. Какой тип должен иметь fix? Это можно
выяснить с помощью таких рассуждений. Исходим из того, что
fix f = f (fix f). Из выражения f (fix f) следует, что f - функция.
Стало быть, её тип должен иметь вид a -> b, где a - это тип выражения
fix f. Но и fix - функция, аргумент которой имеет тип a -> b.
Значит, у fix тип должен быть (a -> b) -> c. А поскольку fix f в f(fix f) является аргументом f, получается, что c = a.
Итак, у f тип a -> b, у fix тип (a -> b) -> a, у fix f тип a,
у f(fix f) тип b. Вспоминаем, что fix f = f(fix f), и типы у них должны совпадать. Стало быть, a = b. Итак, у fix тип (a -> a) -> a и все концы
благополучно сошлись с концами!
Поэтому, чтобы не возиться с тегами, определим fix как
fix = \f -> f (fix f);
и попробуем выполнить “фигуру высшего пилотажа”: закодировать взаимную
рекурсию двух определений без использования явной рекурсии через функцию
fix. Как же это сделать, если у fix аргумент только один, а нам нужно с
его помощью закодировать два определения? А это можно сделать, подсунув
под fix функцию, аргументом которой является пара, а результатом - тоже
пара. Так и сделано в примере
В этом примере пара рекурсивных определений
p = A q;
q = B p;
записана без помощи явной рекурсии. Идея заключается в том, что два
уравнения можно объединить в одно, используя конструктор пар P:
P p q = P (A q) (B p);
Однако, прямо так написать нельзя, поскольку в HLL в левой части определения должна стоять переменная. Но это - не беда. Перепишем определения в виде
r = P (A q) (B p);
p = fst r;
q = snd r;
где fst и snd - функции, выбирающие первый и второй элемент пары
соответственно. Теперь, подставляя вместо p и q их определения, получаем
r = P (A (snd r))(B (fst r));
p = fst r;
Ну, а это уже легко выражается через fix. В результате, задание на
суперкомпиляцию выглядит так:
data Input = A Input | B Input;
data Pair a b = P a b;
fst(fix (\r -> P (A (snd r)) (B (fst r))))
where
fst = \u -> case u of { P x y -> x; };
snd = \u -> case u of { P x y -> y; };
fix = \f -> f(fix f);
А в результате суперкомпиляции получается следующая остаточная программа:
data Input = A Input | B Input;
data Pair a b = P a b;
letrec f=(A (B f)) in f
Таким образом, мы видим, что HOSC в очередной раз справился с преобразованием неявной рекурсии (через редукцию) в явное рекурсивное определение (удалив при этом много промежуточных шагов редукции).