Разные мысли о метавычислениях, суперкомпиляции, специализации программ. И об их применениях. Желающие приглашаются в соавторы блога.

пятница, 29 января 2010 г.

Превращение неявной рекурсии в явную с помощью суперкомпиляции

В послании

обсуждалась возможность записывать явные рекурсивные определения данных. А нельзя ли вообще без них обойтись?

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

Возникает два интересных вопроса:

  • Можно ли пользоваться во входном языке суперкомпилятора Хоск (HOSC) теми приёмами, которые были придуманы для "чистого, классического" лямбда-исчисления?
  • Можно ли использовать суперкомпиляцию для преобразования неявной рекурсии (закодированной с помощью "оператора неподвижной точки") в явную рекурсию?

Начнём с первой проблемы.

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

omega = F (\x -> apply x x);

apply = \x -> case x of { F f -> f; };

и получаем такую приятную остаточную программу

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 - вроде как бы даже и не "функция", а "структура данных" (раз у неё нет аргумента). Молодец, Хоск! Нетривиальное преобразование сумел выполнить.

Однако, нужно заметить, что fix мы закодировали без использования рекурсии только, так сказать, из "спортивного интереса", чтобы посмотреть, испугается ли такого задания Хоск или нет. Не испугался! А на самом деле, Хиндли-Милнер как это ни странно, разрешает нам определить 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

Таким образом, мы видим, что Хоск в очередной раз справился с преобразованием неявной рекурсии (через редукцию) в явное рекурсивное определение (удалив при этом много промежуточных шагов редукции).

четверг, 28 января 2010 г.

Тёмные углы суперкомпилятора HOSC: неполные case-выражения и рекурсивные определения данных

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

Речь будет идти о двух вопросах:

  • Неполные case-выражения (содержащие не все конструкторы из типа данных).
  • Рекурсивные определения, в правой части которых не лямбда-абстракция, а что-то другое.

Неполные case-выражения

Раньше в хосковском HLL было такое ограничение. Если определение типа данных определяло некоторый набор конструкторов C1, C2, ..., Cn, то любое case-выражение, использующее один из этих конструкторов должно было предусматривать ветви для каждого из этих конструкторов:

case e0 of {C1 ... -> e1; C2 ... -> e2; ... Cn -> en; }

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

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

data List a = Nil | Cons a (List a);

data Nat = Z | S Nat;

А теперь попробуем определить функции tail (взятие "хвоста" списка) и pred (вычитание единицы из числа):

tail = \xs -> case xs { Nil -> error; Cons x xs1 -> xs1; };

pred = \n -> case n { Z -> error; S n1 -> n1; };

Если требовать, что для случаев Nil и Z должны присутствовать ветви, то надо как-то указать, что выбор этих ветвей является "ошибкой". Нужно было что-то написать для этих случаев в качестве результата работы функции. Ну, я и написал error. Пока не будем вдаваться в вопрос, что именно означает этот error, но плохо уже то, что в программе пришлось вообще что-то писать для случаев, которых "не должно быть".

Поэтому, теперь в HLL, входном языке Хоска, разрешается часть конструкторов в case-выражениях опускать. Т.е., функции tail и pred теперь можно определить так:

tail = \xs -> case xs { Cons x xs1 -> xs1; };

pred = \n -> case n { S n1 -> n1; };

Мелочь, конечно, но жизнь в некоторых случаях облегчает.

А что получается при попытке вычислить tail Nil или pred Z ? Получается "возникновение ошибки": выполнение программы в этом случае "аварийно завершается".

Выражение "часть конструкторов можно опустить" можно понимать и в том смысле, что можно опустить и вообще все конструкторы, т.е. писать case-выражения вида

case e0 of {}

