scp-notes-ru

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

Сергей Романенко

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 x_1 x_2 ... x_N, то теперь он принимает вид f x_1 x_2 ... x_N 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: higher-order syntax: 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

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

Оригинал послания и комментарии