Топология λ-выражений
Mar. 30th, 2012 07:38 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
codedotПомимо материала, компактно собранного в шпаргалках по теории и практике λ-исчисления, ниже будут использоваться следующие обозначения. Во-первых, металамбда-абстракция λx.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 ∉ 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 M0 … 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 ≠ ⊥} открыто в Λ.
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 ∉ 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 M0 … 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 ≠ ⊥} открыто в Λ.
