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



             

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


Пожалуй, апогеем развития современных вычислительных сред является изучаемая в курсе технологическая платформа 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 ‘ ??.




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