Кодирование по де Брейну

Компиляция в коды абстрактных машин.

ФЯ→λ-выражение→код де Брейна→категориальная комбинаторная логика →

→ код категориальных абстрактных машин (КАМ-код)

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

Пусть есть λ-выражение S и связное вхождение в него переменной х. Построим дерево разбора выражения S.

Глубиной связывания вхождения переменной х называется число λ-узлов дерева разбора между вхождением переменной и ее связыванием.

Пример.

λх.+х1 глубина связывания х равна 0.

λх.λу.+ху глубина связывания х равна 1, глубина связывания у равна 0.

λх. +х((λу.+ух)2)

^{0↑ 0↑1↑}

Обозначение:

1. Заменим имена переменных на их глубину связывания, такие числа называются числами де Брейна.

Глубина связывания переменных обозначается n- число де Брейна. n.

x_i→ n

2. const c →’c

3. MN = S(M,N)-аппликация

4. λ.M = Λ(М) - λ-абстракция.

Примеры кодирования по де Брейну:

1. λх.λу.((+х)у) →Λ(Λ(S(S(’+,1),0)))

^{@ @↑}

2. (λх.+((λх.x)3)x)4→S(Λ(S(S(’+,S(Λ(0),’3)), 0)),’4).

Вычисления по де Брейну: преобразования в соответствии с формализмами Де Брейна.

Замена: λ ~ Λ(), аппликация ~ S(,), n ~ n.

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

1)Пустая среда () - есть среда,

2)если ρ - среда, х - переменная, то пара (ρ,х) есть среда

3) других сред нет.

Для хранения переменных используется среда.

Есть два способа получить значение переменной из среды:

- по имени

- по номеру (Fst,Snd).

По соглашению - среда конечна.

Среда наращивается справа. Самая внешняя переменная имеет 0-е значение числа

Де Брейна.

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

Среда - упорядоченное множество пар “ переменная, значение”.

Кодирование в среде (ρ):

Шаг кодирования

_const

[c] ρ→c - константа, вычисленная в среде равна самой себе => 0(ρ, d) = d

^среда

_{↓переменная} n+1(ρ,d) = nρ

[x]ρ→ ρ(x) - х – переменная, ρ(x) - ее значение в среде ρ.

[(MN)] ρ→(([M] ρ)([N] ρ))

[λх.М]ρ→[M](ρ,x)

^{новая среда}

Предполагается, что если в выражении есть свободные переменные, то они

явным образом находятся в среде.

Алгоритм преобразования λ-выражений по де Брейну.

1. Избавляемся от свободных переменных путем их абстрагирования в поряд-

ке, заданном средой.

2. Рекурсивно выполняем шаг алгоритма кодирования λ-терма в среде.

3. Отбрасываем символы λ, приписанные на первом шаге.

Пример.

λх.+ху ((),у) - среда.

Шаги:

1. λу.λх.+ху

2. Λ(Λ(S(S(’+, 0), 1)))

3. Λ(S(S(’+, 0), 1))

λх.+ху (((),у),z) - среда

λz.λх.+ху

λу.λz.λх.+ху

λ.λ.λ.+ 02

λ.+ 02

Λ(S(S(’+, 0), 2))

Семантические равенства для кодов де Брейна:

0 (х,у) = у

n+1 (х,у) = n х

(’x)y = x

S(x,y)z = xz(yz)

Λ(x)yz = x(y,z) - каррирование, т.е. преобразование функции от двух аргументов в функцию от первого аргумента, задающую функцию от второго аргумента

^.

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

Пара из терма Де Брейна и среды, в которой он рассматривается, называется кодом

Де Брейна.

Вычислять мы можем только код Де Брейна. Вычисление терма в отрыве от среды невозможно.

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

Композицией функций х и у - называется функция (х○у): (х○у)z = x(yz)

Соглашение о композиции: А○В = ВА. Если ”+” - машинная команда вида Λ(+○ Snd)

(из ’M= Λ(+○ Snd)) ^{↑аппликация}

Уравнения, описывающие семантику, называются семантическими:

Семантические равенства с учетом среды: Без учета среды:

||0!||(ρ,d) = d ||0!|| = 0!

||(n+1)!||(ρ,d) = ||n!|| ρ ||n|| = n!

||c|| ρ = c ||c|| = ’c

||MN|| ρ = ||M|| ρ(||N|| ρ) ||MN|| = App○<||M||, ||N||>

||λx.M|| ρ = ||M||(ρ,x) ||λ.M|| = Λ||M||

Snd○Fstⁿ = n! App○<A, B> = S(A,B)

Вычисления с использованием семантических равенств:

Пусть Q - l-терм:

1) применение к Q формализма Де Брейна;

2) преобразование правой части равенства с помощью семантических равенств

После того как терм Q приведен к окончательному виду по Де Брейну, его с помощью семантических равенств вычисляют путем приложения к среде (с помощью категориальных операторов).

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