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

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

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>>),’+>

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

Дата добавления: 2014-01-11