которые исполняются так. Пробуем вычислить e0. Поскольку семантика языка HLL - "ленивая", в результате получается нечто, приведенное к "слабой головной нормальной форме". В данном случае это означает, что на верхний уровень вылезает некий конструктор C. (А лямбда-абстракция вида \x -> e получиться не может из-за ограничений статической типизации). После чего делается попытка выбрать в case-выражении ту ветвь, которая соответствует конструктору C. А такой ветви и нет (поскольку нет ни одной). И это приводит к аварийной остановке программы. Но это только в том случае, если попытка вычисления e0 была успешной. А если вычисление e0 завершилось аварийно, или вообще не остановилось, то до попытки выбора ветви дело не доходит. Впрочем, для гарантированной генерации ошибки, в качестве e0 всегда можно написать нечто всегда завершающееся, например Z, тогда вычисление case Z of {} заведомо аварийно завершается.

В качестве реального примера, когда применение неполных case-выражений позволяет уменьшить размер программы и делает программу более понятной, можно сравнить два варианта интерпретатора лямбда-выражений

В первом варианте, обрабатываемые данные представлены таким типом данных:

data Val = Error | N Nat | C VarName Exp Env;

При этом ошибки, связанные с несоответствием типов, явно представлены с помощью конструктора Error, и все случаи возможного несоответствия типов выписаны в явном виде. Например, при вычислении аппликации App e1 e2, результат вычисления e1 должен быть функцией (точнее, замыканием), но не числом и не ошибкой:

    App e1 e2 ->

      case eval e1 env of {

        Error -> Error;

        N n -> Error;

        C v body env1 ->

          eval body (Bind v (eval e2 env) env1);

      };

А во втором варианте данные предствлены так:

data Val = N Nat | C VarName Exp Env;

Конструктор Error исчез, поскольку для обработки ошибок используется механизм, встроенный в HLL. Сократился и размер интерпретатора, поскольку неполные case-выражения позволяют не выписывать все "нехорошие" ситуации в явном виде. В частности, обработка App e1 e2 теперь принимает такой вид:

    App e1 e2 ->

      case eval e1 env of {

        C v body env1 ->

          eval body (Bind v (eval e2 env) env1);

      };

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

run (Fix VZ (NatS (Var VZ)))

даёт для первой версии интерпретатора

letrec f=case f of { C r15 r13 x20 -> Error; Error -> Error; N y12 -> N (S y12); } in f

а для второй версии

letrec f=case f of { N y13 -> N (S y13); } in f

Справедливости следует отметить, что суперкомпиляторы, имеющие дело с динамически типизированными языками, например SPSC и SPC4,

изначально умеют работать с неполными case-выражениями (представленными в других обличьях). Просто из-за того, что при отсутствии статической типизации и объявлений типов данных, непонятно, что могло бы обозначать такое понятие, как "полный список конструкторов"?

Рекурсивные определения данных

До недавнего времени в HLL, входном языке Хоска, рекурсивные определения можно было писать только для функций, но не для данных. Т.е., рекурсивные определения, записанные в программе после where, дожны были иметь такой вид

f = \x -> e;

Однако, как показывает следующий пример

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

data Xs = X Xs;

data Unit = U;


(f U)

where

-- a = X a;

f = \u -> X (f u);

получалась остаточная программа

data Xs = X Xs; data Unit = U ; letrec g=(X g) in g

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

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

Суперкомпилируем программу

data Input = A Input | B Input;

data Unit = U;


p U
where

-- p = A q;

-- q = B p;


p = \u -> A (q u);

q = \u -> B (p u);

и получаем остаточную программу:

data Input = A Input | B Input; data Unit = U ; letrec f= A (B f) in f

Теперь видно, что p U генерирует бесконечный поток из A и B вида A (B (A (B ... ))).

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

p = A q;

q = B p;

И Хоск теперь это разрешает. Что хорошо, поскольку бесконечные структуры данных хорошо подходят для моделирования систем, которые способны работать бесконечно долго (не выдавая никакого "окончательного" результата). Пример такой системы - Microsoft Windows. :-)

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

