Метавычисления и специализация программ

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

понедельник, 28 марта 2011 г.

Перестройка сверху с откатами (rollbacks)

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

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

среда, 16 марта 2011 г.

Крупношаговая суперкомпиляция (big-step supercompilation)

По поводу нынешнего послания вспомнился мне один эпизод из моего детства. Это было в те времена, когда по радио часто исполняли зажигательную песню “Русский с китайцем - братья навек!”.

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

Меня эта картинка заинтересовала, и я спросил взрослых, что это значит? И мне объяснили, что строить светлое будущее - дело неспешное и утомительное. Поэтому, Председатель Мао, вождь китайского народа, решил ускорить процесс, и придумал для этого теорию “большого скачка”. Поэтому китаец и совершает прыжок над пропастью, на одной стороне которой находится капитализм, а на другой - коммунизм. Тем самым реализуя лозунг, выдвинутый Председателем Мао: “Три года упорного труда - десять тысяч лет счастья”.

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

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

И вот, мы уже живём в другую эпоху. Смеяться над китайцами мы уже перестали... Не достигнув счастья за три года упорного труда, они почему-то после этого не перестали упорно трудиться. И теперь скорее уже у них есть основания над нами смеяться. “А хорошо смеётся тот, кто смеётся последним...”

Тут уместно спросить: “А какое отношение имеет Китай к суперкомпиляции?” И какое отношение имеет суперкомпиляция к теории “большого скачка” и к теории “малых дел”? По поводу первого могу сказать, что мне известен по крайней мере один аспирант, которого прислали из Китая для того, чтобы он позанимался в России суперкомпиляцией. Может быть, чтобы выяснить, стоит ли этим делом вообще заниматься. А аспирантура - это как раз три года. Так что, “три года упорного труда - …”.

С другой стороны, как выясняется, в области операционной семантики языков программирования как раз существует два подхода: “мелкошаговая семантика” (small-step semantics) и “крупношаговая семантика” (big-step semantics). В некоторых случаях они эквивалентны (в отличие от сферы политики и экономики). А в основе любого суперкомпилятора лежит та или иная версия операционной семантики.

Анатомия суперкомпиляции

Суперкомпиляция - это довольно абстрактная идея. Чтобы дойти от суперкомпиляции как идеи до конкретного суперкомпилятора требуется пройти через следующие этапы.

  • Выбираем язык программирования.
  • Выбираем операционную семантику этого языка.
  • Придумываем язык, на котором описываются конфигурации (множества состояний). Реализуем набор операций над конфигурациями: проверку вложения и (аппроксимации) для объединения.
  • Придумываем прогонку как обобщение операционной семантики.
  • Вводим правила обобщения, разрешающие заменять конфигурации на более общие и правила зацикливания.
  • Получается отношение суперкомпиляции, описывающее отношение между исходными и остаточными программами.
  • Добавляем эвристики, целями которых обычно является
    • Устранение недетерминизма (уменьшение числа порождаемых остаточных программ), вплоть до получения детерминированной суперкомпиляции.
    • Формализация целей суперкомпиляции (какие остаточные программы считаются “хорошими”, а какие - “плохими”).

Вывод:

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

Семантика: мелкошаговая vs. крупношаговая

Есть два подхода к определению операционной семантики языка: семантика малых шагов (small-step) и семантика большого шага (big-step). Или, по-русски, “мелкошаговая” и “крупношаговая”.

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

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

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

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

Пример: CEK-машина

Для сравнения особенностей мелкошаговой и крупношаговой семантики, рассмотрим следующий пример. В статье

Olivier Danvy and Kevin Millikin. 2008. On the equivalence between small-step and big-step abstract machines: a simple application of lightweight fusion. Inf. Process. Lett. 106, 3 (April 2008), 100-109. PDF DOI=10.1016/j.ipl.2007.10.010 http://dx.doi.org/10.1016/j.ipl.2007.10.010

