Категориальная комбинаторная логика (ККЛ).

Декартово замкнутая категория подразумевает наличие:

1) аппликации арр,

2) каррирования (Λ),

3) точечной пары (х,у).

Так как есть пара, то есть и функции доступа к элементам:

Fst(x,y) = x

Snd(x,y) = y

 

ККЛ представляется следующей совокупностью комбинаторов:

App - аппликация,

Λ - абстрактор,

<, > - комбинационные пары,

(,) - совокупность,

○ - композиция.

Заявим, что 0 = Snd                         D=λr.rxy

                N = Snd○Fst^{n                          ↑ комбинатор точечной пары.}

 

(ass): (x○y)z = x(yz) – композиция

(fst): Fst(x,y) = x     Fst = CIK

(snd): Snd(x,y) = y    Snd = CI(KI)

(dpair): <x,y>z = (xz,yz)

          Для вычисления композиции в среде предлагается ввести:

                [(M,N)] ρ = <[M],[N]> ρ

(dΛ): Λ(x)yz = x(yz) - операция каррирования.

(app): App(x,y) = xy S = CIS

(quote): (’x)y = x       λxy.x 

(ac): App(Λ(x)y,z) = x(yz) # App(Λ(x)y,z) = Λ(x)yz = x(yz)#

Пример

      Λ(x○Snd)yz = (x○Snd)(y,z) = xz

      (’x)yz = xz

          > quote = Λ(x○Snd) - правило quote является избыточным.

 

Пример. (из λ-исчисления в код Де Брейна).

(λх.х4((λх.х)3))+

(λ.0 4 ((λ. 0)3))+

S(Λ (S(S(0,’4),S(Λ (0),’3))),’+)

           ^{↑Snd             ↑Snd}

_{1 2 3 4   4                 3 2  1}

     

S(x,y) = App○<x,y>

0 заменяем на Snd и получаем выражение:

App○< Λ (App○< App○< Snd,’4>, App○< Λ(Snd),’3>>),’+>

На основе ККЛ можно построить абстрактную машину.

 

Общие свойства абстрактных машин.

Определение.

Абстрактная машина (АМ) - способ формализованного задания алгоритма для математически строго описываемых языков.

(АМ) - характеризуется множеством регистров, множеством состояний регистров и правилами перехода от состояния к состоянию.

 

                                         

                                                                                     два регистра памяти

                                                                                      быстрого доступа

 

          Три стека

Правила перехода из состояния в состояние задаются кодом АМ.

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

Структура [исходное состояние] => Структура [итоговое состояние]

<Новое состояние>=<Функция перехода>(старое состояние).

Функция, описывающая действие оператора кода АМ, имеет в качестве своих аргументов регистры этой машины с содержащимися в них данными, при этом переход машины из

одного состояния в другое соответствует шагу редукции дерева программы исходного языка.

Определение.

Верификация - способ проверки правильности программ на основе теоретических знаний.

 

Категориальная абстрактная машина (КАМ).

 

КАМ состоит из трех регистров: два стека (код и стек) и регистр терм.

                ^{Код               Стек}

                                                                     Терм

 

 

И элементы стека, и элементы терма - символьные выражения, в них могут размещаться структуры символьных данных.

В начале программа в виде кода содержится в стеке ''кода'', ''стек'' пуст.

В конце «код» пуст, в “ терме ” содержится результат. Правила перехода из состояния в состояние определяются набором инструкций машины.

Определение.

Состоянием машины называется тройка <T,C,S>, где T -терм как структурированное значение, например граф; C - код; S - стек или дамп (вспомогательная память).

Закон функционирования КАМ изменяет старую тройку на новую: <T, C, S>→<T^|,C^|,S^|>.

Входной язык КАМ: <,>;Fst; Snd; Λ; ’; (,); app

КАМ – это вариант КЛ, вовлекающий ДЗК, а также техническое устройство, вычисляющее значение выражений.

Средства КЛ имеют категориальный характер, т.е. в категориях используются композиции и тождества, в декартовых категориях дополнительно вводят произведение с использованием спаривания <, >, а также проекции Snd и Fst. Декартовы замкнутые категории дополнительно содержат каррирование Λ, апплицирование и средства экспонирования, т.е. средства построения функциональных правил. 

 

Цикл работы КАМ

1) Выбор категориального терма, построенного из комбинаторов.

2) Означивание этого терма производится путем его аппликации к среде. 

Начальное состояние			Конечное состояние
Терм	Код	Стек	Терм	Код	Стек
(S,t)	car:C	A	S	C	А
(S,t)	cdr:C	A	T	C	А
S	(quoteB)C	A	B	C	А
S	(cur C) C1	A	[C:S]	C1	А
([C:S], t)	app. C1	A	(S,t)	C:C1	А
T	cons C	S:A	(S,t)	C	А
S	push.C	A	S	C	S:A
T	swap.C	S:A	S	C	T:A

А - вектор содержимого стека,

 ”:” - разделитель,

[C:S] - совокупность.

В языке ДЗК (декартово замкнутые категории) использовано 8 символов, которым ставятся в соответствие инструкции КАМ:

 

Сar = Fst        - получает терм (s,t) и заменяет его на s.

Cdr = Snd      - получает терм (s,t) и заменяет его на t.

Quote = ’       - получает терм s и оставляет его без изменений

Cur = Λ         - замещает терм s на С:s, где C - код, инкапсулированный в Λ.

Cons = >        - строит совокупность из вершины стека и терма, заменяет терм на эту 

                         совокупность и проталкивает стек.

app = App     - получает терм (C:s,t), замещает его на (s,t), а оставшейся части кода

                         устанавливает префикс C.

swap =,        - меняет содержимое терма и вершины стека местами.

push = <       - берет терм и помещает его в вершину стека.

 

                 _{Стек                   Код}

А                                         С    Вместо рор используется пара из swap и cons.

                                                     

            

App○<x,y> Term

App(<x,y>Term)

Код: push,[x],swap,[y],cons,app

Пример КАМ кода: сложение 2 и 3

((+2)3) –это аппликация (+ к 2) →(+2) к 3

push push quote + swap quote 2 cons app swap quote 3 cons app

<<’+,’2>App,’3>App   

 

Оптимизация кода КАМ

 Два вида оптимизации:

переход к многоместным операциям, т.е. вместо функции “+”, которая будет брать аргументы по очереди, рассмотрим двуместный “+”.

а) App○< App○<’+,x>,y> = +<x,y>

б) Воспользуемся категориальным равенством для β-редукции.

  App○<Λ(х)○у, z> = x○<y,z>

       {(λx.y)z→[z/x]y – соответствующее категориальное равенство.}