Категориальная абстрактная машина

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

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

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

1. определена функция тождества, или тождественное преобразование (имеющее в комбинаторной логике аналог в форме комбинатора тождества I);
2. определена операция композиции или построения сложной функции (имеющая в комбинаторной логике аналог в форме комбинатора тождества B);
3. определена операция образования упорядоченной пары объектов < . , . >;
4. определена операция взятия первого элемента из упорядоченной пары объектов;
5. определена операция взятия второго элемента из упорядоченной пары объектов;
6. определена операция преобразования терма из алгебраической формы в аппликативную;
7. определена операция аппликации или применения функции к аргументу.

Заметим, что выполнение перечисленных условий необходимо для того, чтобы обеспечить принадлежность состояний категориальной абстрактной машины пространству д.з.к..
Напомним характеристические равенства, которые определяют поведение операторов, задающих синтаксис и семантику языка инструкций категориальной абстрактной машины:
(ass)    (xoy)z = x(yz);
(fst)    Fst[x,y] = x;
(snd)    Snd[x,y] = y;
(dpair)  <x,y>z = [xz,yz];    
(ac)     ε[Λ(x)y,z] = x[y,z];
(quote)  (‘x)y = x.
Соотношение (ass) устанавливает связь аппликации и композиции, соотношения (fst) и (snd) – первой и второй проекций и операции образования упорядоченной пары, соотношение (dpair) – спаривания и формирования совокупности, соотношение (ac) – каррирования и апплицирования, а (quote) характеризует цитирование.
Заметим, что данный перечень характеристических соотношений категориальной комбинаторной логики является базисным и получен с учетом устранения избыточных комбинаторов из рассматриваемой формальной системы.
Завершив этап предварительной подготовки необходимого набора соотношений, перейдем непосредственно к реализации поставленной задачи формализации процедуры трансляции функциональной программы.
Схема процедуры трансляции текста программы на языке функционального программирования в результирующую последовательность инструкций категориальной абстрактной машины является многоэтапной и включает следующие стадии:

1. преобразование текста программы на языке функционального программирования в соответствующее выражение ламбда-исчисления;
2. преобразование полученного выражения ламбда-исчисления в так называемый (промежуточный) код де Брейна (de Brujin);
3. преобразование полученного кода де Брейна в терм категориальной комбинаторной логики;
4. преобразование полученного терма категориальной комбинаторной логики в последовательность инструкций категориальной абстрактной машины;
5. выполнение результирующей последовательности инструкций категориальной абстрактной машины с означиванием в среде вычислений.

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

1. числа де Брейна, замещающие переменные ламбда-термов, заменяются соответствующими комбинаторами n, рассмотренными в ходе предыдущей лекции;
2. операция аппликации заменяется комбинатором S;
3. операция абстракции заменяется комбинатором Λ = λx.(λz.x[y,z]);
4. операция цитирования (в случае наличия в ламбда-терме констант) заменяется комбинатором цитирования ‘ = K = λx.(λy.x).

Проиллюстрируем кодирование ламбда-терма по де Брейну следующим примером. Пусть требуется закодировать ламбда-терм следующего вида:
λx.λy.((+x)y).
В результате получаем код де Брейна следующего вида:
Λ(Λ(S(S(‘+1),0))).
В наших рассуждениях неоднократно использовалось понятие среды вычислений. Среда имеет важнейшее значение в теории и практике языков программирования, поскольку она определяет условия для выполнения той или иной программы в зависимости от характеристик компьютера, операционной системы, транслятора и другого окружения, в котором программа функционирует. Из истории языков программирования естественным образом следует, что в ходе эволюции программных систем среда изменялась в сторону повышения адаптивности и универсальности. Пожалуй, апогеем развития современных вычислительных сред является изучаемая в курсе технологическая платформа Microsoft .NET.
Формализуем понятие среды вычислений применительно к категориальной абстрактной машине.
При кодировании ламбда-выражений по де Брейну среда вычислений понимается как конечное упорядоченное множество пар вида
(<переменная>, <значение>).
При трансляции ламбда-терма в код де Брейна, который представляет собой пару вида (<терм де Брейна>, <среда>) в соответствии с характеристическими равенствами
0![x,y] = y;
(n+1)![x,y] = n!x;
S[x,y] z = xz(yz);Λ(x)yz = x[y,z];
среда вырождается в пустую и обозначается как «( )», а значения переменных явным образом присутствуют в результирующем коде.
Рассмотрим следующий этап процедуры трансляции, который состоит в преобразовании полученного кода де Брейна в выражение категориальной комбинаторной логики.
Переход от кода де Брейна к терму категориальной комбинаторной логики выполняется на основе известных характеристических равенств:
(ass)    (xoy)z = x(yz);
(fst)    Fst[x,y] = x;
(snd)    Snd[x,y] = y;
(dpair)  <x,y>z = [xz,yz];    
(ac)     ε[Λ(x)y,z] = x[y,z];
(quote)  (‘x)y = x.
Таким образом, в результате данного этапа трансляции получается «программа» в форме выражений категориальной комбинаторной логики, в значительной мере схожим с языком программирования.
При этом список «инструкций» «языка программирования» категориальной комбинаторной логики имеет следующий вид («команды» разделены пробелами и указаны без кавычек):
< , > Fst Snd ‘ Λε.
Рассмотрим следующий этап процедуры трансляции, который состоит в преобразовании полученного выражения категориальной комбинаторной логики в «инструкции» «языка программирования» категориальной абстрактной машины.
Отображение выражений категориальной комбинаторной логики в соответствующие «инструкции» категориальной абстрактной машины удобно представить в форме таблицы.
При этом каждая инструкция категориальной абстрактной машины изменяет состояние КАМ, которое определяется значениями тройки {T, C, S}. Смысл состояний КАМ удобно представить в виде таблицы.
Таким образом, процесс работы КАМ сводится к смене состояний вида:
{T, C, S} -> {T’, C’, S’}.
Для завершения описания процедуры функционирования категориальной абстрактной машины осталось описать динамику состояний КАМ.
Циклом работы КАМ назовем множество всевозможных изменений (динамики) ее состояний.
Цикл работы КАМ удобно представить в виде таблицы.
Поскольку в данной таблице рассмотрены все возможные инструкции категориальной абстрактной машины, можно сделать вывод о том, что формализация проведена в полном объеме.

