Error: Incorrect password!
Шпаргалка по λ-исчислению (практика) — codedot — Сохраненная запись в кэше | Ljrate.ru
2012/03/26 17:48:10
Шпаргалка по нужной для практики теории готова, поэтому теперь попробуем сделать выжимку из практической части монографии Барендрегта по λ-исчислению. Речь пойдет о комбинаторной логике, теореме о неподвижной точке и синтаксическом сахаре.

Множество комбинаторов Ξ порождает наименьшее множество Ξ+ следующим образом:

Ξ ⊆ Ξ+;
M, N ∈ Ξ+ ⇒ Μ Ν ∈ Ξ+.

Множество Ξ называется базисом, если ∀M ∈ Λ0: ∃N ∈ Ξ+: M = N.

Произвольную абстракцию можно смоделировать с помощью S и K:

S ≣ λx.λy.λz.x z (y z);
K ≣ λx.λy.x;
I ≣ λx.x = S K K;
x ∉ FV(P) ⇒ λx.P = K P;
λx.P Q = S (λx.P) (λx.Q).

Следовательно, комбинаторы K и S задают базис. Произвольный комбинатор M зачастую описывают не в виде λ-выражения, а с помощью аксиом. Например, формальная система комбинаторной логики CL определяется двумя аксиомами:

K P Q = P;
S P Q R = P R (Q R).

Существуют и одноточечные базисы: один из таких базисов задает комбинатор

X ≣ λx.x K S K.

Действительно, легко проверить, что X X X = K и X (X X) = S.

Стандартными комбинаторами считаются не только составляющие некоторый базис для комбинаторной логики, но и многие другие полезные λ-выражения. Одним из первых примеров обычно дают простейший комбинатор, не имеющий нормальной формы:

Ω ≣ ω ω, где ω ≣ λx.x x.

Далее, истинностные значения T ≣ K и F ≣ λx.I позволяют обозначить выражением B M N операцию «если B, то M, иначе N». Действительно: если B = T, то выражение равно M; если B = F, то выражение равно N. Если B отличен от T и F, то результат может быть произвольным.

Как и в теории множеств, в λ-исчислении можно определить упорядоченные пары:

[M, N] ≣ λx.x M N, [M, N] T ↠ M, [M, N] F ↠ N.

Цифровая система — это последовательность комбинаторов ⎡0⎤, ⎡1⎤, ⎡2⎤…, для которой существуют следование S+ и проверка на нуль Zero:

S+ ⎡n⎤ = ⎡n + 1⎤;
Zero ⎡0⎤ = T;
Zero ⎡n + 1⎤ = F.

В стандартной цифровой системе выбраны

⎡0⎤ ≣ I;
S+ ≣ λx.[F, x];
Zero ≣ λx.x T.

Цифровая система называется адекватной, если относительно нее определимы все рекурсивные функции. Для выполнения этого свойства достаточно, чтобы нашлась функция предшествования P-. Для стандартной цифровой системы это комбинатор

P- ≣ λx.x F.

Одним из основных результатов λ-исчисления является теорема о неподвижной точке: для любого F существует X, такой, что F X = X. Ее доказательство конструктивно. Пусть W = λx. F (x x) и X = W W. Тогда имеем X = W W = (λx. F (x x)) W = F (W W) = F X, что и требовалось доказать. Читатель, возможно, заметил одну особенность в доказательстве этой теоремы. Чтобы установить, что F X = X, мы начинаем с терма X и редуцируем его к F X, а не наоборот.

Комбинатор неподвижной точки — это терм M, такой, что для любого F имеет место M F = F (M F), то есть M F - неподвижная точка для F. Примером комбинатора неподвижной точки чаще всего служит

Y ≣ λf. (λx. f (x x)) (λx. f (x x)).

Комбинатор неподвижной точки позволяет решать задачи следующего типа: построить F, такой, что

F x y = F y x F.

Действительно, решение оказывается несложным:

F x y = F y x F следует из равенства F = λx y. F y x F,

а оно вытекает из F = (λf x y. f y x f) F.

Теперь положим F = Y (λf x y. f y x f), и все в порядке.

В несколько измененном и дополненном виде определенный выше синтаксический сахар записан на эзотерическом языке программирования — предполагается, что программа вычисляет последнее выражение, не используя никаких операций, кроме абстракции и аппликации.
60 посетителей, 1 комментарий, 2 ссылки, за 24 часа