Введение в теорию программирования. Функциональный подход
и операции образования упорядоченной пары,
(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) характеризует цитирование.
Заметим, что данный перечень характеристических соотношений категориальной комбинаторной логики является базисным и получен с учетом устранения избыточных комбинаторов из рассматриваемой формальной системы.
Завершив этап предварительной подготовки необходимого набора соотношений, перейдем непосредственно к реализации поставленной задачи формализации процедуры трансляции функциональной программы.
Схема процедуры трансляции текста программы на языке функционального программирования в результирующую последовательность инструкций категориальной абстрактной машины является многоэтапной и включает следующие стадии:
преобразование текста программы на языке функционального программирования в соответствующее выражение ламбда-исчисления;- преобразование полученного выражения ламбда-исчисления в так называемый (промежуточный) код де Брейна (de Brujin);
преобразование полученного кода де Брейна в терм категориальной комбинаторной логики;- преобразование полученного терма категориальной комбинаторной логики в последовательность инструкций категориальной абстрактной машины;
- выполнение результирующей последовательности инструкций категориальной абстрактной машины с означиванием в среде вычислений.
Подчеркнем, что собственно последовательность инструкций категориальной абстрактной машины (или, сокращенно, КАМ-код) еще не является конечной целью нашего исследования.
Итогом процедуры трансляции является выполнение результирующей последовательности инструкций категориальной абстрактной машины с означиванием в зависимости от среды вычислений.
