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

· Stack - стек, т.е. последовательность атомарных ламбда-выражений (переменных и констант), а также ламбда-абстракций;

· Environment - среда, т.е. хранилище значений, которые связываются с переменными в ходе вычислений;

· Control - управление, т.е. последовательность "инструкций", управляющих работой SECD-машины;

· Dump - дамп, т.е. хранилище состояния SECD-машины (обычно пуст либо содержит прежнее состояние).

Именно перечисленная четверка элементов в полной мере характеризует состояние SECD-машины в произвольный момент вычислений.

Заметим, что именно SECD-машина стала прообразом для более поздних формализаций, на которых реализованы ML-машины, в частности категориальная абстрактная машина (КАМ).

Перейдем к обсуждению теоретического фундамента, на котором основана категориальная абстрактная машина, а конкретно, к формальной системе категориальной комбинаторной логики (ККЛ).

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

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

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

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

3. определена операция образования упорядоченной пары объектов < ., . >;

4. определена операция взятия первого элемента из упорядоченной пары объектов;

5. определена операция взятия второго элемента из упорядоченной пары объектов;

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

7. определена операция аппликации или применения функции к аргументу.

Проанализируем смысл сформулированных условий для категорий.

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

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

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

Заметим, что последняя операция называется каррированием, а обратная ей - декаррированием по имени основоположника комбинаторной логики Х. Карри (Haskell B. Curry).

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

Для реализации категориального расширения комбинаторной логики (известного также как категориальная комбинаторная логика, или, сокращенно, ККЛ), добавим к известным нам комбинаторам

(I) Ia = a;

(K) Кab = a;

(S) Sabc = ac(bc);

(B) Babc = a(bc);

(C) Cabc = acb

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

(D) D = лxy.[x,y] = лxyr.rxy;

(S) S = CIS;

(Л) Л = лx.(лz.x[y,z]);

