Введение в теорию программирования. Функциональный подход
         

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


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

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

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

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

  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 ‘ ??.


Содержание раздела