Шпаргалка по λ-исчислению (теория)

История λ-исчисления уходит в начало прошлого века. Этимология названия данного раздела математической логики, который служит основой для «computer science», следующая. Сам значек «λ» используется для одной из двух основных конструкций в созданной Черчем системе — абстракции. Оказывается, что выбор обозначения абстракции не был совершенно случайным, а сделан в противопоставление другой более ранней конструкции, которую использовали Whitehead и Russell и обозначали как «xˆ». Для новой конструкции, чтобы отличать ее от прежней, Черч заменил обозначение сначала на «∧x», а затем — на «λx», очевидно, интерпретировав первый символ как заглавную букву «Λ», для упрощения набора.

Опишем кратко систему λβη, то есть классическое бестиповое экстенсиональное λ-исчисление, вывернув наизнанку монографию Барендрегта.

Множество λ-выражений Λ строится индуктивно из переменных

x, y, z… ∈ Λ

с помощью абстракций

M ∈ Λ ⇒ λx.M ∈ Λ

и аппликаций

M, N ∈ Λ ⇒ M N ∈ Λ,

при этом аппликация лево-ассоциативна:

(M) ≣ M, M N P ≣ (M N) P.

Рефлексивное транзитивное отношение Μ ⊂ N означает, что M является подвыражением выражения N:

M ⊂ M ⊂ λx.M;
M ⊂ M N ⊃ N;
M ⊂ N ∧ N ⊂ P ⇒ M ⊂ P.

FV(M) — это множество свободных переменных в выражении M:

FV(x) ≣ {x};
FV(λx.M) ≣ FV(M) ∖ {x};
FV(M N) ≣ FV(M) ∪ FV(N).

Переменные, которые не являются свободными, называются связанными и могут быть заменены другой переменной (такое преобразование называют α-конверсией):

y ∉ FV(M) ⇒ λx.M ≣ λy.M[x := y], где M[x := N] — результат подстановки:

x[x := P] ≣ P;
y[x := P] ≣ y;
(λx.M)[x := P] ≣ λx.M;
(λy.M)[x := P] ≣ λy.M[x := P];
(M N)[x := P] ≣ M[x := P] N[x := P].

В четвертом пункте не нужно специально оговаривать условие «x ≢ y и y ∉ FV(P)», так как оно выполняется в силу соглашения о переменных: если в определенном математическом контексте встречаются термы M₁,…, M_n, то подразумевается, что связанные переменные в них выбраны так, чтобы они были отличны от свободных переменных.

Если множество FV(M) пусто, то M называют комбинатором. Множество всех комбинаторов обозначают Λ₀:

Λ₀ ≣ {M ∈ Λ | FV(M) = ∅}.

Следующие отношения β, η и βη являются редукциями:

β ≣ {((λx.M) N, M[x := N]) | M, N ∈ Λ};
η ≣ {(λx.M x, M) | M ∈ Λ, x ∉ FV(M)};
βη ≣ β ∪ η.

Выражение, подвыражением которого является дырка, называется контекстом и обозначается C[ ], при этом C[M] — результат подстановки выражения M вместо дырки в контексте C[ ].

Если σ — редукция, то выражение M — σ-редекс, если ∃N: (M, N) ∈ σ. Также можно говорить и о σ-конверсии «=_σ»:

(M, N) ∈ σ ⇒ C[Μ] →_σ C[N];
M ↠_σ M;
M →_σ N ⇒ M ↠_σ N;
M →_σ N ∧ N →_σ P ⇒ M ↠_σ P;
∃P: M ↠_σ P ∧ N ↠_σ P ⇒ M =_σ N.

σ-нормальной формой называют выражение Μ, если ∄Ν: M →_σ Ν. В экстенсиональном λ-исчислении под редексом имеют в виду βη-редекс, а под нормальной формой — βη-нормальную форму. Говорят, что M имеет нормальную форму N, если M ↠ N. При этом βη-конверсию обычно обозначают просто «=», и это неслучайно: формально система λβη является эквациональной теорией. Так как такие теории свободны от логики, непротиворечивость в них определяется несколько иначе.

Равенством будем считать формулу вида M = N, где M, N — λ-выражения; такое равенство замкнуто, если M и N — комбинаторы. Пусть T — формальная теория, формулами которой являются равенства. Тогда говорят, что T непротиворечива (и пишут Con(T)), если в T доказуемо не любое замкнутое равенство. В противном случае говорят, что T противоречива. Одна из причин рассмотрения λβη состоит в том, что эта теория обладает определенным свойством полноты. Эквациональная теория T называется полной по Гильберту-Посту (сокращенно HP-полной), если для любого равенства M = N в языке теории T или M = N доказуемо, или T + (M = N) противоречива. HP-полные теории соответствуют максимальным непротиворечивым теориям в теории моделей для логики первого порядка.

Стратегия — это такое отображение F: Λ → Λ, что ∀M: M ↠ F(M). Для одношаговой стратегии выполняется ∀M: M → F(M). Стратегия называется нормализующей, если для любого выражения M, имеющего нормальную форму N, для некоторого числа n выполняется Fⁿ(M) ≣ N. Левая редукция F_l — одна из самых простых одношаговых нормализующих стратегий: она заключается в выборе β-редекса, значек «λ» в котором стоит текстуально левее, чем у других β-редексов, либо левого η-редекса, если β-редексов нет. Таким образом, если два терма имеют общую нормальную форму, то с помощью левой редукции доказательство соответствующей формулы можно получить за конечное число простых шагов. Если же формула недоказуема, то либо процесс не завершается вовсе, либо он завершается на разных нормальных формах.

Шпаргалка по λ-исчислению (практика)

Шпаргалка по нужной для практики теории готова, поэтому теперь попробуем сделать выжимку из практической части монографии Барендрегта по λ-исчислению. Речь пойдет о комбинаторной логике, теореме о неподвижной точке и синтаксическом сахаре.

Множество комбинаторов Ξ порождает наименьшее множество Ξ⁺ как замыкание по аппликации:

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

Множество Ξ называется базисом, если ∀M ∈ Λ₀: ∃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), и все в порядке.

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