(`) ` = K = лx.(лy.x).

Заметим, что характеристическое соотношение (D) представляет собой операцию образования упорядоченной пары, соотношение (Л) - каррирование, а соотношение (`), ранее известное нам как характеристика комбинатора-канцелятора K - операцию взятия первой проекции для упорядоченной пары элементов, которую можно также понимать как цитирование.

Продолжим построение формальной системы категориальной комбинаторной логики.

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

Введем одноместную функцию вычисления значения выражения для произвольного выражения, которую обозначим как || ||. Скажем, значение терма M в таком случае будет иметь вид || M ||.

Далее добавим бесконечное множество комбинаторов n! со следующей семантической характеристикой: ||n|| = n!.

Продолжим семантические равенства следующим соотношением, характеризующим значения констант: ||с|| = `с.

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

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

||M,N|| = S [||M||,||N||];

||лx.M|| = Л(M).

Продолжим построение формальной системы категориальной комбинаторной логики.

Заметим, что благодаря введению дополнительных комбинаторов

(D) D = лxy.[x,y] = лxyr.rxy;

(S) S = CIS;

(Л) Л = лx.(лz.x[y,z]);

(`) ` = K = лx.(лy.x)

перечисленные выше синтактико-семантические соотношения сводятся к чисто синтаксическим равенствам, которые имеют следующий вид:

0! [x,y] = y;

(n+1)! [x,y] = n!x;

S[x,y]z = xz(yz);Л(x)yz = x[y,z].

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

Продолжим построение формальной системы категориальной комбинаторной логики.

Для того чтобы формализация приняла более строгий и удобный вид, необходимо ввести в рассмотрение двухместный комбинатор образования пары, который определяется ламбда-выражением следующего вида: < ., . > = лt.[ . t, . t].

При этом комбинаторная характеристика вновь введенного комбинатора образования пары имеет следующий вид:

<f,g> = лt.лz.(ft)(gt) = лt.[ft,gt].

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

||M,N|| = <||[M]||,||[N]||>.

Продолжим построение формальной системы категориальной комбинаторной логики.

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

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

Fst = CIK = (n+1)!

Snd = CI(KI) = (0)!

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

Fst [x,y] = x;

Snd [x,y] = y;

<x,y> z = [xz,yz].

Последнее соотношение определяет связь между комбинатором образования упорядоченной пары и так называемой парой функций, т.е. такой функцией, которая в результате дает совокупность результатов своих функций-компонентов x:A>B и y:A>C в виде функции w:A>BxC.

Продолжим построение формальной системы категориальной комбинаторной логики.

Заметим, что введенная система комбинаторов Fst, Snd, (n+1)!, 0!, S, Л является избыточной.

Избыточность системы комбинаторов устраняется введением комбинатора композиции o = B, который принимается тождественно равным ранее определенному комбинатору композиции B.

Теперь явно введем комбинатор аппликации е.

Выведем соотношения, которые позволят устранить избыточность системы комбинаторов:

S(xyt) = xt(yt) = е[xt,yt] = (е o<x,y>)t.

Отсюда,

(i) S = лxy.(еo<x,y>).

Положим Fstn+1=FstoFstn, для n>1 и Fst1=Fst. Тогда получим, что

(ii) n!=SndoFstn, для n>0, а 0!=Snd.

Завершим построение формальной системы категориальной комбинаторной логики.

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

(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) устанавливает связь аппликации и композиции, соотношение (dpair) - спаривания и формирования совокупности, а соотношение (ac) - каррирования и апплицирования.

Напомним, что соотношения (fst) и (snd) характеризуют операции взятия первой и второй проекций для упорядоченной пары объектов, а (quote) - цитирование.

Приведенные соотношения (ass), (fst), (snd), (dpair), (ac) и (quote) адекватно, то есть полно и непротиворечиво, формализуют систему категориальной комбинаторной логики.

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

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

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

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

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

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

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 ` Ле.

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

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

При этом каждая инструкция категориальной абстрактной машины изменяет состояние КАМ, которое определяется значениями тройки {T, C, S}. Смысл состояний КАМ удобно представить в виде таблицы 11.2.

Таким образом, процесс работы КАМ сводится к смене состояний вида: {T, C, S} -> {T', C', S'}.

Для завершения описания процедуры функционирования категориальной абстрактной машины осталось описать динамику состояний КАМ.

Циклом работы КАМ назовем множество всевозможных изменений (динамики) ее состояний.

Цикл работы КАМ удобно представить в виде таблицы 11.3.

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

Таблица 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#, который будет рассматриваться в ходе изложения курса).

Лекция 13. Оптимизация вычислений и абстрактные машины

В лекции рассматриваются возможные направления и ключевые стратегии повышения вычислительной производительности программных систем. Значительное внимание уделяется моделированию этих направлений и стратегий путем внесения "конструктивных изменений" в инструкции и среду вычислений абстрактных машин, в частности, КАМ.

Проиллюстрируем особенности реализации наиболее существенных стратегий вычислений на примере КАМ.

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

Кроме того, как показывает практика, именно КАМ больше всего подходит для использования в качестве виртуальной машины при реализации современных языков функционального программирования (в частности, языка CaML), в том числе с объектными расширениями (в частности, языка Object CaML).

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

Перечислим наиболее существенные (с учетом целей и задач нашего курса) из этих недостатков.

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

Другим существенным недостатком КАМ является отсутствие поддержки рекурсивных вычислений, которое, как мы увидим впоследствии, устраняется посредством модификации среды вычислений.

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

Выявив и оценив недостатки "классической" реализации категориальной абстрактной машины, наметим возможные направления оптимизации программ на языке инструкций КАМ.

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

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

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

Наконец, следует рассмотреть вопрос о реализации на основе категориальной абстрактной машины поддержки вычислений по необходимости, иначе называемых "ленивыми" (lazy).

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

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

Заменим "встроенные" в систему команд категориальной абстрактной машины одноместные функции на двухместные.

В частности, в целях экономии времени, рассуждая без ограничения общности, приведем пример записи двухместной функции сложения:

+<x,y> = еo<еo<'+,x>,y>.

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

еo<Л(x)oy,z> = xo<y,z>,

которое находится в полном соответствии с правилами редукции, принятыми в формальной системе категориальной комбинаторной логики, на основе которой построена КАМ.

Продолжим обсуждение перехода к многоместным операциям в языке программирования категориальной абстрактной машины. Пересмотрим цикл работы (схему смены состояний) категориальной абстрактной машины, расширив пространство состояний КАМ дополнительными инструкциями, которые, по аналогии с основными командами КАМ, представим в форме таблицы 12.1.

Таблица 12.1. Дополнительные инструкции пространства состояний КАМ

Старое состояние КАМ	Новое состояние КАМ
Терм	Код	Стек	Терм	Код	Стек
true	if abc	sm	S	a c	m
false	if abc	sm	S	b c	m
(a,b)	add c	S	{a+b}	C	S
(a,b)	eq c	S	true/false	C	S

Как видно из приведенной таблицы, пространство состояний категориальной абстрактной машины расширено посредством введения операций сравнения if, проверки условия eq, а также сложения add. Проиллюстрируем практическую эффективность программного кода усовершенствованной категориальной абстрактной машины следующим примером. Рассмотрим программу категориальной абстрактной машины, вычисляющую сумму целых чисел 2 и 3 в "классической" версии "языка программирования" КАМ:

push cur (push push cdr swap quote 2 cons app swap push cur (cdr) swap quote 3 cons app cons app) swap quote + cons app.

"Запрограммируем" ту же задачу в усовершенствованной версии КАМ:

push quote 2 swap quote 3 cons add.

Как видно, объем программы сократился более чем втрое.

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

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

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

Таблица 12.2. Дополнительные инструкции КАМ для реализации рекурсивных вычислений

Старое состояние КАМ	Новое состояние КАМ
Терм	Код	Стек	Терм	Код	Стек
T	dum c	sm	$Y	C	S
[a:b]	wind c	(t$Y)S	(t.[a:b])	C	S

Как видно из приведенной таблицы, пространство состояний категориальной абстрактной машины расширено посредством введения операций wind и dum для обработки рекурсивных объектов.

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

При вычислении с вызовом по значению (call-by-value) все выражения должны быть означены до вычисления операции аппликации.

При вычислении с вызовом по имени (call-by-name) до вычисления операции аппликации необходима подстановка термов вместо всех вхождений формальных параметров перед означиванием. Именно эта стратегия лежит в основе "ленивых" (lazy), "отложенных" (delayed) или "замороженных" (frozen) вычислений, которые принципиально необходимы для обработки потенциально бесконечных структур данных.

Наконец, при вычислении с вызовом по необходимости (call-by-need) ранее вычисленные значения аргументов сохраняются в памяти компьютера только в том случае, если необходимо их повторное использование.

Чтобы устранить сложности с поддержкой категориальной абстрактной машиной "ленивых" вычислений, пересмотрим цикл работы КАМ, расширив пространство состояний дополнительными инструкциями для "замораживания" (freeze) и "размораживания" (unfreeze), которые представим в форме таблицы 12.3.

Таблица 12.3. Дополнительные инструкции КАМ для реализации "ленивых" вычислений

Старое состояние КАМ	Новое состояние КАМ
Терм	Код	Стек	Терм	Код	Стек
s	{freeze c}.C1	S	C.s	C1	S
C.s	unfreeze.C	S	s	C	S
s	unfreeze.C	S	s	C	S

Сформулируем ряд теорем, известных по именам их авторов как теоремы Черча-Россера и позволяющих установить особенности различных вычислительных стратегий, а также взаимосвязей между ними.

Заметим, что возможность "ленивого" связывания переменных с их значениями в языках функционального программирования вытекает из формулировки теорем Черча-Россера.

Поскольку доказательство теорем Черча-Россера выходит за рамки настоящего курса, ограничимся приведением формулировок теорем как таковых.

Теорема Черча-Россера

Пусть E1 и E2 суть ламбда-выражения, причем справедливо соотношение: E1 = E2.

Тогда существует ламбда-выражение E такое, что выполнены следующие условия: во-первых, E1 = E, и, во-вторых, E2 = E.

Заметим, что символ "=" в формулировке теоремы понимается в смысле отношения конвертируемости.

Теорема Черча-Россера (1)

Если в языке вызовы по имени и по значению приводят к определенному результату, то это один и тот же результат.

Теорема Черча-Россера (2)

Если вычисление значения выражения приводит к определенному результату, то к нему всегда приводит вызов по имени и не всегда - по значению.

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

Наиболее очевидным, исходя из специфики курса, представляется подход, при котором пересматривается цикл работы категориальной абстрактной машины, причем пространство состояний расширяется дополнительными инструкциями для "замораживания" (freeze) и "размораживания" (unfreeze).

Напомним, что ни SECD-машина П. Лендина, ни категориальная абстрактная машина редукция графов в "классическом" представлении не обладают способностью поддержки реализации механизма отложенного означивания переменных.

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

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

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

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

Во-первых, необходимо отметить, что в рамках рассматриваемой инструментально-технологической платформы Microsoft NET используется виртуальная машина с универсальным высокоуровневым ассемблером (известным под названием Microsoft Intermediate Language, или, сокращенно, MSIL), принципиально подобная КАМ. Абстрактная машина NET транслирует исходный текст на языке программирования в код MSIL, который в значительной степени подобен КАМ-коду.

Во-вторых, виртуальная машина инструментально-технологической платформы Microsoft NET является достаточно универсальным решением и предусматривает такие важнейшие механизмы поддержки проектирования и реализации языков программирования, как централизованная "сборка мусора", обработка ошибок и исключительных ситуаций. Кроме того, виртуальная машина NET, как и категориальная абстрактная машина, отличается высокой аппаратной совместимостью, поскольку реализует целый ряд механизмов, обеспечивающих безопасную схему вычислений.

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

В-четвертых, виртуальная машина NET обеспечивает поддержку универсальной среды вычислений с широким спектром унифицированных предопределенных типов и структур данных.

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

Прежде всего, нами была рассмотрена история развития языков программирования, а также построен вариант классификации современных подходов к программированию.

Затем было дано представление важнейших математических формальных систем, которые составляют теоретическое основание современных подходов к программированию и, прежде всего, функционального подхода. В частности, были рассмотрены исчисление ламбда-конверсий, комбинаторная логика, а также теория категорий и теория вычислений Д. Скотта.

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

Кроме того, было исследовано интуитивно ясное понятие типа, изучены основы теории типов и типизации в языках программирования.

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

Еще одним пунктом исследований стали важнейшие аспекты реализации языков программирования, включая схемы трансляции в промежуточнные коды для виртуальных машин SECD и КАМ.

Наконец, мы провели сравнительное исследование различных стратегий вычислений и оптимизации кода.

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

В связи с этим в ходе дальнейшего исследования планируется систематическое изучение следующих вопросов:

1. математическое обоснование объектного подхода к программированию (на примере языка программирования C#);

2. компонентное проектирование интегрированных гетерогенных программных систем (на примере языков функционального программирования SML и объектно-ориентированного программирования C#);

3. теория и практика разработки событийно управляемых приложений;

4. сравнительное исследование функционального и объектно-ориентированного подходов к программированию.

Дальнейшие исследования, согласно практике, сложившейся на протяжении первой части курса, будут проводиться синтетически по направлениям теоретического обоснования программирования на основе современных формальных систем computer science и современной практики проектирования и реализации программного обеспечения на основе универсальной и прогрессивной программно-инструментальной платформы Microsoft NET.

Учебники к курсу

1. Зыков С.В. Введение в теорию программирования

2. Интернет-университет информационных технологий - ИНТУИТ.ру, 2004

3. Городняя Л.В. Основы функционального программирования

4. Интернет-университет информационных технологий - ИНТУИТ.ру, 2004

5. Непейвода Н.Н. Стили и методы программирования

6. Интернет-университет информационных технологий - ИНТУИТ.ру, 2005

Размещено на Allbest.ru