ЮрИнфоР >>> Электронная библиотека >>>
МОДЕЛИ ЛАМБДА-ИСЧИСЛЕНИЯ
С.В. Косиков
НОУ «Институт актуального образования «Юринфор-МГУ»
г. Москва
Публикуется в сокращении
Ламбда-алгебры
Ламбда-термы над комбинаторной алгеброй
Так как в комбинаторной алгебре M можно смоделировать абстракцию с помощью k и s, оказывается возможным интерпретировать в M ламбда-термы.Обозначение. Пусть С – некоторое множество констант. Обозначим через Λ(C) множество ламбда-термов, возможно, содержащих константы из C. Если M= (X, ·, k, s) – аппликативная структура, то Λ(M) есть по определению Λ(X).
Обозначение. Пусть M– комбинаторная алгебра.
(i) Введём отображения
CL : Λ(M) →T (M),
λ: T (M) →Λ(M),
используя обозначения CL(M) = MCL, λ(A) = Aλ.
Отображение CL:
xCL = x
cCL = c
(MN)CL = MCL NCL
(λx.M)CL = λ* x.MCL
Отображение λ:
xλ = x
Kλ = λxy . x
Sλ = λxyz . xz (yz)
cλ = c
(MN)λ = Mλ Nλ
(ii) Для M, N из Λ(M) полагаем по определению
[M]Mρ = [MCL]Mρ
M, ρ |= M = N ⇔[M]ρ = [N]ρ
M |= M = N ⇔M, ρ |= M = N для всех ρ
Ламбда-алгебры
Определение. Комбинаторная алгебра M называется λ-алгеброй, еслиλ ├ Aλ = Bλ ⇒ M |= A = B
для любых A, B из T(M)
Лемма (признак ламбда-алгебры). Пусть M – комбинаторная алгебра. M является λ-алгеброй тогда и только тогда, когда для всех M, N из Λ(M):
(i) λ ├ M = N ⇒ M |= M = N
(ii) M |= Kλ, CL = K, M |= Sλ, CL = S.
Никакая часть содержащегося здесь текста ни в каких целях не может быть воспроизведена в какой бы то ни было форме и какими бы то ни было средствами, будь то электронные или механические, если на то нет письменного разрешения АО "Центр ЮрИнфоР".
(Размещена 12 января 2010 г.)
