Интерпретация во время компиляции, или Альтернативное понимание лямбд в C++11

На Хабре недавно проскочила ещё одна статья про вычисления на шаблонах C++ от HurrTheDurr. В комментариях к ней лично я увидел вызов:

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

А так ли сложно будет написать универсальный вычислитель на типах, более удобный для программирования, чем клеточный автомат? Как оказалось, несложно; я в 30 раз больше времени потратил на эту статью, чем на написание и отладку собственно кода вычислителя.

Чуть раньше AveNat опубликовала введение в лямбда-исчисление в двух частях, так что вдохновение пришло мгновенно. Хотелось, чтобы можно было (образно) писать так:

#include <iostream>

#include <LC/kernel.h>
#include <LC/church_numerals.h>

int main()
{
    // Представление натуральных чисел в виде лямбда-абстракций
    typedef ChurchEncode<2> Two;    // 2 = λfx.f (f x)
    typedef ChurchEncode<3> Three;  // 3 = λfx.f (f (f x))

    // * = λab.λf.a (b f)
    typedef Lambda<'a', Lambda<'b', Lambda<'f',
                Apply<Var<'a'>, Apply<Var<'b'>, Var<'f'> > >
        > > > Multiply;

    // Вычисление (* 2 3)
    typedef Eval<Apply<Apply<Multiply, Two>, Three>> Output;

    // Переход обратно от лямбда-абстракций к натуральным числам
    typedef ChurchDecode<Output> Result;

    std::cout << Result::value;
}

А на выходе получать такое:

ilammy@ferocity ~ $ gcc cpp.cpp
ilammy@ferocity ~ $ ./a.out
6

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

Под катом находится очередное прокомментированное конструктивное доказательство Тьюринг-полноты шаблонов C++ в виде compile-time интерпретатора бестипового лямбда-исчисления (плюс печеньки в виде макросов и рекурсии).

(Так как компиляторы C++03 требуют <асимметричных<угловых<скобок<в<шаблонах> > > > >, а меня в большинстве случаев коробит от их внешнего вида, то для компиляции необходима или поддержка C++11, или sed ':l;s/>>/> >/g;tl'. За исключением части про макросы, в коде не используются никакие другие возможности C++11.)

Синтаксис

Поехали. Как известно, термы в лямбда-исчислении бывают трёх видов:

	ссылка на переменную	v — имя переменной
	абстракция	v — имя переменной, B — терм
	аппликация	f и x — термы

Все эти конструкции необходимо представить с помощью шаблонов C++. Значениями в языке шаблонов являются типы. Каждый из этих типов должен нести информацию о своих компонентах. Объявляя их, мы вводим аксиому «существуют следующие выражения»:

template <class Var>            struct Ref; // ссылки
template <class Var, class Exp> struct Lam; // абстракции
template <class Fun, class Arg> struct App; // аппликации

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

template <char  Var>            struct Ref;
template <char  Var, class Exp> struct Lam;
template <class Fun, class Arg> struct App;

Мы воспользовались возможностью шаблонизации с помощью целочисленных значений. Вот только значениятипа char можно записывать ещё и строками, что очень удобно: не надо заранее объявлять каждую переменную, используемую в программе. Заодно это явно показывает, что сами переменные не являются значениями (то есть типами C++).

Теперь мы можем записывать с помощью шаблонов любые лямбда-термы!

typedef Lam<'f', App<Lam<'x', App<Ref<'f'>, App<Ref<'x'>, Ref<'x'>>>>,
                     Lam<'x', App<Ref<'f'>, App<Ref<'x'>, Ref<'x'>>>>>> Y;

Что дальше?

Умея записывать термы, необходимо научиться их вычислять. Вот тут уже всё не так просто, поэтому применим достаточно известный подход к написанию адовой магии на шаблонах: сначала всё записать на каком-нибудь декларативном языке программирования, затем только исправить синтаксические различия. Лично мне ближе Scheme, так что я буду использовать его. С равным успехом можно применить и любой другой функциональный язык вроде Haskell. (А ещё лучше — Пролог.)

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

