ЮрИнфоР >>> Электронная библиотека >>>
МОДЕЛИ ЛАМБДА-ИСЧИСЛЕНИЯ
С.В. Косиков
НОУ «Институт актуального образования «Юринфор-МГУ»
г. Москва
Публикуется в сокращении
Модели из термов
Определение. Пусть T – некоторая ламбда-теория.(i) M =T N ⇔T ├ M = N
[M]T = {N из Λ| M =T N}
Λ/ T = {[M]T | M из Λ}
[M]T ·[N]T = [MN]T ; эта операция корректно определена.
(ii) Модель из открытых термов для теории T есть комбинаторная алгебра
M (T) = <Λ/ T, · , [K]T , [S]T >.
(iii) Модель из замкнутых термов для теории T есть комбинаторная алгебра
M0 (T) = <Λ0 / T, · , [K]0T , [S]0T >.
Теорема. Пусть T – ламбда-теория.
(i) M0 (T) – ламбда-алгебра.
(ii) M (T) – ламбда-модель.
Замечание. В общем случае неверно, что M0 (T) – ламбда-модель.
Теорема (Барендрегт - Койманс). Любая ламбда-алгебра может быть вложена в ламбда-модель.
Никакая часть содержащегося здесь текста ни в каких целях не может быть воспроизведена в какой бы то ни было форме и какими бы то ни было средствами, будь то электронные или механические, если на то нет письменного разрешения АО "Центр ЮрИнфоР".
(Размещена 12 января 2010 г.)
