Сергей Романенко
4 января 2010 г.
В посланиях
рассматривались два способа встраивания проблемно-ориентированного (ПО) языка. Первый способ - “честно” написать интерпретатор ПО-языка, представив программы на ПО-языке в виде констант первого порядка (деревьев абстрактного синтаксиса, например). Второй способ - реализовать ПО-язык через набор функций высшего порядка (комбинаторов), представив каждую конструкцию ПО-языка в виде функции (комбинатора) высшего порядка.
И в первом, и во втором случае, эффективность исполнения ПО-программ можно увеличить, подвергнув их суперкомпиляции, при этом после суперкомпиляции, вроде бы, получаются вполне приличные остаточные программы (сопоставимые с программами, написанными вручную).
Общий вывод был такой:
Нехорошо, что теги загаживают остаточную программу. Но, между прочим, теги ещё и отравляют жизнь при попытке реализовать в ПО-языке циклические определения данных и функций! Вот с этой стороной дела мы и попробуем сейчас разобраться более подробно.
Итак, в послании
был рассмотрен интерпретатор первого порядка, для бестипового
λ-исчисления. При этом λ-исчисление было “нечистым”: в
λ-термах можно было использовать натуральные числа и записывать
рекурсивные определения с помощью конструкции fix f-> e, эквивалентной
letrec f = e in f.
Однако же, не приводилось ни одного примера того, что получается при
попытке просуперкомпилировать выражения, содержащие fix. И неспроста,
ибо при суперкомпиляции получаются явные гадости, и обсуждение этих
интересных и поучительных гадостей отвлекло бы нас от главной темы
послания. Но теперь наступил подходящий момент, чтобы выложить все карты
на стол и узнать горькую правду. Раскрываем уже известное нам задание на
суперкомпиляцию Lambda: first-order syntax (HOCL)
и пробуем просуперкомпилировать выражение
run (Fix VZ (NatS (Var VZ)))
в более “человеческом” синтаксисе это выражение выглядит так:
fix(\n -> S n). А поскольку главное свойство конструкции fix состоит в
том, что fix f = f(fix f), имеем
fix(\n-> S n) ⟹ (\n-> S n)(fix(\n-> S n)) ⟹ S (fix(\n-> S n))
Наружу вытолкнулся конструктор S а в его аргументе оказалось исходное
выражение. Отсюда очевидно, что вычисление fix(\n -> S n) должно
порождать “бесконечное” натуральное число S (S (S ( ... ))).
Отлично, суперкомпилируем run (Fix VZ (NatS (Var VZ))) и что получаем? А
получаем такой замечательный результат:
(letrec f=case f of { Error -> Error;
F g -> Error;
N n -> (N (S n));
} in f)
Когда я увидел это в первый раз, то я некоторое время хлопал глазами, а
потом мне прямо-таки стало нехорошо… Что бы такой результат мог
означать? Ну хорошо, есть в нём дурацкие манипуляции с тегами. Вместо
того, чтобы просто надеть на число n конструктор S, мы сначала снимаем с
n тег N, потом надеваем S, а потом снова надеваем N. Ну, ещё и
проверять приходится, что число - это число. Ладно! Это всё - зло понятное и
необходимое (для интерпретатора первого порядка). Смущает другое! В
данном случае, letrec - это форма записи уравнения
f=case f of { Error -> Error; F g -> Error; N n -> (N (S n)); }
и решение этого уравнения является “смыслом” конструкции. Есть ли у
этого уравнения решение? О да! Например, подставим в правую часть в
качестве значения f бесконечное выражение N (S(S(...))) и выполним шаг
редукции
case N(S(S(...))) of { Error -> Error;
F g -> Error;
N n -> (N (S n)); } ⟹
N(S(S(S(...))))
И в результате получилось то же самое выражение N(S(S(...))) ! Оно,
конечно, один конструктор S внутри добавился, но раз выражение S(S(...))
бесконечное, от этого ничего не изменилось. Стало быть, N(S(S(...)))
является решением уравнения. Чего и следовало ожидать. Хоть и выглядит
этот letrec диковато, но решение-то правильное даёт! А что получится,
если мы попробуем подставить f = Error? И Error подходит в качестве
решения!
case Error of { Error -> Error; F g -> Error; N n -> (N (S n)); } ⟹ Error
А если попробовать f = F (\x -> x)? Получается
case F (\x -> x) of { Error -> Error;
F g -> Error;
N n -> (N (S n)); } ⟹
Error
Ну, слава Богу, хоть F (\x -> x) в качестве решения не годится,
поскольку в результате редукции получается что-то другое (Error).
Итак, подозрение, что в конструкции
(letrec f=case f of { Error -> Error;
F g -> Error;
N n -> (N (S n));
} in f)
таится какая-то гнильца, вполне оправдывается. При этом, патология не в
том, что эта конструкция не имеет смысла, а в том, что этих смыслов
слишком много: один смысл N(S(S(...))), а другой - Error. А какой же из
них является “истинным”? Как говорят в кино, “в конце должен остаться
только один” (ну, или “Росинант не вынесет двоих).
Поэтому я сначала решил, что такое остаточное выражение - результат какой-то ошибки в суперкомпиляторе HOSC. Исправит Илья Ключников ошибочку - и станет хорошо. Но, после некоторых дополнительных размышлений, я понял, что HOSC в данном случае не виноват! HOSC строго сохраняет семантику программ (не расширяя и не сужая область определения функций). Поэтому HOSC не породил, а выявил проблему, запрятанную в недрах интерпретатора, подвергшегося суперкомпиляции!
Если встать на математическую точку зрения, то конструкция
(letrec f=case f of { Error -> Error;
F g -> Error;
N n -> (N (S n));
} in f)
имеет не два смысла, а только один! Как написано в учебниках,
посвящённых денотационной семантике программ, смыслом программы является
не любая неподвижная точка, а минимальная неподвижная точка! А
минимальной неподвижной точкой в данном случае является “дно” (bottom).
А Error и N(S(S(...))) хотя и являются решениями уравнения, но они не
минимальны.
А если взглянуть на проблему “по рабоче-крестьянски”, т.е. с
операционной, а не денотационной точки зрения, то фокус в том,
что при попытке вычислить выражение run (Fix VZ (NatS (Var VZ)))
интерпретатор просто зациклится. А остаточное выражение, получившееся в
результате суперкомпиляции, просто показывает проблему в
“дистиллированном” виде.
Действительно, чтобы надеть конструктор S на f, нужно сначала снять тег
N с f. А откуда мы знаем, что этот тег - именно N? Нужно “пощупать” f,
проанализировать его структуру. Для этого нужно вместо f подставить его
определение. И, в процессе редукции, начинает порождаться бесконечная
последовательность выражений
case f of ...
case (case f of ...) of ...
case (case (case f of ...) of ...) of ...
Но в случае остаточного выражения - это очевидно (ну, или стало очевидно после внимательного разглядывания), а на текст исходного интерпретатора сколько ни гляди - ничего подозрительного не заметишь.
Ведь fix в исходном интерпретаторе реализован простым и “естественным”
путём. В чём состоит главное свойство конструкции fix(\v -> e)? В том, что
fix (\v -> e) = (\v -> e)(fix (\v -> e))
Стало быть, вычисление
eval (Fix v body) env
должно давать тот же результат, что и вычисление
eval (App (Lam v body) (Fix v body)) env
Так можно было в интерпретаторе и написать. Но, чтобы сделать графы конфигураций более компактными (тем самым, облегчив жизнь и суперкомпилятору, и себе), я немного подоптимизировал интерпретатор λ-выражений вручную: определил вспомогательную функцию
evalFix = \v body env -> eval (App (Lam v body) (Fix v body)) env;
и сделал несколько шагов редукции в правой части вручную. Получилось такое определение функции evalFix:
evalFix = \v body env -> eval body (Bind v (evalFix v body env) env);
В результате этого, интерпретатор стал удовлетворять “принципу композиционности” (the principle of compositionality). Слово-то какое красивое: “композиционность”! Звучит - как музыка. А означает, что некую штуковину мы разбираем, познаём по-отдельности смысл каждой из её частей, а потом синтезируем смысл всей штуковины в целом из смысла её частей.
Применительно к интерпретатору, это означает, что он должен разломать
каждую конструкцию на части, и свести её вычисление к вычислению её
отдельных частей. Определение смысла eval (Fix v body) env через смысл
eval (App (Lam v body) (Fix v body)) env
принципу “композиционности” не удовлетворяет, поскольку тут происходит
не объяснение целого на основе его частей, а объяснение выражения
eval (Fix v body) env через ещё ещё более “навороченное” выражение
(внутри которого, кстати, снова появляется само же выражение
eval (Fix v body) env).
Вообще-то суперкомпилятор умеет справляться и с “некомпозиционными”
определениями функций и превращать их в “композиционные” (или хотя бы в
“более композиционные”). Но из-за “некомпозиционности” граф конфигураций
раздувается, его потом труднее изучать. Вот я и решил немного помочь
суперкомпилятору (и себе).
Всё это я говорю, чтобы объяснить, что та реализация конструкции fix,
которая описана в послании
выглядит как вполне “естественная”, и получена на основе (с виду) “простых” и “естественных” рассуждений. И, наверное, мало кто из читателей послания заметил в этом определении какой-то подвох. А в результате - получилась какая-то откровенная гадость…
А вот при использовании комбинаторов, fix реализуется “естественным”
путём, и проблема не возникает. Ибо она возникает из-за манипуляций
с тегами, а при использовании комбинаторов теги не нужны…
Тут возник естественный вопрос: а можно ли исправить интерпретатор
первого порядка так, чтобы он выдавал для конструкции fix что-то
соответствующее здравому смыслу? Я призадумался. Ответ сразу был
неочевиден… А Новый Год был уже на носу! Что было делать? Поэтому я
поступил так: вымарал из послания все примеры на суперкомпиляцию
конструкции fix и отправился пить шампанское. Расчёт был на то, что и
читатели тоже уже приготовились пить шампанское, и будут не в состоянии
заметить, что с реализацией fix-а в интерпретаторе что-то “не того” (или
“того”?).
Встретив и проводив, я вернулся к изучению вопроса. :-)
Начал снова перечитывать интерпретатор. И пришёл к выводу, что он
написан не совсем “честно”. Раз сказано, что интерпретатор должен быть
“первого порядка”, значит, не только исходная программа должна быть
задана в виде константы первого порядка, но и сам интерпретатор должен
быть написан на языке первого порядка! А между тем, в среде env у меня
использовались функции (для того, чтобы изображать “замыкания”, т.е.
“задержанные вычисления”). Неправильно! Замыкания, для чистоты
эксперимента, нужно тоже представлять в виде констант первого порядка.
В результате у меня получился вариант интерпретатора, представленный в задании Lambda: first-order syntax (FOCL).
Первым делом я заменил определение универсального типа данных
data Val = Error | N Nat | F (Val -> Val);
на определение “первого порядка”
data Val = Error | N Nat | C VarName Exp Env;
и “подкрутил” реализацию вычисления App и Lam. Потом снова попробовал
просуперкомпилировать выражение
run (Fix VZ (NatS (Var VZ)))
Получилось такое остаточное выражение:
(letrec f=case f of { Error -> Error;
C v e r -> Error;
N n -> (N (S n));
} in f)
В принципе, та же самая “проблема тегов” снова воспроизвелась… Слабая надежда на чудо была, но она не оправдалась!
Как же сделать так, чтобы генерировался letrec, которому не надо было бы
“щупать” теги? Ведь без тегов тоже обойтись нельзя? Функция eval exp env
ведь заранее не знает, что получится в результате вычисления выражения
exp: ошибка, число или функция. Значит, тип результата надо как-то
помечать. Возникает, вроде бы, неразрешимая дилемма… Мучился я
мучился, и вдруг вспомнил, что одно из решений проблемы было описано в
статье:
Там, правда, была немного другая проблема: частичный вычислитель начинает обрабатывать выражение, а заранее не знает, какое оно получится: “статическое” или “динамическое”. И из-за этого, опять же, неизвестно, какого типа получится результат: “статического” или “динамического”. Но язык реализации частичного вычисления - ленивый. Вот Mogensen и предложил решение: а давайте пытаться вычислить выражение сразу двумя способами: предполагая, что оно - статическое, и предполагая, что оно - динамическое. Хоть один из двух вариантов да и сработает. А результат вычисления надо выдавать в виде пары, представляющей два результата вычисления: для “статического” случая и для “динамического”.
В случае нашего λ-языка результат может быть либо “ничем”, либо числом, либо замыканием. “Никакой” результат означает, что вычисление “загнулось” из-за несоответствия типов (например, при попытке применить число, а не функцию, к чему-то). Поэтому, можно представлять результат вычисления в виде пары: первый элемент пары будет содержать число (если таковое получилось), а второй элемент пары - замыкание (если таковое получилось).
Полностью это решение приведено в задании на суперкомпиляцию Lambda: first-order syntax (FOCL, pair).
Первым делом определяются вспомогательные типы данных:
data Unit = U;
data Bool = True | False;
Затем определяем тип данных Val, который изображает результат вычисления
λ-выражения:
data Nat = Z | S Nat;
data Closure = C VarName Exp Env;
data Val = Val Nat Closure;
Каждое значение типа Val - это пара из числа и замыкания.
Теперь определяем абстрактный синтаксис λ-выражений:
data VarName = VZ | VS VarName;
data Exp =
NatZ | NatS Exp |
Var VarName | App Exp Exp | Lam VarName Exp |
Fix VarName Exp;
Среды состоят только из значений первого порядка:
data Env = Empty | Bind VarName Val Env;
Для возврата “ошибок” (когда не получилось выдать число или замыкание),
определяем функцию error, которая просто зацикливается:
error = \u -> error U;
Функции getN и getC достают из пары число и замыкание, соответственно.
varNameEq сравнивает имена переменных, а lookup вытаскивает из среды
значение переменной по её имени:
getN = \v -> case v of { Val n c -> n;};
getC = \v -> case v of { Val n c -> c;};
varNameEq = \x y ->
case x of {
VZ -> case y of {VZ -> True; VS y1 -> False;};
VS x1 -> case y of {VZ -> False; VS y1 -> varNameEq x1 y1;};
};
lookup = \v env ->
case env of {
Empty -> Val (error U)(error U);
Bind w val env1 ->
case (varNameEq v w) of {
True -> val;
False -> lookup v env1;
};
};
Торжественный момент: определяем функцию eval через две функции: evalN и
evalC. В этом - вся суть трюка! evalN всегда выдаёт числа, а evalC -
замыкания. Стало быть, отпадает необходимость навешивать теги на
значения. А, как говорил один авторитетный товарищ, “нет тега - нет
проблемы”. При этом, функции evalN и evalC выдают “дно” (вызывая
error U), когда не могут выдать значение “своего” типа.
eval = \e env -> Val (evalN e env) (evalC e env);
evalN = \e env ->
case e of {
NatZ -> Z;
NatS e1 -> S (evalN e1 env);
Var v -> getN(lookup v env);
Lam v body -> error U;
App e1 e2 ->
case evalC e1 env of {
C v body env1 ->
evalN body (Bind v (eval e2 env) env1);};
Fix v body -> evalFixN v body env;
};
evalC = \e env ->
case e of {
NatZ -> error U;
NatS e1 -> error U;
Var v -> getC(lookup v env);
Lam v body -> C v body env;
App e1 e2 ->
case evalC e1 env of {
C v body env1 ->
evalC body (Bind v (eval e2 env) env1);};
Fix v body -> evalFixC v body env;
};
Теперь, естественно, выясняется, что вместо одной функции evalFix
получилось две функции: evalN и evalC. Каждая из них ищет неподвижную
точку “своего” типа. Поэтому им не надо снимать и надевать теги. А в
этом-то и была проблема!
evalFixN = \v body env ->
evalN body (Bind v (Val (evalFixN v body env) (error U)) env);
evalFixC = \v body env ->
evalC body (Bind v (Val (error U) (evalFixC v body env)) env);
run = \e -> eval e Empty;
И вот теперь, наконец, попытаемся просуперкомпилировать выражение
run (Fix VZ (NatS (Var VZ)))
Получается такой результат:
(Val (letrec f=(S f) in f) (letrec g=g in g))
Ура! Наконец, получился осмысленный результат! Это хорошо… Но только если забыть о том, что при использовании комбинаторов хороший результат получился сразу же и без “вставаний на уши”. :-)
В заключение уместно отметить, что данный вариант интерпретатора написан
на том варианте HLL (входного языка суперкомпилятора HOSC), который
существует в момент написания данного послания. А в данный момент в HLL
наборы образцов в case-выражениях должны быть “исчерпывающими”: сколько
разных конструкторов имеется в типе данных, столько и должно быть
перечислено в case-выражении. Из-за этого и пришлось вставить в
интерпретатор вызовы функции error U. Можно разрешить опускать часть
конструкторов в case-выражениях, и считать, что при возникновении
ситуации, не предусмотренной в case-выражении, возникает “ошибка”
(приводящая к аварийной остановке программы). Тогда часть ветвей в
интерпретаторе можно будет просто опустить. Он от этого станет поменьше,
но извращённость и противоестественность его конструкции от этого никуда
не денется.