; Y = λf.(λx.f (x x)) (λx.f (x x))
(define Y '(lambda (f) ((lambda (x) (f (x x)))
                        (lambda (x) (f (x x))) )))

Зафиксируем синтаксис лямбда-исчисления:

; Терм — это ссылка, абстракция, или аппликация.
(define (term? exp)
  (or (ref? exp) (lam? exp) (app? exp)) )

; Ссылки записываются символами.
(define (ref? exp) (symbol? exp))

; Абстракция — это список из трёх элементов.
(define (lam? exp)
  (and (list-of? 3 exp)
; Где первый — это символ lambda.
       (eqv? 'lambda (first exp))
; Второй — это список из одного символа.
       (list-of? 1 (second exp))
       (symbol? (first (second exp)))
; А третий — это терм.
       (term? (third exp)) ) )

; Аппликация — это список из двух термов.
(define (app? exp)
  (and (list-of? 2 exp)
       (term? (first exp))
       (term? (second exp)) ) )

Далее определим функцию eval, которая будет интерпретировать термы, различая их по синтаксису:

(define (eval exp)
  (cond ((ref? exp) (eval-ref exp))
        ((lam? exp) (eval-lam (first (second exp)) (third exp)))
        ((app? exp) (eval-app (first exp) (second exp)))
        (else (error "eval: syntax error" exp)) ) )

Отлично. Но как реализовать eval-ref? Откуда интерпретатор узнает значение переменной? Для этого существует такое понятие как окружение (environment). В окружениях сохраняются связи между переменными и их значениями. Поэтому eval на самом деле выглядит так — с дополнительным аргументом:

(define (eval exp env)
  (cond ((ref? exp) (eval-ref exp env))
        ((lam? exp) (eval-lam (first (second exp)) (third exp) env))
        ((app? exp) (eval-app (first exp) (second exp) env))
        (else (error "Syntax error" exp)) ) )

Теперь вычисление ссылки на переменную определяется просто — это поиск значения переменной в окружении:

(define (eval-ref var env)
  (lookup var env) )

Значением абстракции должна быть анонимная функция одного аргумента. Эту функцию вызовет аппликация, когда придёт время. Смысл абстракции состоит в том, чтобы вычислить своё тело exp в окружении, где переменная абстракции var имеет значение переданного аргумента arg. О создании такого окружения позаботится функция bind.

(define (eval-lam var exp env)
  (lambda (arg)
    (eval exp (bind var arg env)) ) )

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

Наконец, аппликация — применение значения абстракции fun к значению аргумента arg.

(define (eval-app fun arg env)
  ((eval fun env) (eval arg env)) )

Здесь сначала вычисляется абстракция и её аргумент, а потом уже происходит вызов. Соответственно, eval выполняет редукцию лямбда-термов в аппликативном порядке (с вызовом по значению).

Осталось только определить пару функций для работы с окружениями. lookup для поиска значения переменной в окружении и bind для создания новых окружений:

(define (bind var val env)       ; Для окружений используются ассоциативные списки:
  (cons (cons var val) env) )    ;   (bind 'x 1 '((y . 2)))  ===>  ((x . 1) (y . 1))
                                 ;   (lookup 'x '((x . 1) (y . 2)))  ===>  1
(define (lookup var env)         ;   (lookup 'y '((x . 1) (y . 2)))  ===>  2
  (let ((cell (assq var env)))   ;   (lookup 'z '((x . 1) (y . 2)))  ===>  #<ERROR>
    (if cell (cdr cell)
        (error "lookup: unbound variable" var) ) ) )

Супер! У нас есть интерпретатор лямбда-исчисления, написанный в чистом функциональном стиле. (Весь исходник.) И он даже работает:

(eval '((lambda (x) x) B)
       (bind 'B 42 '()) ) ; ===> 42

Но что за скобки? И при чём здесь C++?

Глядя на исходный код интерпретатора на Scheme, можно относительно легко догадаться, как писать интерпретатор лямбда-термов на шаблонах C++. Напомню, что сами термы записываются следующими шаблонами:

template <char  Var>            struct Ref;
template <char  Var, class Exp> struct Lam;
template <class Fun, class Arg> struct App;

Шаблонные функции (не те)

Функция-интерпретатор называется Eval. Так как в шаблонах нет функций, то нам придётся обойтись одними шаблонами:

template <class Exp, class Env> struct Eval;

Вызовом такой функции является инстанциирование шаблона: Eval<Exp, Env>. Возвращаемое значение этого вызова должно быть типом C++. Условимся, что Eval определяет внутри себя тип value, если её значение определено для переданных аргументов:

typename Eval<Exp, Env>::value

Подобный код позволяет получить значение вызова Eval с аргументами Exp и Env (в виде типа value). Если конкретный вызов ошибочен (не имеет смысла), то тип value не будет определён и мы получим ошибку времени компиляции. Подобным образом определяются и другие «шаблонные функции».

Eval и Apply

Теперь с помощью частичной специализации шаблонов мы можем декларативно описать поведение Eval. Например, вычисление ссылки на переменную — это поиск значения переменной в окружении с помощью функции Lookup (она возвращает значение через result):

template <char Var, class Env>
struct Eval<Ref<Var>, Env>
{
    typedef typename Lookup<Var, Env>::result value;
};

Результат вычисления абстракции — это замыкание, представляемое шаблонным типом Closure. Замыкание сохраняет в себе (анонимную) функцию и окружение определения этой функции:

template <char Var, class Exp, class Env>
struct Eval<Lam<Var, Exp>, Env>
{
    typedef Closure<Lam<Var, Exp>, Env> value;
};

Результат вычисления аппликации — это применение вычисленного замыкания к вычисленному аргументу (выполняемое функцией Apply):

template <class Fun, class Arg, class Env>
struct Eval<App<Fun, Arg>, Env>
{
    typedef typename Apply<typename Eval<Fun, Env>::value,
                           typename Eval<Arg, Env>::value>::result value;
};

Таким образом, Eval определена только для Ref, Lam, App (и окружений вторым аргументом). Вызовы Eval с другими аргументами просто не скомпилируются.

Идём дальше. Замыкания — это просто структуры данных интерпретатора, хранящие два значения (функцию и окружение её определения). Реализуются, естественно, ещё одним шаблоном:

template <class Abs, class Env> struct Closure;

Вся суть лямбда-исчисления сконцентрирована в определении функции Apply. Замыкания вычисляются в окружении своего определения, которое Bind расширяет привязкой аргумента вычисляемой функции к его фактическому значению:

template <class Fun, class Arg> struct Apply;

template <char Var, class Exp, class Env, class Arg>
struct Apply<Closure<Lam<Var, Exp>, Env>, Arg>
{
    typedef typename Eval<Exp, Bind<Var, Arg, Env>>::value result;
};

(Заметьте, что Apply в принципе можно определить вообще для чего угодно, не только для применения абстракций.)

Lookup и Bind

Осталось разобраться с окружениями. Для начала, неплохо было бы иметь пустое окружение:

struct NullEnv;

Далее, необходимо реализовать механизм расширения окружений с помощью Bind. Этот тип данных определяет новое окружение, в котором переменная Var связана со значением Val, а значения остальных переменных определяются окружением Env:

template <char Var, class Val, class Env> struct Bind;

Получили своеобразный связный список на шаблонах.

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

template <char Var, class Env> struct Lookup;

В пустом окружении ничего нет. Если искомое значение есть в текущем окружении, то возвращаем его. Иначе рекурсивно просматриваем остальные окружения:

template <char Var>
struct Lookup<Var, NullEnv>;

template <char Var, class Val, class Env>
struct Lookup<Var, Bind<Var, Val, Env>>
{
    typedef Val result;
};

template <char Var, char OtherVar, class Val, class Env>
struct Lookup<Var, Bind<OtherVar, Val, Env>>
{
    typedef typename Lookup<Var, Env>::result result;
};

Конец

Вот так в 50 строках мы полностью определили синтаксис и семантику лямбда-исчисления с помощью шаблонов C++, что доказывает Тьюринг-полноту механизма раскрытия шаблонов C++ (при условии неограниченного объёма доступной памяти).

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

Окей, попробуем провести простейшее вычисление, используя полученные возможности (полный код):

/* Определения, показанные выше */

#include <iostream>

int main()
{
    // 1 = λfx.f x
    typedef Lam<'f', Lam<'x', App<Ref<'f'>, Ref<'x'>>>> One;

    // 2 = λfx.f (f x)
    typedef Lam<'f', Lam<'x', App<Ref<'f'>, App<Ref<'f'>, Ref<'x'>>>>> Two;

    // + = λab.λfx.a f (b f x)
    typedef Lam<'a', Lam<'b', Lam<'f', Lam<'x',
                App<App<Ref<'a'>, Ref<'f'>>,
                    App<App<Ref<'b'>, Ref<'f'>>, Ref<'x'>>>
        >>>> Plus;

    // Output := (+ 1 2)
    typedef Eval<App<App<Plus, One>, Two>, NullEnv>::value Output;

    // Э-э-э... А как вывести результат?
    Output::invalid_field;
}

ilammy@ferocity ~/dev/tlc $ g++ -std=c++11 lc.cpp
lc.cpp: В функции «int main()»:
lc.cpp:79:5: ошибка: неполный тип «Output {aka Closure<Lam<'f', Lam<'x', App<App<Ref<'a'>, Ref<'f'> >, App<App<Ref<'b'>, Ref<'f'> >, Ref<'x'> > > > >, Bind<'b', Closure<Lam<'f', Lam<'x', App<Ref<'f'>, App<Ref<'f'>, Ref<'x'> > > > >, NullEnv>, Bind<'a', Closure<Lam<'f', Lam<'x', App<Ref<'f'>, Ref<'x'> > > >, NullEnv>, NullEnv> > >}» использован во вложенном спецификаторе имени
     Output::invalid_field;
     ^

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

Расширение множества термов

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

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

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

Чтобы получить возможность расшифровки результатов вычислений, необходимо использовать прикладное лямбда-исчисление — в нём множество термов расширено элементами некоторого предметного множества. В нашем случае это будет множество типов данных C++.

Введём для них соответствующий терм:

template <class T> struct Inj;

Он обозначает инъекцию типа T во множество термов лямбда-исчисления.

После расширения синтаксиса необходимо уточнить семантику языка — определить с помощью Eval значение новой синтаксической конструкции. Ну… так как T — это произвольное значение, то Eval о нём известно лишь то, что такое значение существует. Единственный смысл, который можно придать функции в подобных условиях — это тождество:

template <class T, class Env>
struct Eval<Inj<T>, Env>
{
    typedef T value;
};

Теперь мы можем передавать в качестве аргументов числа (представленные типами):

struct Zero
{
    static const unsigned int interpretation = 0;
};

Осталось придумать, как передать функцию, и мы сможем превращать числа Чёрча в нормальные числа int. Ведь если N раз применить функцию инкремента к нулю, то в итоге получится натуральное число N.

Представим, что каким-то образом мы смогли это сделать, передав в интерпретатор типы Succ (successor) и Zero. Проследим, что происходит при вызове такой функции:

Eval<App<Inj<Succ>, Inj<Zero>>, Env>::value

Apply<Eval<Inj<Succ>, Env>, Eval<Inj<Zero>, Env>>::result

Apply<Succ, Zero>::result

Бинго! Для определения поведения Succ необходимо специализировать Apply для неё! (Подобные преобразования называются дельта-правилами.)

Например, вот так определяется функция инкремента:

struct Succ;

template <class N>
struct Apply<Succ, N>
{
    typedef struct _ {
        static const unsigned int interpretation = N::interpretation + 1;
    } result;
};

Возвращаемое значение Apply должно быть типом, объявленным как result. Поэтому результатом инкремента является тип данных, структурно идентичный описанному выше Zero. Это позволяет представить натуральные числа нешаблонными типами данных, сохраняя возможность получить обычный int с соответствующим значением.

Теперь наконец можно вывести результат сложения! (Полный код.)

/* Определения, показанные выше */

#include <iostream>

int main()
{
    // 1 = λfx.f x
    typedef Lam<'f', Lam<'x', App<Ref<'f'>, Ref<'x'>>>> One;

    // 2 = λfx.f (f x)
    typedef Lam<'f', Lam<'x', App<Ref<'f'>, App<Ref<'f'>, Ref<'x'>>>>> Two;

    // + = λab.λfx.a f (b f x)
    typedef Lam<'a', Lam<'b', Lam<'f', Lam<'x',
                App<App<Ref<'a'>, Ref<'f'>>,
                    App<App<Ref<'b'>, Ref<'f'>>, Ref<'x'>>>
        >>>> Plus;

    // Sum = (+ 1 2)
    typedef App<App<Plus, One>, Two> Sum;

    // Result := (Sum +1 =0)
    typedef App<App<Sum, Inj<Succ>>, Inj<Zero>> Output;

    typedef Eval<Output, NullEnv>::value Result;

    std::cout << Result::interpretation;
}

ilammy@ferocity ~/dev/tlc $ g++ -std=c++11 lc.cpp

ilammy@ferocity ~/dev/tlc $ ./a.out
3

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

Я думаю, вы уже заметили, что в main() мы всегда вызываем Eval с пустым окружением, а все необходимые абстракции «инлайним». Но это вовсе не обязательно. Если передать в первый вызов Eval какое-то окружение, то оно будет играть роль глобального для вычисляемого терма: именно оно задаёт значения свободных переменных — тех, которые ни с чем не связаны лямбда-абстракциями.

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

/* ... */

#include <iostream>

int main()
{
    /* Определения One, Two, Plus пропущены */

    // Unchurch = λn.(n +1 =0), преобразование чисел Чёрча в int
    typedef Lam<'n', App<App<Ref<'n'>, Ref<'I'>>, Ref<'O'>>> Unchurch;

    // Result := (Unchurch (+ 1 2))
    typedef Eval<App<Ref<'U'>,
                     App<App<Ref<'+'>, Ref<'1'>>, Ref<'2'>>>,

                Bind<'+', typename Eval<Plus, NullEnv>::value,
                Bind<'1', typename Eval<One,  NullEnv>::value,
                Bind<'2', typename Eval<Two,  NullEnv>::value,
                Bind<'U', typename Eval<Unchurch,
                                        Bind<'I', Succ,
                                        Bind<'O', Zero,
                                            NullEnv>>
                                    >::value,
                    NullEnv>>>>

        >::value Result;

    std::cout << Result::interpretation;
}

Окружения представляют память интерпретатора. Если бы это был компилятор с линкером, то там должны были бы лежать скомпилированные функции. В случае же интерпретатора они находятся в «предвычисленном» состоянии — уже пропущенные через Eval.

Ещё стоит обратить внимание на свободные переменные Unchurch. Они входят в окружение безо всяких Inj вокруг. Это тоже потому, что в памяти интерпретатора эти значения представляются именно таким образом. Inj необходима только для записи их в тексте программ (в лямбда-термах).

Макросы

Никого ещё не достало, что для записи функций нескольких аргументов их необходимо вручную каррировать? И все эти постоянные Ref<'foo'>?

А между прочим, даже в лямбда-исчислении приняты удобные сокращения:

До	После

Давайте реализуем такие же.

Существует множество подходов к реализации макросов. Для нашего случая стоит избрать самый простой: внешний препроцессор. «Внешний» означает, что определения макросов находятся вне обрабатываемой программы. То есть мы не будем вводить какой-либо новый синтаксис для лямбда-исчисления, чтобы выражать внутри него макросы; это было бы слишком сложно. Макропроцессор просто «натравливается» на программу и на выходе выдаёт чистый лямбда-терм — так же, к примеру, работает MOC в Qt.

Две фазы

До этого момента в жизни наших программ было только одно важное событие — определение их значения с помощью Eval. Теперь к нему прибавится ещё раскрытие макросов с помощью Expand. Всё, что подаётся на вход Eval, сначала необходимо пропустить через Expand. Введём новую удобную функцию Compute, которая объединяет эти действия:

template <class Exp> struct Expand;

template <class Exp, class Env>
struct Compute
{
    typedef typename Eval<typename Expand<Exp>::result, Env>::value value;
};

Expand принимает только один аргумент. Будем считать, что это чёрный ящик: на входе программа с макросами, на выходе — без них. В нашем простом случае не нужны какие-либо макроокружения.

Реализация макросов

Теперь макросы, очевидно, необходимо реализовать внутри Expand. Нам нужны некие Lam_ и App_, которые раскрываются следующим образом:

В C++11 появились шаблоны произвольной арности, что порядком облегчает задачу. Обладателям компиляторов C++03 остаётся только страдать и писать тысячу и одну специализацию: Lam_2 для двух аргументов, Lam_3 для трёх, App_4 для четырёх, и т. д. Ну, или извращаться ещё сильнее и повторить всё, что показано ниже, с помощью родного препроцессора C++.

Lam_

Правда, даже у шаблонов С++11 есть свои ограничения, поэтому синтаксис придётся ещё чуть-чуть подпилить. Пачка аргументов может быть только последним аргументом шаблона, поэтому для Lam_ необходимо ввести специальную «держалку аргументов»:

template <char... Vars> struct Args;
template <class Args, class Exp> struct Lam_;

template <char Var, class Exp>
struct Expand<Lam_<Args<Var>, Exp>>
{
    typedef typename Expand<Lam<Var, Exp>>::result result;
};

template <char Var, char... Vars, class Exp>
struct Expand<Lam_<Args<Var, Vars...>, Exp>>
{
    typedef Lam<Var, typename Expand<Lam_<Args<Vars...>, Exp>>::result> result;
};

Обратите внимание на повторные вызовы Expand в процессе раскрытия. Они необходимы, так как Expand<...>::result всегда должен быть чистым лямбда-термом без макросов.

App_

А ещё шаблоны C++11 не позволяют смешивать в пачке аргументы-числа и аргументы-типы, поэтому у App_ будет два соответствующих варианта. Печалька.

Реализации App_s (для символов) и App_i (для типов) более объёмные, поэтому объяснения и код спрятаны под спойлер.

struct Nil;
template <class First, class Rest> struct RefList;

template <char... Vars> struct ToRefList_s;

template <char Var>
struct ToRefList_s<Var>
{
    typedef RefList<Ref<Var>, Nil> result;
};

template <char Var, char... Vars>
struct ToRefList_s<Var, Vars...>
{
    typedef RefList<Ref<Var>, typename ToRefList_s<Vars...>::result> result;
};

template <class... Exps> struct ToRefList_i;

template <class Exp>
struct ToRefList_i<Exp>
{
    typedef RefList<Exp, Nil> result;
};

template <class Exp, class... Exps>
struct ToRefList_i<Exp, Exps...>
{
    typedef RefList<Exp, typename ToRefList_i<Exps...>::result> result;
};

template <class Apps, class RefList> struct App_wrap;

template <class A, class D, class R>
struct App_wrap<Nil, RefList<A, RefList<D, R>>>
{
    typedef typename App_wrap<App<A, D>, R>::result result;
};

template <class Apps, class A>
struct App_wrap<Apps, RefList<A, Nil>>
{
    typedef typename App_wrap<App<Apps, A>, Nil>::result result;
};

template <class Apps, class A, class D>
struct App_wrap<Apps, RefList<A, D>>
{
    typedef typename App_wrap<App<Apps, A>, D>::result result;
};

template <class Apps>
struct App_wrap<Apps, Nil>
{
    typedef Apps result;
};

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

template <char...  Exps> struct App_s;
template <class... Exps> struct App_i;

template <char... Exps>
struct Expand<App_s<Exps...>>
{
    typedef typename Expand<
                typename App_wrap<Nil,
                    typename ToRefList_s<Exps...>::result
            >::result
        >::result result;
};

template <class... Exps>
struct Expand<App_i<Exps...>>
{
    typedef typename Expand<
                typename App_wrap<Nil,
                    typename ToRefList_i<Exps...>::result
            >::result
        >::result result;
};

Остальное

И последнее, но важное дополнение. Экспандер должен правильно обрабатывать встроенные конструкции языка, раскрывая макросы там, где они могут встретиться:

template <char Var>
struct Expand<Ref<Var>>
{
    typedef Ref<Var> result;
};

template <char Var, class Exp>
struct Expand<Lam<Var, Exp>>
{
    typedef Lam<Var, typename Expand<Exp>::result> result;
};

template <class Fun, class Arg>
struct Expand<App<Fun, Arg>>
{
    typedef App<typename Expand<Fun>::result,
                typename Expand<Arg>::result> result;
};

Кто заметил в работе Expand параллели с Eval и Apply, тот молодец.
(Полный код с поддержкой макросов.)

Рекурсия

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

В лямбда-исчислении нельзя выразить рекурсию напрямую, так как у абстракций отсутствуют имена. Для записи рекурсии в привычном виде потребуется магический оператор Rec, который подобен обычной абстракции Lam, но создаёт абстракции с дополнительным аргументом — ссылкой на саму определяемую абстракцию.

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

// Y = λf.(λx.f (x x)) (λx.f (x x))
typedef Lam<'f', App<Lam<'x', App<Ref<'f'>, App_s<'x', 'x'>>>,
                     Lam<'x', App<Ref<'f'>, App_s<'x', 'x'>>>>> Y;

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

В конечном счёте, все нужные определения связываются с соответствующими символами и укладываются в окружение StandardLibrary. Теперь можно красиво и удобно записать производящую функцию для факториала:

// F = λfn.if (= n 0) 1
//            (* n (f (- n 1)))
typedef Lam_<Args<'f', 'n'>,
            App_i<Ref<'?'>, App_s<'=', 'n', '0'>,
                Ref<'1'>,
                App_i<Ref<'*'>, Ref<'n'>,
                      App_i<Ref<'f'>, App_s<'-', 'n', '1'>>> > > Fact_gen;

Она отличается от обычной унарной тем, что принимает дополнительный аргумент f — функцию вычисления факториала (уже обычную). Роль Y-комбинатора состоит в том, чтобы по производящей функции Fact_gen определить такую функцию Fact, чтобы App<Fact_gen, Fact> ≡ Fact — это и называется: «найти неподвижную точку».

Окей, попробуем применить всё это вместе, вычислив (Y F 1) — факториал единички:

/* ... */

#include <iostream>

int main()
{
    /* Определения Y и Fact_gen */

    typedef Compute<App<Ref<'U'>,
                App_i<Y, Fact_gen, MakeChurch(1)> >,
            StandardLibrary>::value Result;

    std::cout << Result::interpretation;
}

ilammy@ferocity ~/dev/tlc $ g++ -std=c++11 lc.cpp 2>&1 | wc -c
64596

Не компилируется. И лог ошибок на 64 килобайта. Почему?

Всё дело в порядке вычислений. Обычный Y-комбинатор записывается из расчёта на нормальный порядок вычислений. В нём кусочек f (x x) сначала вызовет подстановку (x x) в тело f, и только потом, если это понадобится, значение (x x) будет вычислено (тоже с ленивой подстановкой).

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

Если расшифровать лог, выплёвываемый gcc, то там так и написано, что:

struct Apply<
    Closure<
        Lam<'x', App<Ref<'f'>, App<Ref<'x'>, Ref<'x'>>>>,
        Bind<'f',
            Closure<Fact_gen, StandardLibrary>,
            StandardLibrary > >,
    Closure<
        Lam<'x', App<Ref<'f'>, App<Ref<'x'>, Ref<'x'>>>>,
        Bind<'f',
            Closure<Fact_gen, StandardLibrary>,
            StandardLibrary > > >

не определяет типа result, то есть этот вызов не имеет смысла. Компилятор увидел и разорвал бесконечный цикл подстановки шаблонов, который по стандарту является неопределённым (14.7.1/15).

Шаблоны C++ тоже проводят вычисления в аппликативном порядке, потому что вызовом функции typename Eval<Exp, Env>::value является инстанциирование шаблона. Инстанциирование Eval очевидно требует инстанциирования Exp и Env.

В языках с аппликативным порядком вычислений следует применять Z-комбинатор — модификацию Y-комбинатора, в которой выражение (x x) завёрнуто в абстракцию, что предотвращает его преждевременное вычисление:

// Z = λf.(λx.f (λy.x x y)) (λx.f (λy.x x y))
typedef Lam<'f', App<Lam<'x', App<Ref<'f'>, Lam<'y', App_s<'x', 'x', 'y'>>>>,
                     Lam<'x', App<Ref<'f'>, Lam<'y', App_s<'x', 'x', 'y'>>>>>> Z;

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

Стоп! А когда компилятор вообще должен прекратить подставлять факториал сам в себя? В смысле, когда мы хотим, чтобы он прекратил так делать? По идее, за это отвечает оператор If: когда аргумент факториала равен нулю, то нужно вернуть единицу, а не пытаться делать рекурсивный вызов. А как определяется If?

typedef Lam_<Args<'c', 't', 'f'>, App_s<'c', 't', 'f'>> If;

Как абстракция. Вроде бы всё хорошо, стандартное определение для булевых констант Чёрча… Вот только рассчитано оно тоже на нормальный порядок редукции! При аппликативном порядке If вычисляет обе ветки сразу вместе с условием, и только после этого делает выбор.

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

template <class Cond, class Then, class Else> struct If;

template <class Cond, class Then, class Else>
struct Expand<If<Cond, Then, Else>>
{
    typedef typename Expand<
        App_i<Cond, Lam<'u', Then>,
                    Lam<'u', Else>,
                    Lam<'u', Ref<'u'>> >
    >::result result;
};

Строго говоря, переменная 'u' не должна совпадать ни с одной свободной переменной Then или Else. Такой возможности (гигиены) наша макросистема не предоставляет. И вообще, имён переменных у нас весьма ограниченное количество. Поэтому зарезервируем идентификатор 0 в качестве ни с чем не совпадающего идентификатора:

template <char Var>
struct Lookup<Var, NullEnv>;

template <class Env>
struct Lookup<0, Env>;

template <char Var, class Val, class Env>
struct Lookup<Var, Bind<Var, Val, Env>>
{
    typedef Val result;
};

Вот теперь наконец-то факториал заработает. (Полный код.)

ilammy@ferocity ~/dev/tlc $ time g++ -std=c++11 lc.cpp -DARG=6

real    0m12.630s
user    0m11.979s
sys     0m0.466s

ilammy@ferocity ~/dev/tlc $ ./a.out
720

К сожалению, дождаться вычисления факториала семи мне не удалось, не говоря уже о том, что на 32-битных системах компилятор попросту умирает от переполнения стека. Но всё равно!..

Заключение

Практической инженерной пользы от этого интерпретатора, наверное, никакой нет, но сама по себе идея восхитительна. Шаблоны C++ — это она из «нечаянно Тьюринг-полных» вещей в теоретической информатике. Схожее ощущение у меня возникло разве что тогда, когда я узнал, что подсистема управления страничной памятью x86-процессоров тоже полна по Тьюрингу. Если этот интерпретатор позволяет выполнять вычисления, не выполняя ни одного оператора C++, то MMU позволяет выполнять вычисления, не выполняя ни одной машинной инструкции программы.

К сожалению, DCPL я дочитал пока только до восьмой главы, поэтому написание интерпретатора типизированного лямбда-исчисления оставляется читателям в качестве упражнения. У меня пока ещё слишком слабая математическая подготовка для этого.

P.S. Всё время, пока я писал пост, меня не покидала мысль: «Это или уже есть в Бусте, или пишется там в три строки».

Автор: ilammy

Источник