История λ-исчисления уходит в начало прошлого века. Этимология названия данного раздела математической логики, который служит основой для «computer science», следующая. Сам значек «λ» используется для одной из двух основных конструкций в созданной Черчем системе — абстракции. Оказывается, что выбор обозначения абстракции не был совершенно случайным, а сделан в противопоставление другой более ранней конструкции, которую использовали Whitehead и Russell и обозначали как «xˆ». Для новой конструкции, чтобы отличать ее от прежней, Черч заменил обозначение сначала на «∧x», а затем — на «λx», очевидно, интерпретировав первый символ как заглавную букву «Λ», для упрощения набора.
Опишем кратко систему λβη, то есть классическое бестиповое экстенсиональное λ-исчисление, сделав конспект классической монографии по λ-исчислению (Х. Барендрегт, «Ламбда-исчисление. Его синтаксис и семантика», перевод с английского Г. Е. Минца под редакцией А. С. Кузичева, Москва, «Мир», 1985).
Множество λ-выражений Λ строится индуктивно из переменных
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)», так как оно выполняется в силу соглашения о переменных: если в определенном математическом контексте встречаются термы M1,…, Mn, то подразумевается, что связанные переменные в них выбраны так, чтобы они были отличны от свободных переменных.
Если множество FV(M) пусто, то M называют комбинатором. Множество всех комбинаторов обозначают Λ0:
Λ0 ≣ {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 ↠σ M;
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 выполняется Fn(M) ≣ N. Левая редукция Fl — одна из самых простых одношаговых нормализующих стратегий: она заключается в выборе β-редекса, значек «λ» в котором стоит текстуально левее, чем у других β-редексов, либо левого η-редекса, если β-редексов нет. Таким образом, если два терма имеют общую нормальную форму, то с помощью левой редукции доказательство соответствующей формулы можно получить за конечное число простых шагов. Если же формула недоказуема, то либо процесс не завершается вовсе, либо он завершается на разных нормальных формах.
Речь пойдет о комбинаторной логике, теореме о неподвижной точке и синтаксическом сахаре.
Множество комбинаторов Ξ порождает наименьшее множество Ξ+ как замыкание по аппликации:
Ξ ⊆ Ξ+;
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), и все в порядке.
Помимо материала, компактно собранного выше, в заключительной части конспекта, посвященной топологии на λ-выражениях, будут использоваться следующие обозначения. Во-первых, металамбда-абстракция λ.f(x) — безымянная запись теоретико-множественной функции f, например (λx.x2 + 1)(3) = 10. Во-вторых, определим множество кодов конечных последовательностей (при какой-либо стандартной их кодировке натуральными числами)
Seq = {<n1,…, nk> | k ∈ N, n1,…, nk ∈ N} ∪ {< >};
lh(< >) = 0;
α = <n1,…, nk> ∈ Seq ⇒ lh(α) = k;
α = <m1,…, mp>, β = <n1,…, nq> ∈ Seq ⇒ a * b = <m1,…, mp, <n1,…, nq>;
α = <m1,…, mp>, β = <n1,…, nq> ∈ Seq ∧ p ≤ q ∧ m1 = n1 ∧ … ∧ mp = np ⇒ α ≤ β.
Пусть D = (D, ⊑) — частично упорядоченное множество с рефлексивным отношением ⊑. Тогда подмножество X ⊆ D называется направленным, если
X ≠ ∅ ∧ ∀x, y ∈ X: ∃z ∈ X: x ⊑ z ∧ y ⊑ z.
При этом D называется полным, если для любого направленного подмножества X ⊆ D существует супремум ⊔X ∈ D и имеется дно ⊥:
∃⊥ ∈ D: ∀x ∈ D: ⊥ ⊑ x.
Топология Скотта на полном частично упорядоченном множестве (D, ⊑) определяется следующим образом: множество O ⊆ D считается открытым, если
1) x ∈ O ∧ x ⊑ y ⇒ y ∈ O;
2) X ⊆ D ∧ ⊔X ∈ O ⇒ X ∩ O ≠ ∅.
Частичное отображение φ: X ⤳ Y — это отображение φ, такое, что область определения Dom(φ) ⊆ X. Для x ∈ X запись φ(x)↓ означает, что φ(x) определено, то есть x ∈ Dom(φ); выражения φ(x)↑ и φ(x) = ↑ означают, что φ(x) не определено, то есть x ∉ Dom(φ).
Если Σ — некоторое множество символов, то частично Σ-помеченное дерево — это частичное отображение φ: Seq ⤳ Σ × N, такое, что
1) φ(σ)↓ ∧ τ ≤ σ ⇒ φ(τ)↓;
2) φ(σ) = <a, n> ⇒ ∀k ≥ n: φ(σ * <k>)↑.
Обнаженное дерево, лежащее в основе частично Σ-помеченного дерева φ, — это дерево
Tφ = {< >} ∪ {σ = σ' * <k> ∧ φ(σ') = <a, n> ∧ k < n}.
Если σ ∈ Tφ и φ(σ) = <a, n>, то a называется меткой в узле σ. Если же для σ ∈ Tφ φ(σ)↑, то говорят, что узел σ непомеченный. Частично помеченные деревья будем обозначать заглавными буквами и будем писать σ ∈ A вместо σ ∈ TA и A(α) = ⊥, когда A(α)↑, но все же α ∈ A.
Если Σ = {λx1…xn.x | n ≥ 0, x1,…, xn, x ∈ Λ}, то частично Σ-помеченное дерево называется деревом бемовского типа. Множество всех таких деревьем обозначим B. Поддерево дерева A, исходящее из узла α — это Aα = λβ.A(α * β). Очевидно, что ∀A ∈ B: ∀α: Aα ∈ B.
Комбинатор M разрешим, если
∃n: ∃N1,…, Nn ∈ Λ0: M N1 … Nn = I.
Например, комбинатор неподвижной точки разрешим, так как Y (K I) = K I (Y (K I)) = I. С другой стороны, Ω неразрешим. Произвольное λ-выражение разрешимо, если разрешим комбинатор λx1 … xn.M, где {x1,…, xn} = FV(M).
λ-выражение M является головной нормальной формой, если оно имеет вид
M ≣ λx1…xn.x M1 … Mm, m, n ≥ 0.
Говорят, что M имеет головную нормальную форму N, если M = N. Главной называется та головная нормальная форма выражения, которая первой достигается его левой редукцией.
Уодсворт ввел класс λ-выражений, не имеющих головной нормальной формы, и привел доводы в пользу того, что элементы этого класса должны рассматриваться как бессмысленные выражения в λ-исчислении. Также ему принадлежит следующий важный результат: λ-выражение разрешимо тогда и только тогда, когда оно имеет головную нормальную форму. Таким образом, из неразрешимости M следует, что для любых выражений N1,…, Nn выражение M N1 … Nn не имеет нормальной формы.
Дерево Бема для терма M, обозначаемое через BT(M), — это дерево бемовского типа, определяемое следующим образом:
1) если M неразрешим, то ∀σ: BT(Μ)(σ)↑,
2) если M разрешим и имеет главную головную нормальную форму λx1…xn.x M1 … Mm — 1, то
BT(M)(< >) = <λx1…xn.x, m>;
k < m ⇒ BT(M)(<k> * σ) = BT(Mk)(σ);
k ≥ m ⇒ BT(M)(<k> * σ)↑.
Рассмотрим полное частично упорядоченное множество B = (B, ⊆) с топологией Скотта. Топология деревьев на множестве Λ — это наименьшая топология, в которой непрерывно отображение BT: Λ → B. Иными словами, открытые подмножества Λ имеют вид BT-1(O), где O открыто в топологии Скотта на B.
Используя топологию деревьев, можно выразить обычные понятия, относящиеся к λ-исчислению, в топологических терминах. Например, нормальные формы оказываются изолированными точками, а неразрешимые выражения — точками компактификации, то есть такими точками, единственной окрестностью которых является само топологическое пространство.
Доказано, что аппликация и абстракция непрерывны в топологии деревьев на Λ, причем для аппликации это нетривиальный результат, имеющий интересные следствия. Например, множество Sol ⊆ Λ разрешимых термов открыто. Действительно, в любом полном частично упорядоченном множестве множество {x | x ≠ ⊥} открыто по Скотту. Следовательно, множество Sol = BT-1{A | A ≠ ⊥} открыто в Λ.
Автор: codedot
Здоровское изложение!