ЮрИнфоР >>> Электронная библиотека >>>
МОДЕЛИ ЛАМБДА-ИСЧИСЛЕНИЯ
С.В. Косиков
НОУ «Институт актуального образования «Юринфор-МГУ»
г. Москва
Публикуется в сокращении
Ламбда-модели
Слабая экстенсиональность
Определение. Пусть M – комбинаторная алгебра. Она называется слабо экстенсиональной, еслиM |= для любого x (A = B) ⇒λx. A = λx. B
для любых A, B из T(M).
Ламбда-модели
Определение.(i) 1 = S (KI)
(ii) Ламбда-модель – это ламбда-алгебра, в которой выполняется следующая аксиома Майера-Скотта:
для любого x (a x = b x) ⇒1 a = 1 b.
Лемма. Пусть M – комбинаторная алгебра. Тогда в ней
(i) 1ab = ab.
Если, кроме того, M есть ламбда-алгебра, то
(ii) 1 = λxy. xy, и, следовательно, 1a = λy. ay;
(iii) 1(λx. A) = λx. A, для всех A из T(M);
(iv) 11 = 1.
Предложение. M есть ламбда-модель ⇔ M – слабо экстенсиональная ламбда-алгебра.
Предложение. Пусть M есть ламбда-алгебра. Тогда M экстенсиональна ⇔ M слабо экстенсиональная и удовлетворяет равенству I = 1.
Никакая часть содержащегося здесь текста ни в каких целях не может быть воспроизведена в какой бы то ни было форме и какими бы то ни было средствами, будь то электронные или механические, если на то нет письменного разрешения АО "Центр ЮрИнфоР".
(Размещена 12 января 2010 г.)