описаны две подхода к определению операционной семантики CEK машины. CEK-машина реализует приведение λ-термов к слабой головной нормальной форме с использованием редукции слева направо в аппликативном порядке. Переменные изображаются индексами де Брюйна (de Bruijn indices). (Кто не верит, что de Bruijn - это “де Брюйн”, может проверить, пошарив по именам авторов книг. Например: http://www.ozon.ru/context/detail/id/2367530/ .)

В статье семантика виртуальных машин запрограммирована на языке Standard ML, мы же перепишем её на языке HLL, являющемся входным языком суперкомпилятора HOSC (и представляющем собой подмножество языка Haskell).

Итак, сначала определяем понятие λ-терма:

data Nat = Z | S Nat;
data Term = Var Nat | Lam Term | App Term Term;

Понадобилось определить понятие натурального числа, поскольку натуральные числа используются в качестве индексов де Брюйна.

Будем считать, что результатом вычисления терма (если это вычисление завершается) является представление его слабой головной нормальной формы в виде замыкания, имеющего вид Clo t e, где t - λ-терм, а e - среда, приписывающая значения свободным переменным терма t. Среда при этом представляет собой список из значений переменных. Заметим, что имена переменных хранить в среде не требуется, поскольку индексы де Брюйна прямо задают позиции для значений переменных в среде.

На языке HLL это описывается так:

data List a = Nil | Cons a (List a);
data Val = Clo Term (List Val);

Извлечение значения переменной с индексом i из среды e может быть выполнено с помощью функции lookup:

lookup = \i env ->
 case env of {
   Cons n env1 ->
     case i of {
       Z -> n;
       S i1 -> lookup i1 env1;
     };
 };

Мелкошаговая семантика CEK-машины

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

data RC = RC0
       | RC1 RC Term (List Val)
       | RC2 Val RC;

Мелкошаговая семантика CEK-машины определяется через понятие текущего состояния:

data Conf = Eval Term (List Val) RC
         | Apply RC Val;

data State = Final Val | Inter Conf;

Работа CEK-машины распадается на шаги. Действия, предпринимаемые на каждом шаге, зависят от того, какой вид имеет текущее состояние.

  • Final v . В этом случае состояние считается заключительным, а v - окончательным результатом вычисления.
  • Inter conf . В этом случае состояние считается промежуточным, а confизображает текущую конфигурацию виртуальной машины.

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

  • Apply c v . Такая конфигурация означает, что значение v нужно вставить внутрь объемлющего контекста c и продолжить вычисление.
  • Eval t e c . Такая конфигурация означает, что терм t следует вычислить в среде e, а потом вставить результат в контекст c.

Как же вычисляется терм t, входящий в конфигурацию Eval t e c ? Способ вычисления t зависит от того, какой вид он имеет.

  • Var i. Нужно достать из окружения e значение переменной, находящееся в e в i-й позиции. И вставить это значение в контекст c. Значение переменной извлекается из контекста с помощью функции lookup (описанной выше).
  • Lam t0 . Нужно сформировать замыкание Clo t0 e и вставить его в контекст c. Помимо терма t0 замыкание содержит и среду, в которой этот терм должен вычисляться.
  • App t0 t1 . Этот случай - самый интересный. Нужно заняться вычислением терма t0, отложив вычисление терма t1 на будущее. Для этого контекст c заменяется на новый контекст RC1 c t1 e, после чего вычисляется t0, и получается результат v, который вставляется в контекст RC1 c t1 e. А операция вставления v в контекст вида RC1 c t1 e реализована так, что начинается вычисление терма t1 в окружении e, а v запоминается в контексте вида RC2 v c1.

Собрав всё воедино, получаем функцию move, реализующую преобразование текущей конфигурации (незаключительного состояния) в следующее состояние:

move = \conf ->
 case conf of {
   Eval t e c ->
     case t of {
       Var i -> Inter (Apply c (lookup i e));
       Lam t0 -> Inter (Apply c (Clo t0 e));
       App t0 t1 -> Inter (Eval t0 e (RC1 c t1 e));
     };
   Apply c v ->
     case c of {
       RC0 -> Final v;
       RC1 c1 t1 e -> Inter (Eval t1 e (RC2 v c1));
       RC2 v1 c1 ->

         case v1 of {

           Clo t2 e2 -> Inter (Eval t2 (Cons v e2) c1); };
     };
 };

Самое интересное место в этом определении - вставление значения v в контекст вида RC2 v1 c1. Этот контекст означает, что наступил момент применить замыкание v1 к аргументу v. Для этого из замыкания Clo t2 e2 извлекается тело функции t2 и среда e2, к среде e2 добавляется v (аргумент функции), после чего t2 вычисляется в этой среде.

Теперь осталось определить функцию-”погонялу” drive, приводящую виртуальную машину в движение. Эта функция смотрит на текущее состояние. Если это состояние - заключительное, то выдаётся окончательный результат работы. Если состояние - незаключительное, выполняется переход в следующее состояние (с помощью функции move) и процесс продолжается:

drive = \state -> case state of {
  Final v -> v;
  Inter conf -> drive (move conf);
};

И вот, наконец, функция smallStepEval, которая инициализирует и запускает мелкошаговую виртуальную машину:

smallStepEval = \t -> drive (Inter (Eval t Nil RC0));

Крупношаговая семантика CEK-машины

Теперь рассмотрим другой вариант семантики CEK-машины: крупношаговую семантику, реализованную в виде функции bigStepEvaluate:

eval = \t e c ->
 case t of {
   Var i -> apply c (lookup i e);
   Lam t1 -> apply c (Clo t1 e);
   App t0 t1 -> eval t0 e (RC1 c t1 e);
 };

apply = \t v ->
 case t of {
   RC0 -> v;
   RC1 c1 t1 e1 -> eval t1 e1 (RC2 v c1);
   RC2 v1 c1 ->

     case v1 of {

       Clo t2 e2 -> eval t2 (Cons v e2) c1; };
 };

bigStepEvaluate = \t -> eval t Nil RC0;

Мы не будет подробно разбирать, как устроено это определение, поскольку самое сложное в нём - смысл контекстов. А он - тот же самый, что и в случае функции smallStepEval. Самое интересное в том, что теперь процесс вычислений не распадается на отдельные “шаги”. В отличие от smallStepEval, отсутствует и понятие “состояния”, как некоего единого и неделимого значения.

Эквивалентность мелкошаговой и крупношаговой семантики CEK-машины

Возникает естественный вопрос: верно ли, что мелкошаговая и крупношаговая семантики CEK-машины эквивалентны? Технически этот вопрос сводится к тому, эквивалентны ли функции smallStepEval и bigStepEval.

В вышеупомянутой работе [Olivier Danvy and Kevin Millikin, 2008] на этот вопрос даётся положительный ответ. Для этого авторам пришлось проявить остроумие и изобретательность. А именно, в статье эквивалентность smallStepEval и bigStepEval доказывается с помощью трансформационного подхода. А именно, авторами была найдена цепочка из нескольких преобразований, последовательное применение которых постепенно превращает smallStepEval в bigStepEval.

Возникает интересный вопрос: может ли доказательство такого рода быть автоматизировано?

Доказательство эквивалентности smallStepEval и bigStepEval с помощью суперкомпиляции

Оказывается, что эквивалентность smallStepEval и bigStepEval может быть доказана автоматически с помощью следующего метода.

Пусть имееется суперкомпилятор SC. Обозначим через SC[e] остаточную программу, выдаваемую SC для входной программы e. Пусть ≅ обозначает отношение операционной эквивалентности программ, а ≡ - отношение синтаксической эквивалентности программ (т.е., что программы либо текстуально совпадают, либо различаются “несущественно”, например, совпадают с точностью до имён связанных переменных).

Пусть ∀e, eSC[e], т.е. SC строго сохраняет эквивалентность программ.

Метод доказательства. Просуперкомпилируем программы/выражения e1 и e2. Пусть получились программы/выражения SC[e1] и SC[e2], которые синтаксически эквивалентны. Тогда можно утверждать, что e1 и e2 эквивалентны. В символическом виде:

SC[e1] ≡ SC[e2] ⇨ e1e2

Обоснование (почти тавтология). Смысл SC[e1] и SC[e2] одинаков, поскольку это - фактически одна и та же программа. А SC сохраняет семантику программ, т.е. смысл e1 и e2, тот же, что и смысл SC[e1] и SC[e2] соответственно. Значит, смысл e1 совпадает со смыслом e2. В символическом виде:

e1SC[e1] ≡ SC[e2] ≅ e2

У читателя уже, наверное, сводит скулы от скуки, при виде тривиальности и очевидности только что описанного метода доказательства. Ну да, если мы, просуперкомпилировав две разные программы, получаем одно и то же, значит - и исходные программы эквивалентны. Однако, до недавнего времени, этот метод почему-то никому не приходил в голову. Первое применение этого метода описано в статье

Alexei Lisitsa and Matt Webster. Supercompilation for equivalence testing in metamorphic computer viruses detection. First International Workshop on Metacomputation in Russia (META 2008). PDF

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

Позднее, в статье

Ilya Klyuchnikov and Sergei Romanenko. Proving the Equivalence of Higher-Order Terms by Means of Supercompilation. In: Perspectives of Systems Informatics (Proceedings of Seventh International Andrei Ershov Memorial Conference, PSI 2009, Novosibirsk, Russia, June 15-19, 2009). Novosibirsk: A.P. Ershov Institute of Informatics Systems, 2009, pages 150-158. PDF slides PDF DOI

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

Теперь попробуем применить этот метод к функциям smallStepEval и bigStepEval. Суперкомпилируем определения этих функций с помощью суперкомпилятора HOSC (http://code.google.com/p/hosc/). Оказывается, что и в том, и в другом случае получается одна и та же (с точностью до имён связанных переменных) остаточная программа:

data Nat  = Z  | S Nat;
data List a = Nil  | Cons a (List a);
data Term  = Var Nat | Lam Term | App Term Term;
data Val  = Clo Term (List Val);
data RC  = RC0 | RC1 RC Term (List Val) | RC2 Val RC;
data Conf  = Eval Term (List Val) RC | Apply RC Val;
data State  = Final Val | Inter Conf;

(letrec
 f=(\r47->
   (\s47->
     (\t47->
       case  r47  of {
         App w5 x19 -> (((f w5) s47) (RC1 t47 x19 s47));
         Lam p30 ->
           case  t47  of {
             RC0  -> (Clo p30 s47);
             RC1 y21 w12 x21 ->

               (((f w12) x21) (RC2 (Clo p30 s47) y21));
             RC2 t33 r46 -> case  t33  of {

               Clo y4 w17 ->

                 (((f y4) (Cons (Clo p30 s47) w17)) r46); };
           };
         Var s41 ->
           case  t47  of {
             RC0  ->
               (letrec
                 g=(\x48->
                   (\y48->
                     case  x48  of {

                       Cons w39 z27 ->

                         case  y48  of {

                           Z  -> w39;

                           S p10 -> ((g z27) p10); }; }))
               in
                 ((g s47) s41));
             RC1 w45 z10 p22 ->
               (((f z10) p22)
                 (RC2
                   (letrec
                     h=(\z48->
                       (\u48->
                         case  z48  of {

                           Cons t11 v27 ->

                             case  u48  of {

                               Z  -> t11;

                               S t5 -> ((h v27) t5); }; }))
                   in
                     ((h s47) s41))
                   w45));
             RC2 z12 v1 ->
               case  z12  of {
                 Clo v5 w37 ->
                   (((f v5)
                       (Cons
                         (letrec
                           f1=(\v48->
                             (\w48->
                               case  v48  of {
                                 Cons v26 s14 ->

                                   case  w48  of {

                                     Z  -> v26;

                                     S x16 -> ((f1 s14) x16); };
                               }))
                         in
                           ((f1 s47) s41))
                         w37))
                     v1);
               };
           };
       })))
in
 (((f t) Nil) RC0))

Из этого следует, что и исходные определения функций - эквивалентны. “Вживую” этот пример можно посмотреть здесь: CEK machine.

Интересно, что в этом случае доказательство строится полностью автоматически.

Крупношаговая суперкомпиляция

Обязательно ли суперкомпиляция должна основываться на мелкошаговой семантике?

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

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

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

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

Достоинства крупношаговой суперкомпиляции

В статье

И.Г.Ключников. Суперкомпиляция: идеи и методы // Практика функционального программирования. (http://fprog.ru/)

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

2011-04-13. А вот и обещанная ссылка: http://fprog.ru/2011/issue7/.

Достоинства получившегося суперкомпилятора.

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

Что интересно попробовать сделать

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

  • Реализуем некоторый суперкомпилятор на основе мелкошаговой семантике.
  • Суперкомпилируем суперкомпилятор с помощью суперкомпилятора HOSC.
  • Изучаем, что получится. Есть основания ожидать, что получится суперкомпилятор, основанный на крупношаговой операционной семантике.

Заключение

Важно назвать вещи своими именами. После того, как осознана возможность двух подходов (small-step supercompilation и big-step supercompilation), становятся понятно, что различия между ними нужно исследовать. У big-step supercompilation просматривается определённый потенциал, который нужно изучить и извлечь из него пользу.

Послесловие к заключению

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

Если хорошенько подумать, что в природе пока ещё не было ни одного суперкомпилятора, который был бы на 100% основан на мелкошаговой семантике. Все суперкомпиляторы, что называется “сидят на двух стульях” и основывают прогонку на какой-то “адской смеси” мелкошаговой и крупношаговой операционной семантики.

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

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

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

Посему, наступая на горло собственном авторскому тщеславию, предлагаю читателям забыть всё, что я тут понаписал! :-)

вторник, 15 марта 2011 г.

Заметки о суперкомпиляции

Здесь, для удобства, собраны в одном месте ссылки на несколько заметок о суперкомпиляции. Время от времени, этот список будет пополняться (благодаря тому, что в Блоггере у авторов есть возможность редактировать послания задним числом). Как говорится, "прошлое непредсказуемо"!

вторник, 30 ноября 2010 г.

Саймон Пейтон Джонс о Meta 2010 и суперкомпиляции.

Саймон Пейтон Джонс дал интервью русскоязычному журналу "Практика функционального программирования", где среди прочего рассказал о посещении в этом году Второго международного семинара по метавычислениям Meta-2010, проводимого в Переславле-Залесском.


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

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

пятница, 30 апреля 2010 г.

Комбинаторные парсеры. Часть 1

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






Возьмем простой язык L, алфавит которого состоит всего из двух символов - A и B. Рассмотрим следующее подмножество регулярных выражений для этого языка L:

re = a | b | concat re1 re2 | or re1 re2;


  • Слово w соответствует регулярному выражению a, если слово начинает с A, то есть w = A w1.
  • Слово w соответствует регулярному выражению b, если слово начинает с B, то есть w = B w1.
  • Слово w соответствует регулярному выражению (concat re1 re2), если слово w превставимо в виде w = w1 w2 w3, где w1 - соответсвует re1, а w2 - соответсвует re2.
  • Слово w соответствует регулярному выражению (or re1 re2), если оно соответствует либо выражению re1 либо выражению re2.

Для удобства чтения (or re1 re2) можно записывать как (re1|re2), а конкатенацию (concat re1 re2) - как (re1)(re2).

Результат сопоставление слова языка L с регулярным выражение re определяется так: если существует начальная часть слова, удовлетворяющая выражению, то от слова откусывается такая часть и возвращается оставшаяся часть слова; если же никакая начальная не соответствует выражению, то возвращается неудача.


Напишем парсеры и соответствующие комбинаторы для языка L в духе примера из упомянутого послания, но с одним отличием - в том примере алфавит языка и представление слов были жестко связаны вместе:


data Input = Eof | A Input | B Input | C Input;

Мы же разделим понятие алфавит и слова. Конкретный алфавит языка будет представляться конкретным перечислением букв, а слово языка - это список букв.

Получаем что-то в таком духе:


data Symbol = A | B;
data List a = Nil | Cons a (List a);
data Option a = Some a | None;
par1 = concat (or a (concat a b)) (or (concat b b) a);
or = \p1 p2 word -> case p1 word of {
 Some word1 -> Some word1;
 None -> p2 word;
};
concat = \p1 p2 word -> case p1 word of {
 Some word1 -> p2 word1;
 None -> None;
};
a = \word -> case word of {
 Nil -> None;
 Cons sym word1 -> case sym of {
  A -> Some word1;
  B -> None;
 }; 
};
b = \word -> case word of {
 Nil -> None;
 Cons sym word1 -> case sym of {
  A -> None;
  B -> Some word1;
 }; 
};

Что делают функции - понятно:


  • a (парсер) - соответствует регулярному выражению a - откусывает (если можно) от слова символ A и возвращает оставшуюся часть. Если слово пустое или не начинается с A, возвращает неуспех.
  • b (парсер) - аналогично a
  • or (комбинатор парсеров) - берет два парсера p1 и p2 и делает новый парсер, который возвращает результат работы первого парсера, если это успех, а в противном случае возвращает результат второго парсера
  • concat (комбинатор парсеров) - конкатенирует (соединяет) два парсера, - делает новый парсер, который возвращает успех, тогда и только тогда, когда первый парсер завершается успешно и второй парсер, примененный к остатку слова, выплюнутому первым парсером, также завершатся успехом.
  • par1 - парсер, соответствующий регулярному выражению (a|ab)(bb|a)

Попробуем применить парсер par1 к слову ABBA - соответсвует выражению aBB - выражению bb. Ожидается, что результатом работы будет Some w1, где w1 - пустое слово.

Поскольку суперкомпилятор можно применять и в качестве интерпретатора, попросим HOSC вычислить выражение par1 (Cons A (Cons B (Cons B Nil))), - как и ожидалось в результате получается (Some Nil).

Пойдем дальше - применим парсер par1 к слову ABA. AB - соответсвует выражению ab, A - выражению a. Опять ожидаем, что результатом работы будет Some w1, где w1 - пустое слово.

Вычисляем выражение par1 (Cons A (Cons B (Cons A Nil))). Получаем ... None!

Как же так? Дерево вычислений, показанное HOSC'ом помогает найти ответ на вопрос - после некоторого числа шагов вычисление исходного выражения сводится (редуцируется) к вычислению выражения (or (concat b b) a) (Cons B (Cons A Nil)), которое завершается неудачей.


Можно еще отсукомпилировать выражение par1 w для неизвестного слова wПолучается следующий результат:


case  w  of {
  Nil  -> None;
  Cons u10 x11 ->
    case  u10  of {
      A  ->
        case  x11  of {
          Nil  -> None;
          Cons p3 u13 ->
            case  p3  of {
              A  -> (Some u13);
              B  -> case  u13  of { 
                 Nil  -> None; 
                 Cons z10 u8 -> case  z10  of { 
                    A  -> None; 
                    B  -> (Some u8); 
                 }; 
              };
            };
        };
      B  -> None;
    };
}


Видно, что на самом деле мы закодировали регулярное выражение a(a|bb), или (что то же самое) (aa|abb). Как же так получилось?


Дело в том, что парсер (or (a) (concat a b)) никогда не будет откусывать от слова AB - из-за того, что если парсер (concat a b) способен для данного слова выдать что-то наружу, то на это способен и парсер a, а он вызывается в нашей реализации первым - и получается, что наш комбинатор or работает для парсера (or p1 p2) правильно только в случае, если p1 и p2 не могут выдавать успех на одном и том же слове. Или (говоря более научно), когда языки, определяемые парсерами p1 и p2 не пересекаются.

Как же решить возникшую проблему? Как сделать, чтобы результирующий парсер (сконструированный из комбинаторов) пробовал все варианты? В нашем случае мы сделали так, что парсер возвращает ровно одно успешное сопоставление. Одно из решений проблемы -- заставить парсер возвращает не одно единственное сопоставление в случае успеха, а все возможные. Ясно, что тогда усложняется логика работы комбинаторов парсеров -- они должны анализировать все сопоставления парсеров, переданных как аргументы. Таким образом парсер or p1 p2 должен возращать объединение результатов парсеров p1 и p2. А парсер (concat p1 p2) должен к каждому из вариантов сопоставления p1 попробовать применить p2 и тоже объединить результаты. Этот подход изложен в классической статье Филиппа Уодлера "How to Replace Failure by a List of Successes (A method for exception handling, backtracking, and pattern matching in lazy functional languages)".

Но можно пойти и другим путем - можно каждому парсеру в качестве дополнительного аргумента передавать парсер, который будет вызван на следующем шаге сопоставления. Такой подход по духу очень близок стилю программированию в продолжениях (Continuation passing style). Действительно, в нашей первой наивной реализации парсер (or (a) (concat a b)) действовал по принципу "После нас хоть потоп" - возвращал всегда первое сопоставление - его не интересовало, пригоден ли его ответ для обработки следующим парсером в цепочке.

Легко кодируются в таком стиле парсеры для выражений a и b.


a = \next word -> case word of {
  Nil -> None;
  Cons sym word1 -> case sym of {
    A -> next word1;
    B -> None;
  }; 
};


b = \next word -> case word of {
  Nil -> None;
  Cons sym word1 -> case sym of {
    A -> None;
    B -> next word1;
  }; 
};


Дополнительный аргумент next - это следующий парсер. Логика парсера a проста - если слово начинается с A, то на остаток слова натравливается парсер next, в противном случае -- неудача.

Комбинатор or записывается так:


or = \p1 p2 next word -> case p1 next word of {
  Some word1 -> Some word1;
  None -> p2 next word;
};


А комбинатор concat записывается очень изящно:

concat = \p1 p2 next word -> p1 (p2 next) word;


Композиция парсеров представляется в виде композиции функций!


Неожиданно возникает вопрос а как применить парсер к слову? Ведь теперь любой парсер требует своего продолжения! Для этого потребуется специальный парсер return, который разрывает порочный круг из бесконечных продолжений:


return = \w -> Some w;

В итоге для сопоставления выражения (a|ab)(bb|a) со словом ABA получается следующая программа:


data Symbol = A | B;
data List a = Nil | Cons a (List a);
data Option a = Some a | None;
par1 (Cons A (Cons B (Cons A Nil)))
where
par1 = concat (or a (concat a b)) (or (concat b b) a) return;
return = \w -> Some w;
or = \p1 p2 next word -> case p1 next word of {
  Some word1 -> Some word1;
  None -> p2 next word;
};
concat = \p1 p2 next word -> p1 (p2 next) word;
a = \next word -> case word of {
  Nil -> None;
  Cons sym word1 -> case sym of {
    A -> next word1;
    B -> None;
  }; 
};
b = \next word -> case word of {
  Nil -> None;
  Cons sym word1 -> case sym of {
    A -> None;
    B -> next word1;
  }; 
};


Вычисляем это выражение с помощью суперкомпилятора и получаем (Some Nil)! Если посмотреть на трассировку вычислений, то видно, что новый парсер по очереди перебирает все варианты, пока не найдет успешный, - грубо говоря, неявным образом составляются все возможные комбинации парсеров и по очереди применяются ко входному слову. Первая комбинация завершиласть неудачно - пробуется вторая и т.д. Можно еще сказать, что новый комбинатор or как бы выносит разбор вариантов из глубины регулярного выражения наружу. То есть в каком то смысле переписывает регулярное выражение (re1|re2)re3 -> ((re1 re2) | (re1 re3)).

Вычисление par1 (Cons A (Cons B (Cons B Nil))) тоже выдает (Some Nil).


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


(a|ab)(bb|a) -> (a(bb|a))| (ab(bb|a)) -> abb|aa|abbb|aba


И наш парсер по очереди перебирает эти 4 варианта -- то есть в худшем случае он 4 раза перемещается по входному слову туда-сюда. При более сложных выражениях парсер может бегать по входному слову туда-сюда очень много раз. Это особенно проявляется в случаях, когда входное слово не соответствует регулярному выражению, - прежде чем выдать неудачу парсер попробует все варианты.


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

А попробуем сопоставить наше игрушечное регулярное выражение с произвольным словом w, то есть вычислить concat (or a (concat a b)) (or (concat b b) a) return w с помощью суперкомпилятора HOSC. Результат такой:

case  w  of {
  Nil  -> None;
  Cons p40 v20 ->
    case  p40  of {
      A  ->
        case  v20  of {
          Nil  -> None;
          Cons v1 u30 ->
            case  v1  of {
              A  -> (Some u30);
              B  ->
                case  u30  of { 
                  Nil  -> None; 
                  Cons y18 p22 -> case  y18  of { 
                    A  -> (Some p22); 
                    B  -> (Some p22); 
                  }; 
                };
            };
        };
      B  -> None;
    };
}

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

Заключение

Было показано, как с использованием комбинаторного подхода реализуется проблемно-ориентированный язык для работы с подмножеством регулярных выражений. Реализовать этот язык у нас получилось только со второго раза, что является подтверждением того, что хотя работать с комбинаторным DSL легко и приятно, реализовать даже простой DSL не так то уж и тривиально. Оказалось, что суперкомпилятор HOSC способен устранять накладные расходы, вызванные использованием изящного, но требовательного к ресурсам DSL, реализованный через комбинаторы.

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

воскресенье, 14 февраля 2010 г.

Недетерминизм: выбор по надобности или выбор при вызове?

В послании

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

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

choice2 e1 e2 --> e1

choide2 e1 e2 --> e2

Вроде бы, всё ясно и понятно... Однако, есть тут один "подводный камень". Рассмотрим такое недетерминированное выражение:

(\x -> P x x) (choice2 True False)

где P - конструктор, формирующий пару. Каковы возможные результаты вычисления этого выражения? Это зависит от того, в каком порядке выполнять редукцию. Если первый шаг редукции - применение функции (\x -> P x x) к аргументу (choice2 True False), то на первом шаге получается выражение

P (choice2 True False) (choice2 True False)

в результате дальнейшей редукции которого могут получиться 4 разных выражения: P True True, P True False, P False True, P False False.

А если первый шаге редукции - упрощение (choice2 True False), то получается одно из двух выражений

(\x -> P x x) True

(\x -> P x x) False

и дальнейшие вычисления дают только два возможных результата: P True True, P False False.

Когда выбирать: когда нужен результат или при передаче параметра?

Из рассмотренного примера видно, что результат вычисления недетерминированных конструкций может зависеть от порядка вычислений и от моментов, в которые производится выбор между возможностями. Можно затягивать выбор до последней возможности: выбирать только тогда, когда результат, возвращаемый конструкцией выбора реально понадобился. В литературе этот вариант называется "выбором по надобности" (need-time choice). А можно выбирать в тот момент, когда конструкция выбора оказывается аргументом функции. В литературе этот вариант называется "выбором при вызове" (call-time choice).

В послании

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

Это наглядно можно увидеть просуперкомпилировав выражение

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

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

case c of {

  D u z3 ->

    case z3 of {

      D u5 y5 -> (P case u5 of { L t4 -> True; R p4 -> False; }

                    case y5 of { L y8 -> True; R p2 -> False; });

  };}

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

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

Если уж "выбор при вызове", то тогда уж и "вызов по значению"

Но тут сразу же выясняется, что если мы хотим, чтобы выбор происходил до передачи аргумента в тело функции, то это означает, что аргумент функции должен вычисляться до передачи аргумента в тело функции. Другими словами, параметры должны передаваться в тело функции не "по имени" (call by name), а "по значению" (call by value).

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

А теперь предположим, что нам хочется реализовать недетерминированный язык через набор комбинаторов, и при этом комбинаторы нужно писать на "ленивом" языке. Можно ли при этом реализовать "выбор при вызове"? Ведь для этого надо, чтобы параметры передавались "по значению", а в "ленивом" языке параметры передаются "по имени". Оказывается, что можно...

Реализация вызова по значению в ленивом языке через "продолжения"

Вызов параметров по значению можно реализовать в рамках "ленивого" язык, если использовать писать программу "в стиле передачи продолжений" (continuation passing style). А именно, к параметрам каждой функции f нужно добавить дополнительный параметр k (который называется "продолжением"). Если вызов функции f выглядел как f x1 x2 ... xN, то теперь он принимает вид f x1 x2 ... xN k. При этом, в тех местах, где функция возвращала результат a, нужно выдачу результата делать не напрямую, а вызывать k, передав ему результат в качестве аргумента: k a.

В послании

рассматривалась реализация "ленивого" лямбда-исчисления через набор комбинаторов (см. задание на суперкомпиляцию Lambda: higher-order syntax (transparent)):

var = \x -> x;

lam = \f -> f;

app = \e1 e2 -> e1 e2;

cst = \a -> a;

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

Эти комбинаторы настолько тривиальны, что трудно даже понять их смысл! Тавтология - она тавтология и есть. Если мы реализуем ленивый язык с вызовом параметров по имени через ленивый же язык с вызовом параметров по имени, то понятия реализуемого языка тривиально отображаются на язык реализации.

А теперь попробуем сделать так, чтобы аргумент функции сначала вычислялся и только после этого связывался с параметром функции, переписав комбинаторы в стиле с продолжениями (см. задание на суперкомпиляцию Lambda: HOAS, CPS, CBV)!

var = \x k -> k x;

lam = \f k -> k f;

app = \e1 e2 k -> e1 (\f -> e2 (\v -> f v k));

cst = \a k -> k a;

var, lam и cst устроены неинтересно: переменная подсовывает продолжению k своё значение, lam - функцию, а cst - свой аргумент. Весь интерес - в комбинаторе app! Он работает так. Сначала вычисляется e1, и результат этого вычисления подсовывается продолжению (и связывается с переменной f). Затем вычисляется e2, и результат этого вычисления подсовывается продолжению (и связывается с переменной v). После этого вычисляется результат применения f к v и подсовывается продолжению k. Вот и получается, что при вызове функции предварительно вычисляется ей аргумент. В рамках "ленивого" языка реализован вызов параметра по значению.

Самый тонкий вопрос - как определить fix! Определение fix - это некая смесь из определений app и lam:

fix = \e k -> k (fixLoop e);

fixLoop = \e x k -> e(fixLoop e)(\f -> f x k);

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

run = \e -> e (\x -> x);

Для того, чтобы можно было определять функции, что-то делающие с натуральными числами, определим ещё три комбинатора. natZ - вырабатывает ноль, natS сначала вычисляет свой аргумент, а потом прибавляет к тому, что получилось, единицу. natCase реализует разбор случаев: проверяет, является ли нулём её первый аргумент, а затем вызывает второй или третий аргумент.

data Nat = Z | S Nat;

natZ = \k -> k Z;

natS = \e k -> e (\v -> k(S v));

natCase = \e eZ eS k -> e (\v -> case v of {

  Z -> eZ k;

  S n -> eS n k;

  });

Теперь можно определять функции над натуральными числами

data Bool = True | False;

natIsZ = \e -> natCase e (cst True) (\n -> (cst False));
natPred = \e k -> e (\v -> case v of { S v1 -> k v1;});

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

run (fix(\natId -> lam(\x ->

  natCase (var x)

    natZ

    (\x1 -> (natS (app (var natId) (var x1)))))))

Просуперкомпилировав это выражение, получаем остаточную программу

\x k->

   letrec f = \x0 k0 -> case x0 of {

     Z -> k0 Z;

     S x1 -> f x1 (\x2 -> k0 (S x2)); }

   in f x k

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

Реализация "выбора при вызове" через комбинаторы

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

но используем в комбинаторах, реализующих недетерминированный язык стиль с продолжениями. Результат можно увидеть заглянув в задание на суперкомпиляцию Lambda: non-determinism (HOAS, CPS k c, CBV).

Посмотрим, что получается. Сначала определяются типы данных, которые используются в дальнейшем:

data Bool = True | False;

data Choice = L Choice | R Choice;

data Nat = Z | S Nat;

data Pair a b = P a b;

Здесь интересно то, что при реализации выбора по надобности в определении Choice нам понадобились три конструтора: L (левый выбор), R (правый выбор) и D (разделение последовательности выборов на две подпоследовательности). А теперь в определении Choice - только два конструктора: L и R. Это связано с тем, что при реализации языка с передачей параметров по значению и выбором при вызове получается, что последовательность, в которой выполняются вычисления, проста и заранее предсказуема. Поэтому нет и надобности "разветвлять" последовательность выборов: можно аккуратно "протаскивать" одну последовательность через весь процесс вычислений.

Основная идея проста. Пусть у нас есть выражение e. При вычислении этого выражения ему должно подсовываться два дополнительных аргумента: продолжение k и последовательность выборов c. Другими словами, хотим получить значение e - вычисляем e k c. При этом, в отличие от случая детерминированных программ, продолжение k должно принимать не только результат, вырабатываемый выражением e, но ещё и некоторую последовательность выборов c1. Т.е., k должно иметь вид (\v1 c1 -> e1). Откуда же берётся c1? Дело в том, что если выражение e содержит конструкции choice2, то эти конструкции могут потреблять выборы из входной последовательности выборов c. И продолжение должно получить оставшуюся "неизрасходованную" часть последовательности выборов через параметр c1.

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

run = \e с -> e (\v c1 -> v) с;

Эта функция подсовывает выражению e продолжение \v c1 -> v и последовательность выборов c. Продолжение принимает результат, возвращаемый выражением e и выдаёт этот результат. А остаток последовательности выборов просто игнорирует. Ведь исполнение программы завершено, и этот остаток больше ни для чего не нужен.

Теперь определим комбинатор cst предназначенный для вставления констант в программу:

cst = \a k с -> k a с;

cst просто передаёт продолжению k константу a и неизменённую последовательность выборов (при вычислении константы выбирать ничего не приходится). Определение cst можно немного упростить используя "eta-редукцию". Зачем принимать и передавать c продолжению k в явном виде? Просто выдаём k a, т.е. функцию. И пусть уж она сама и забирает c! Те же соображения применимы и к функции run. Упростив run и cst получаем:

run = \e -> e (\v c -> v);

cst = \a k -> k a;

Теперь можно попробовать просуперкомпилировать первое выражение

run (cst True) --> (\c -> True)

Результат получается вполне разумный: для любой последовательности выборов всегда выдаётся True.

Теперь "возьмём быка за рога" и определим самую интересную конструкцию - choice2 (ради реализации которой всё и затевалось):

choice2 = \e1 e2 k c ->

   case c of {

     L c1 -> e1 k c1;

     R c2 -> e2 k c2;};

choice2 должен решить, какое выражение вычислять: e1 или e2? Для этого и используется c. Если c начинается с L, то выбираем e1, а если с R - то выбираем e2. После чего передаём остаток последовательности выборов либо в e1, либо в e2.

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

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

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

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

  \c -> case c of {

    L c1 -> Z;

    R c2 -> case c2 of { L c21 -> S Z; R c22 -> S (S Z); }; }

Теперь определим самые главные комбинаторы - var, lam и app:

var = \x k -> k x;
lam = \f k -> k f;
app = \e1 e2 k -> e1 (\f -> e2 (\v -> f v k));

Выглядит загадочно, но если не применять eta-редукцию и выписать определения в неоптимизированном виде, то получается

var = \x k c -> k x c;
lam = \f k c -> k f c;
app = \e1 e2 k c -> e1 (\f c1 -> e2 (\v c2 -> f v k c2) c1) c;

Поскольку в реализуемом языке параметры передаются по значению, то с переменными связываются уже "полностью готовые" результаты, а не выражения, которые ещё нужно вычислять (как в случае передачи по имени). Т.е., в значениях переменных уже всё вычислено и никакого недетерминизма уже нет! Поэтому при вычислении var x k c значение переменной x в неизменном виде передаётся продолжению k. Последовательность выборов c тоже передаётся в k без изменения.  То же самое происходит и при вычислении lam f k c. f - это готовая функция, с которой ничего делать не надо.

А вот вычисление app e1 e2 k c - это уже более интересный случай. Сначала вычисляется e1. Ему подсовывается продолжение и последовательность выборов c. Продолжение получает результат f и остаток последовательности выборов c1. Затем c1 подсовывается под e2, и продолжение получает результат v и остаток последовательности выборов c2. После этого имеется известная функция f, известный аргумент v и остаток последовательности выборов c2. Вычисляем f v k c2.

Тонким местом является то, что f - это не просто функция от одного аргумента v, а функция, которая принимает ещё два дополнительных аргумента: продолжение k и последовательность выборов c2!

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

lam (\x -> var x) -->

  \k-> k (\x k1-> k1 x)

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

  (\c -> True)

Теперь наступил момент, когда мы можем вернуться к вопросу о том, какой результат должен получаться в результате вычисления выражения (\x -> P x x) (choice2 True False). Для этого определим комбинатор pairP, формирующий пару из своих двух аргументов:

pairP = \e1 e2 k ->

  e1 (\v1 -> e2 (\v2 -> k (P v1 v2)));

Здесь просто выписано то, что при вычислении pairP e1 e2 нужно сначала вычислить e1, получив v1, затем - e2, получив v2, а затем - выдать P v1 v2. Ну, естественно, при этом должны надлежащим образом выполняться манипуляции с продолжениями и с последовательностью выборов.

Теперь суперкомпилируем

run (app (lam (\x -> pairP (var x) (var x)))

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

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

и видим, что, как мы и хотели, возможными результатами вычисления этого выражения могут быть только P True True и P False False. За что боролись, то и получили.

Теперь, для интереса, напишем недетерминированную программу, генерирующую "произвольное натуральное число". Для этого определим комбинаторы, работающие с натуральными числами:

natZ = \k -> k Z;

natS = \e k -> e (\v -> k (S v));

natCase = \e eZ eS k -> e (\v -> case v of {

  Z -> eZ k;

  S n -> eS n k;

  });

natZ возвращает ноль Z, а natS e вычисляет e, получает значение v и выдаёт S v. Теперь мы умеем генерировать натуральные числа!

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

fix = \e k -> k (fixLoop e);
fixLoop = \e x k -> e(fixLoop e)(\f c1 -> f x k c1);

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

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

Заведём переменную и присвоим ей 0. А дальше будем крутить цикл и на каждом шаге решать: остановиться или продолжать. Если останавливаемся, то выдаём значение переменной в качестве результата. Если решаем не останавливаться, то прибавляем к переменной 1 и крутим цикл дальше.

В функциональных понятиях это можно переформулировать так. Определим функцию

f x = choice2 x (f (S x));

и вычислим выражение

f Z

Теперь расписываем всё это в виде имеющихся у нас комбинаторов. Определение функции f принимает вид

fix (\f -> lam (\x -> choice2 (var x) (app (var f)(natS (var x)))))

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

run (app (fix (\f -> lam (\x -> choice2 (var x) (app (var f)(natS (var x)))))) natZ) c

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

letrec g = \v c1 -> case c1 of {

  L c11 -> v;

  R c12 -> g (S v) c12; }

in g Z c

Ну что же, суперкомпилятор Хоск показал себя молодцом! В остаточной программе от комбинаторов ничего не осталось...

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