ЮрИнфоР >>> Электронная библиотека >>>

МОДЕЛИ ЛАМБДА-ИСЧИСЛЕНИЯ

С.В. Косиков
НОУ «Институт актуального образования «Юринфор-МГУ»
г. Москва

Публикуется в сокращении

Next

Конверсия

Аппликативные термы

(i) x - переменная    ├    x - терм.
(ii) A, B - термы    ├    (AB) - терм.
(iii) Других термов нет.


λ - термы

(i) x - переменная    ├    x - терм.
(ii) 1. A, B - термы    ├    (AB) - терм.
     2. A - терм    ├    (λx.A) - терм.
(iii) Других термов нет.
Множество λ-термов обозначим через Λ, множество замкнутых λ- термов – через Λ0.

Конверсия

(α) λx.A = λy.(A [y / x]).
(β) (λx.A) B = A [B / x].
(μ) A = B    ├    CA = CB.
(ν) A = B    ├    AC = BC.
(ξ) A = B    ├    λx.A = λx.B.
(ρ) A = A.
(σ) A = B    ├    B = A.
(τ) A = B, B = C    ├    A = C.

Экстенсиональность

(η) λx.Ax = A.

Next

Никакая часть содержащегося здесь текста ни в каких целях не может быть воспроизведена в какой бы то ни было форме и какими бы то ни было средствами, будь то электронные или механические, если на то нет письменного разрешения АО "Центр ЮрИнфоР".

(Размещена 12 января 2010 г.)