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

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


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

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

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

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

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

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

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

Формальная система с д.з.к. должна удовлетворять следующим условиям:

  1. определена функция тождества, или тождественное преобразование (имеющее в комбинаторной логике аналог в форме комбинатора тождества I);

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

Заметим, что выполнение перечисленных условий необходимо для того, чтобы обеспечить принадлежность состояний категориальной абстрактной машины пространству д.з.к..

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



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






Forekc.ru
Рефераты, дипломы, курсовые, выпускные и квалификационные работы, диссертации, учебники, учебные пособия, лекции, методические пособия и рекомендации, программы и курсы обучения, публикации из профильных изданий