учебники, программирование, основы, введение в,

 

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

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

  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’}.
Для завершения описания процедуры функционирования категориальной абстрактной машины осталось описать динамику состояний КАМ.
Циклом работы КАМ назовем множество всевозможных изменений (динамики) ее состояний.
Цикл работы КАМ удобно представить в виде таблицы.
Поскольку в данной таблице рассмотрены все возможные инструкции категориальной абстрактной машины, можно сделать вывод о том, что формализация проведена в полном объеме.


Таблица 11.1. Отображение выражений категориальной комбинаторной логики в "инструкции" категориальной абстрактной машины

№ п/п

Терм ККЛ

Инструкция КАМ

Пояснени

1

Fst

car

Голова списка (взятие первого элемента упорядоченной пары)

2

Snd

cdr

Хвост списка (взятие второго элемента упорядоченной пары)

3

push

Значение терма помещается на вершину стека

4

swap

Значения терма и вершины стека меняются местами

5

cons

Вершина стека помещается в голову терма; стек «проталкивается»

6

ε

app

Аппликация

7

Λ

cur

Каррирование

8

quote

Цитирование

Таблица 11.2. Состояния КАМ

№ п/п

Код элемента состояния КАМ

Обозначение элемента состояния КАМ

Пояснение

1

T

Терм

Среда вычислений (первоначально пуста)

2

C

Код

«Программа» на «языке» КАМ

3

S

Стек

Модель оперативной памяти компьютера

Таблица 11.3. Динамика состояний КАМ

Старое состояние КАМ

Новое состояние КАМ

Терм

Код

Стек

Терм

Код

Стек

t

push.C

S

t

С

t.S

t

swap.C

s.S

s

C

t.S

t

cons.C

s.S

[s, t]

C

S

S

(cur C).C1

S

C:s

C

S

S

(quote c).C

S

c

C

S

S

C

s

S

car.C

[s, t]

[s,t]

cdr.C

S

t

C

S

S

C@C1

[s, t]

S

app.C1

[C:s, t]

Проиллюстрируем процедуру трансляции программы на языке функционального программирования в последовательность инструкций категориальной абстрактной машины с последующим вычислением результирующего значения в среде на примере.
Рассмотрим текст следующей программы на языке функционального программирования 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#, который будет рассматриваться в ходе изложения курса).

 

 
На главную | Содержание | < Назад....Вперёд >
С вопросами и предложениями можно обращаться по nicivas@bk.ru. 2013 г.Яндекс.Метрика