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