Шпаргалка по λ-исчислению (практика)
Mar. 26th, 2012 04:48 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
codedotШпаргалка по нужной для практики теории готова, поэтому теперь попробуем сделать выжимку из практической части монографии Барендрегта по λ-исчислению. Речь пойдет о комбинаторной логике, теореме о неподвижной точке и синтаксическом сахаре.
Множество комбинаторов Ξ порождает наименьшее множество Ξ+ как замыкание по аппликации:
Ξ ⊆ Ξ+;
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 ≣ (λ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), и все в порядке.
В несколько измененном и дополненном виде определенный выше синтаксический сахар записан на эзотерическом языке программирования — предполагается, что программа вычисляет последнее выражение, не используя никаких операций, кроме абстракции и аппликации.
Множество комбинаторов Ξ порождает наименьшее множество Ξ+ как замыкание по аппликации:
Ξ ⊆ Ξ+;
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 ≣ (λ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), и все в порядке.
В несколько измененном и дополненном виде определенный выше синтаксический сахар записан на эзотерическом языке программирования — предполагается, что программа вычисляет последнее выражение, не используя никаких операций, кроме абстракции и аппликации.
