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

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

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

Редукция

(α) λ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 → C    ├    A → C.

Теорема Чёрча-Россера

Теорема. Если A = B, то существует такой терм C, что A → C и B → C.
Другая формулировка теоремы:
Теорема. Если D → A и D → B, то существует такой терм C, что A → C и B → C.

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

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