Первичность/вторичность (бес)типового λ-исчисления

Читая о моделях λ-исчисления в классической монографии по λ-исчислению (Х. Барендрегт, «Ламбда-исчисление. Его синтаксис и семантика», перевод с английского Г. Е. Минца под редакцией А. С. Кузичева, Москва, «Мир», 1985), я вдруг нашел ответ на свое старое недоумение, почему категорщикам не нравится отсутствие типов:

Используя категорное определение модели λ-исчисления, Скотт сделал следующие философские замечания.

1. Модели бестипового λ-исчисления возникают из декартово-замкнутых категорий с рефлексивным объектом. Сами декартово-замкнутые категории соответствуют типовому λ-исчислению… Поэтому типовое λ-исчисление первично, а бестиповая теория вторична.

2. Пусть C — декартово-замкнутая категория с рефлексивным объектом U. По лемме Йонеды категорию C можно вложить в топос D = Set^Cop. Используя семантику Крипке–Жуаяля, мы видим, что в D объект U^U является полным пространством функций на U и потому U удовлетворяет аксиоме слабой экстенсиональности [∀x (M = N) → λx.M = λx.N] в D. За что приходится платить переходом к интуиционистской логике, так как классическая логика неполна относительно интерпретации Крипке–Жуаяля.

Некоторые комментарии. Что касается замечания 1, то имеются, конечно, красивые результаты о типовом λ-исчислении… Мы, однако, не согласны с выводом Скотта о первичности типового λ-исчисления по сравнению с бестиповой теорией. Во всяком случае это не верно с точки зрения вычислимости: типовое λ-исчисление (даже в присутствии рекурсора) способно представить лишь собственное подмножество множества рекурсивных функций, в то время как бестиповая теория представляет их все. В связи с замечанием 2 очень интересно предложение Скотта осуществить старую мечту Черча и Карри — изоморфизм U^U ≃ U — внутри топоса…

Комбинаторные алгебры (молча о патологиях)

В копилку цитат из монографии (Х. Барендрегт, «Ламбда-исчисление. Его синтаксис и семантика», перевод с английского Г. Е. Минца под редакцией А. С. Кузичева, Москва, «Мир», 1985), то есть туда же, где «и все в порядке»:

Комбинаторная алгебра — это аппликативная структура [множество с бинарной операцией]… с двумя выделенными элементами k, s, удовлетворяющими равенствам

k x y = x, s x y z = x z (y z).

Отметим, что комбинаторная алгебра нетривиальна [множество содержит больше одного элемента] тогда и только тогда, когда k ≠ s… При рассмотрении комбинаторных алгебр мы обычно молчаливо подразумеваем, что они нетривиальны. [Тривиальные комбинаторные алгебры соответствуют противоречивым эквациональным теориям.]

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

Нетривиальные комбинаторные алгебры

1) некоммутативны,
2) неассоциативны,
3) неконечны,
4) нерекурсивны.

Топология λ-выражений

Помимо материала, компактно собранного в шпаргалках по теории и практике λ-исчисления, ниже будут использоваться следующие обозначения. Во-первых, металамбда-абстракция λx.f(x) — безымянная запись теоретико-множественной функции f, например (λx.x² + 1)(3) = 10. Во-вторых, определим множество кодов конечных последовательностей (при какой-либо стандартной их кодировке натуральными числами)

Seq = {<n₁,…, n_k> | k ∈ N, n₁,…, n_k ∈ N} ∪ {< >};
lh(< >) = 0;
α = <n₁,…, n_k> ∈ Seq ⇒ lh(α) = k;
α = <m₁,…, m_p>, β = <n₁,…, n_q> ∈ Seq ⇒ a * b = <m₁,…, m_p, n₁,…, n_q>;
α = <m₁,…, m_p>, β = <n₁,…, n_q> ∈ Seq ∧ p ≤ q ∧ m₁ = n₁ ∧ … ∧ m_p = n_p ⇒ α ≤ β.

Пусть 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 вместо σ ∈ T_A и A(α) = ⊥, когда A(α)↑, но все же α ∈ A.

Если Σ = {λx₁.…λx_n.x | n ≥ 0, x₁,…, x_n, x ∈ Λ}, то частично Σ-помеченное дерево называется деревом бемовского типа. Множество всех таких деревьем обозначим B. Поддерево дерева A, исходящее из узла α — это A_α = λβ.A(α * β). Очевидно, что ∀A ∈ B: ∀α: A_α ∈ B.

Комбинатор M разрешим, если

∃n: ∃N₁,…, N_n ∈ Λ₀: M N₁ … N_n = I.

Например, комбинатор неподвижной точки разрешим, так как Y (K I) = K I (Y (K I)) = I. С другой стороны, Ω неразрешим. Произвольное λ-выражение разрешимо, если разрешим комбинатор λx₁.…λx_n.M, где {x₁,…, x_n} = FV(M).

λ-выражение M является головной нормальной формой, если оно имеет вид

M ≣ λx₁.…λx_n.x M₁ … M_m, m, n ≥ 0.

Говорят, что M имеет головную нормальную форму N, если M = N. Главной называется та головная нормальная форма выражения, которая первой достигается его левой редукцией.

Уодсворт ввел класс λ-выражений, не имеющих головной нормальной формы, и привел доводы в пользу того, что элементы этого класса должны рассматриваться как бессмысленные выражения в λ-исчислении. Также ему принадлежит следующий важный результат: λ-выражение разрешимо тогда и только тогда, когда оно имеет головную нормальную форму. Таким образом, из неразрешимости M следует, что для любых выражений N₁,…, N_n выражение M N₁ … N_n не имеет нормальной формы.

Дерево Бема для терма M, обозначаемое через BT(M), — это дерево бемовского типа, определяемое следующим образом:

1) если M неразрешим, то ∀σ: BT(Μ)(σ)↑,
2) если M разрешим и имеет главную головную нормальную форму λx₁.…λx_n.x M₀ … M_{m - 1}, то

BT(M)(< >) = <λx₁.…λx_n.x, m>;
k < m ⇒ BT(M)(<k> * σ) = BT(M_k)(σ);
k ≥ m ⇒ BT(M)(<k> * σ)↑.

Рассмотрим полное частично упорядоченное множество B = (B, ⊆) с топологией Скотта. Топология деревьев на множестве Λ — это наименьшая топология, в которой непрерывно отображение BT: Λ → B. Иными словами, открытые подмножества Λ имеют вид BT^-1(O), где O открыто в топологии Скотта на B.

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

Доказано, что аппликация и абстракция непрерывны в топологии деревьев на Λ, причем для аппликации это нетривиальный результат, имеющий интересные следствия. Например, множество Sol ⊆ Λ разрешимых термов открыто. Действительно, в любом полном частично упорядоченном множестве множество {x | x ≠ ⊥} открыто по Скотту. Следовательно, множество Sol = BT^-1{A | A ≠ ⊥} открыто в Λ.