В этом примере определяются две функции enqueue и repeat.

data List a = Nil | Cons a (List a);

data Bool = True | False;


repeat (Cons True (Cons False Nil))


where


repeat = \xs -> case xs of {

   Nil -> Nil;

   Cons x xs1 -> Cons x (repeat (enqueue x xs1));

};


enqueue = \a xs -> case xs of {

   Nil -> Cons a Nil;

   Cons x xs1 -> Cons x (enqueue a xs1);

};

enqueue a xs вставляет a в конец списка xs, а repeat xs строит бесконечный список в котором повторяются элементы списка xs. Например, repeat [A, B, C] порождает [A, B , C, A, B, C, ...]. При этом, repeat реализована таким "топорным" способом: она всё время "вращает" xs, т.е. берёт из xs первый элемент, выдаёт его и переставляет в конец списка xs (с помощью функции enqueue). В результате суперкомпиляции выражения

repeat (Cons True (Cons False Nil))

получается такое выражение:

Cons True (Cons False (letrec f=(Cons True (Cons False f)) in f))

Видно, что суперкомпилятор "прокрутил" список [True, False] один раз и сообразил, что можно построить цикл в графе конфигураций. А о том, что то же самое можно было бы записать в более краткой форме

letrec f=(Cons True (Cons False f)) in f

Хоск не догадался. "Мозгов" ему не хватило... Но и так результат неплохой.

среда, 6 января 2010 г.

Реализация недетерминизма в проблемно-ориентированных языках через абстрактный синтаксис высшего порядка

В посланиях

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

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

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

В некоторых случаях написать программу, формализующую некую систему, труда не составляет. Это в тех случаях, когда язык программирования уже содержит в готовом виде те понятия, которые нужны для описания системы. А если нет? Тогда может оказаться, что изготовление такой программы превращается в занудное и трудоёмкое дело.

Вот типичный пример. Моделируемая система является недетерминированной, а её нужно смоделировать с помощью языка программирования, в котором нет никакого недетерминизма: какую программу ни напиши, она оказывается детерминированной. Что же делать? Один из подходов - расширить язык программирования новыми понятиями (реализовав в его рамках некоторый проблемно-ориентированный язык) и писать программу-модель на ПО-языке, предоставляющем систему понятий адекватную решаемой задаче.

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

choice2 e1 e2

которая дожна исполняться следующим образом. При вычислении choice2 e1 e2 следует произвольно выбрать одно из выражений e1 или e2 и вычислить выбранное выражение. И результат этого вычисления должен считаться результатом вычисления всей конструкции choice2 e1 e2.

Как и в предыдущих посланиях, мы реализуем "недетерминированное" лямбда-исчисление как расширение языка HLL. HLL - это подмножество языка Haskell, являющееся входным языком суперкомпилятора HOSC.

Итак, нам нужно реализовать недетерминизм, а любая программа на языке HLL - детерминированная. Откуда же может взяться недетерминизм? Ответ прост: из внешнего мира. Используем следующий тривиальный приём: будем считать, что при запуске программы ей на вход подаётся бесконечная последовательность, которая говорит, какое из выражений в choice2 e1 e2 нужно выбрать: левое или правое. Будем считать, что эта последовательность имеет следующий тип:

data Choice = L Choice | R Choice;

А когда возникает необходимость вычислить choice2 e1 e2, программа должна заглянуть в эту последовательность и посмотреть на верхний конструктор. Если вверху конструктор L (left), нужно выбрать левое выражение, а если конструктор R (right) - то правое.

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

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

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

Начнём мы с реализации "детерминированного", статически-типизированного лямбда-исчисления, а потом добавим к нему недетерминизм.

В послании

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

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

А именно, в качестве "переменных" реализуемого ПО-языка можно использовать прямо переменные того языка, поверх которого реализуется ПО-язык. В литературе этот трюк известен под именем "использование абстрактного синтаксиса высшего порядка". Суть дела проще всего объяснить на конкретном примере, посмотрев следующее задание на суперкомпиляцию Lambda: higher-order syntax 2.