Проиллюстрируем процедуру трансляции программы на языке функционального программирования в последовательность инструкций категориальной абстрактной машины с последующим вычислением результирующего значения в среде на примере.
Рассмотрим текст следующей программы на языке функционального программирования SML:
val curry = fn f => fn x => fn y => f(x,y);
fun sum ab = a+b;
(curry sum) 1 2;
Заметим, что данная программа на языке SML реализует функцию вычисления значения суммы целых чисел 1 и 2, представленную в каррированной форме.
Рассмотрим поэтапно процедуру трансляции программы на языке функционального программирования в последовательность инструкций категориальной абстрактной машины с последующим вычислением результирующего значения в среде.
На первом этапе процедуры трансляции произведем преобразование текста программы на языке функционального программирования в соответствующее выражение ламбда-исчисления.
В результате получим:
((λx.x)1((λx.x)2))+.
На втором этапе процедуры трансляции произведем преобразование полученного выражения ламбда-исчисления в код де Брейна.
В результате получим:
(λ.0 1((λ.0)2)+.
На третьем этапе процедуры трансляции произведем преобразование полученного кода де Брейна в терм категориальной комбинаторной логики.
В результате получим:
<Λ(<<Snd,‘1>ε,<Λ(Snd),‘2 >ε>ε),‘+>ε.
На четвертом этапе процедуры трансляции произведем преобразование полученного терма категориальной комбинаторной логики в последовательность инструкций категориальной абстрактной машины.
В результате получим:
push cur (push push cdr swap quote 1 cons
app swap push cur (cdr) swap quote 2 cons
app cons app) swap quote + cons app.
На пятом этапе процедуры трансляции выполним результирующую последовательность инструкций категориальной абстрактной машины с означиванием в среде вычислений.
Создав таблицу с графами, соответствующими терму, коду и стеку КАМ, производим вычисления согласно инструкциям КАМ, полученным в предыдущем пункте до окончательного результата.
Последний пункт преобразований предлагается произвести самостоятельно в качестве упражнения.
Подводя итоги рассмотрения формальной системы категориальной комбинаторной логики и ее применения для реализации категориальной абстрактной машины на состояниях, принадлежащих пространству д.з.к., можно сделать следующие выводы (в сопоставлении КАМ с виртуальной машиной технологической платформы Microsoft .NET).
Во-первых, как уже упоминалось ранее, схема трансляции в .NET явно содержит в своем составе абстрактную машину.
Во-вторых, абстрактная машина .NET транслирует исходный текст на языке программирования в высокоуровневый ассемблер (известный под названием Microsoft Intermediate Language, или MSIL), который во многом подобен коду категориальной абстрактной машины.
В-третьих, виртуальная машина .NET способна осуществлять трансляцию из широкого спектра языков программирования, в том числе, в отличие от категориальной абстрактной машины, и для императивных языков (C++, C# и целого ряда других языков программирования).
В-четвертых, виртуальная машина .NET, как и категориальная абстрактная машина, отличается высокой аппаратной совместимостью, поскольку реализует целый ряд механизмов, обеспечивающих безопасную схему вычислений.
Наконец, в-пятых, отметим, что виртуальная машина .NET лучше адаптирована для объектно-ориентированных языков программирования (в том числе для языка C#, который будет рассматриваться в ходе изложения курса).