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



             

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


(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. выполнение результирующей последовательности инструкций категориальной абстрактной машины с означиванием в среде вычислений.

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

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




Содержание  Назад  Вперед