Будем считать, что в нашем лямбда-исчислении имеются булевские значения и натуральные числа, которые определяются так

data Bool = True | False;

data Nat = Z | S Nat;

После чего определяются комбинаторы var (переменная), lam (лямбда-абстракция), app (аппликация) и cst (константа). Основная идея заключается в том, что переменную x можно представлять прямо в виде var x, а лямбда-абстракцию \x -> e в виде lam (\x -> e). При этом x - это, одновременно, и переменная реализуемого языка, и переменная языка реализации (т.е. HLL). Тогда, например, выражение (\x -> x) True изображается следующим образом: app (lam (\x -> var x)) (cst True).

А теперь посмотрим, как определяются комбинаторы:

var = \x -> x;

lam = \f -> f;

app = \e1 e2 -> e1 e2;

cst = \a -> a

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

Для полноты картины определим ещё fix, if и прибавление единицы к числу:

fix = \f -> f (fix f);


if = \e0 e1 e2 ->

  case e0 of {

    True -> e1;

    False -> e2;

  };


natS = \n -> S n;

Ну, ежели по-честному fix определять, то его следовало бы определить как

fix = \f -> app (lam f) (fix f)

но, выполнив пару редукций вручную, убеждаемся, что app (lam f) (fix f) быстро превращается в f (fix f). Поэтому я и не удержался от искушения, и подоптимизировал определение fix.

Теперь пробуем просуперкомпилировать несколько выражений. Получается:

cst (S (S Z)) --> (S (S Z))

app (lam (\x -> var x)) (cst True) --> True

lam (\x -> if x False True) --> (\r-> case r of { True -> False; False -> True; })

fix (\x -> natS x) --> (letrec f=(S f) in f)

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

Переопределим комбинаторы так, чтобы они "потихоньку" передавали друг-другу дополнительный параметр типа Choice, содержащий последовательность выборов.

data Choice = L Choice | R Choice;

Тогда комбинатор choice2 можно будет реализовать так:

choice2 = \e1 e2 c ->

  case c of {

    L c1 -> e1;

    R c2 -> e2;

  };

Есть, правда, одна проблема: в некоторых случаях вычисление "разветвляется": нужно вычислить два разных выражения e1 и e2. При этом, поскольку язык "ленивый", e1 и e2 могут вычисляться не сразу, а постепенно по мере надобности. Немного e1 повычисляли, а потом повычисляли e2, и т.д. Хорошо было бы снабдить e1 и e2 независимыми последовательностями выборов: передать в e1 и e2 две последовательности выборов - и не заботиться о взаимодействии этих двух вычислений.

Мы можем добиться возможности "разветвлять" последовательности выборов переопределив тип данных Choice следующим образом:

data Choice = L Choice | R Choice | D Choice Choice;

Теперь L - "левый" выбор, R - "правый" выбор, а D - "разделение" последовательности на две независимые последовательности.

После этого мы переписываем комбинаторы так, как это сделано в задании на суперкомпиляцию Lambda: non-determinism (direct). И вот что получается.

Каждый из комбинаторов получает дополнительный параметр c. Комбинаторы cst и natZ его просто игнорируют:

cst = \a c -> a;

natZ = \c -> Z;

Комбинатор natS должен вычислить свой аргумент и надеть на результат конструктор S. Он так и делает, но передаёт c своему аргументу:

natS = \e c -> S (e c);

var x c передаёт c в x, поскольку значением переменной является выражение, которое нуждается в аргументе c.

var = \x c -> x c;

lam f с просто отбрасывает c (как и cst a c):

lam = \f c -> f;

Самые интересные случаи - app e1 e2 с и choice2 e1 e2. В случае с app e1 e2 c проблема в том, что сначала нужно вычислить e1, а потом применить то, что получится к e2. При этом мы не знаем, какую часть последовательности выборов "съест" e1. Поэтому, мы требуем, чтобы последовательность выборов c разветвилась на c1 и c2:

