было показано, что недетерминированные программы можно писать в рамках детерминированного ленивого функционального языка, реализовав с помощью комбинаторов проблемно-ориентированный язык, содержащий конструкцию "произвольного выбора". Идея-то с виду простая: реализуем конструкцию choice2 e1 e2. И пусть вычисление этой конструкции сводиться к вычислению e1 или e2, а выбор между e1 и e2 делается произвольно.
Или, говоря более формально, считаем, что семантика языка определяется через правила редукции выражений (т.е. сведения одних выражений к другим), просто считаем, что для choice2 определено два правила редукции:
Вроде бы, всё ясно и понятно... Однако, есть тут один "подводный камень". Рассмотрим такое недетерминированное выражение:
Когда выбирать: когда нужен результат или при передаче параметра?
Из рассмотренного примера видно, что результат вычисления недетерминированных конструкций может зависеть от порядка вычислений и от моментов, в которые производится выбор между возможностями. Можно затягивать выбор до последней возможности: выбирать только тогда, когда результат, возвращаемый конструкцией выбора реально понадобился. В литературе этот вариант называется "выбором по надобности" (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
Ну что же, суперкомпилятор Хоск показал себя молодцом! В остаточной программе от комбинаторов ничего не осталось...