app = \e1 e2 c ->

  case c of {

    D c1 c2 -> (e1 c1) e2 c2;

  };

c1 используется при вычислении e1, а e2 - при применении результата вычисления e1 к e2.

Ну, а определение choice2 e1 e2 c говорит само за себя:

choice2 = \e1 e2 c ->

  case c of {

    L c1 -> e1 c1;

    R c2 -> e2 c2;

  };

Есть, правда, в определениях app и choice2 одна тонкость: используются case-выражения, в которых набор конструкторов - неполный. До какого-то момента так делать не разрешалось, но недавно это ограничение в HOSC было снято. Семантика неполных case-выражений такая. Если в процессе исполнения программы требуется выполнить редукцию выражения вида

case C ... of { ... }

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

Поэтому, если в app попадает c, у которого на верхнем уровне не D, то программа просто "грохается". А если в choice2 попадает c, у которого на верхнем уровне не L и не R, то и тогда программа аварийно завершается.

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

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

В определении комбинатора if используется тот же приём, что и в реализации app: разделение последовательности выборов:

if = \e0 e1 e2 c ->

  case c of {

    D c1 c2 ->

      case e0 c1 of {

        True -> e1 c2;

        False -> e2 c2;

    };

  };

И, наконец, определение комбинатора fix:

//fix = \f c -> app (lam f) (fix f) c;

fix = \f c -> f (fix f) c;

Выражение f (fix f) c является слегка оптимизированной версией выражения app (lam f) (fix f) c, учитывающей, что lam f просто игнорирует c.

Ну вот, а теперь попробуем посуперкомпилировать некоторые лямбда-выражения и посмотрим, что получается.

(choice2 (cst True) (cst False)) c -->

    case c of { L c1 -> True; R c2 -> False; }

(choice2 (cst Z) (choice2 (cst (S Z)) (cst (S(S Z))))) c -->

    case c of { L c1 -> Z; R c2 -> case c2 of { L c3 -> (S Z); R c4 -> (S (S Z)); }; }

(app (lam (\x -> if (var x) (cst False) (cst True))) (cst True)) c -->

    case c of { D c1 c2 -> case c2 of { D c3 c4 -> False; }; }

(fix (\x -> choice2 natZ (natS (var x)))) c -->

    (letrec f=(\c1 ->

       case c1 of {

         L c2 -> Z;

         R c3 -> S (f c3); })

     in (f c))

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

choice2 natZ (natS (

  choice2 natZ (natS (

    choice2 natZ (natS ( ... )) )) ))

Происходит выбор между Z и S(x), где x - "недетерминированное" натуральное число. Вот и получается, что может породиться любое натуральное число. Красота!

понедельник, 4 января 2010 г.

Специализация интерпретаторов и проблема устранения тегов

В посланиях

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

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

Общий вывод был такой:

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

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

Итак, в послании

был рассмотрен интерпретатор первого порядка, для бестипового лямбда-исчисления. При этом лямбда-исчисление было "нечистым": в лямбда-термах можно было использовать натуральные числа и записывать рекурсивные определения с помощью конструкции fix f-> e, эквивалентной letrec f = e in f .

Однако же, не приводилось ни одного примера того, что получается при попытке просуперкомпилировать выражения, содержащие fix. И неспроста, ибо при суперкомпиляции получаются явные гадости, и обсуждение этих интересных и поучительных гадостей отвлекло бы нас от главной темы послания. Но теперь наступил подходящий момент, чтобы выложить все карты на стол и узнать горькую правду. Раскрываем уже известное нам задание на суперкомпиляцию Lambda: first-order syntax 2 и пробуем просуперкомпилировать выражение

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 u3 -> Error; N p2 -> (N (S p2)); } in f)

Когда я увидел это в первый раз, то я некоторое время хлопал глазами, а потом мне прямо-таки стало нехорошо... Что бы такой результат мог означать? Ну хорошо, есть в нём дурацкие манипуляции с тегами. Вместо того, чтобы просто надеть на число n конструктор S, мы сначала снимаем с n тег N, потом надеваем S, а потом снова надеваем N. Ну, ещё и проверять приходится, что число - это число. Ладно! Это всё - зло понятное и необходимое (для интерпретатора первого порядка). Смущает другое! В данном случае, letrec - это форма записи уравнения

f=case f of { Error -> Error; F u3 -> Error; N p2 -> (N (S p2)); }

и решение этого уравнения является "смыслом" конструкции. Есть ли у этого уравнения решение? О да! Например, подставим в правую часть в качестве значения f бесконечное выражение N (S(S(...))) и выполним шаг редукции

case N(S(S(...))) of { Error -> Error; F u3 -> Error; N p2 -> (N (S p2)); }

N(S(S(S(...))))

И в результате получилось то же самое выражение N(S(S(...))) ! Оно, конечно, один конструктор S внутри добавился, но раз выражение S(S(...)) - бесконечное, от этого ничего не изменилось. Стало быть, N(S(S(...))) является решением уравнения. Чего и следовало ожидать. Хоть и выглядит этот letrec диковато, но решение-то правильное даёт! А что получится, если мы попробуем подставить f = Error ? И Error подходит в качестве решения!

case f of { Error -> Error; F u3 -> Error; N p2 -> (N (S p2)); }

Error

А если попробовать f = F (\x -> x) ? Получается

case F (\x -> x) of { Error -> Error; F u3 -> Error; N p2 -> (N (S p2)); }

Error

Ну, слава Богу, хоть F (\x -> x) в качестве решения не годится, поскольку в результате редукции получается что-то другое (Error).

Итак, подозрение, что в конструкции

(letrec f=case f of { Error -> Error; F u3 -> Error; N p2 -> (N (S p2)); } in f)

таится какая-то гнильца, вполне оправдывается. При этом, патология не в том, что эта конструкция не имеет смысла, а в том, что этих смыслов слишком много: один смысл N(S(S(...))), а другой - Error. А какой же из них является "истинным"? Как говорят в кино, "в конце должен остаться только один" (ну, или "Росинант не вынесет двоих).

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

Если встать на математическую точку, то конструкция

(letrec f=case f of { Error -> Error; F u3 -> Error; N p2 -> (N (S p2)); } 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 1.

Первым делом я заменил определение универсального типа данных

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 { C r1 y1 v1 -> Error; Error -> Error; N w6 -> (N (S w6)); } in f)

В принципе, та же самая "проблема тегов" снова воспроизвелась... Слабая надежда на чудо была, но она не оправдалась!

Как сделать так, чтобы генерировался letrec, которому не надо было бы "щупать" теги? Ведь без тегов тоже обойтись нельзя? Функция eval exp env ведь заранее не знает, что получится в результате вычисления выражения exp: ошибка, число или функция. Значит, тип результата надо как-то помечать. Возникает, вроде бы, неразрешимая дилемма... Мучился я мучился, и вдруг вспомнил, что одно из решений проблемы было описано в статье:

Mogensen, T. Æ. 1995. Self-applicable online partial evaluation of the pure lambda calculus. In Proceedings of the 1995 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (La Jolla, California, United States, June 21 - 23, 1995). PEPM '95. ACM, New York, NY, 39-44. DOI=http://doi.acm.org/10.1145/215465.215469

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

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

Полностью это решение приведено в задании на суперкомпиляцию Lambda: first-order syntax 1 (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-выражении, возникает "ошибка" (приводящая к аварийной остановке программы). Тогда часть ветвей в интерпретаторе можно будет просто опустить. Он от этого станет поменьше, но извращённость и противоестественность его конструкции от этого никуда не денется.

Постоянные читатели