Теоретические сведения. Исследовательская работа в программировании
часто начинается с выбора объемлющей теории, то есть теории-оболочки,
в которой удобно представлять и исследовать вновь разрабатываемые
механизмы. При необходимости установления и поддержания системы
типов возникает необходимость в использовании такой теории-оболочки,
которая позволяет устанавливать и рассматривать различные идеи, каса-
ющиеся типов. По всей вероятности, в оболочке лучше совсем отказаться
от какой-либо априорной идеи типизации. Другими словами, приходится
иметь дело с бестиповой теорией, и хорошим примером такого рода слу-
жит бестиповое λ-исчисление.
В настоящем разделе исследуется установление связи теоретико-ка-
тегорных понятий с понятиями бестипового λ-исчисления. Пусть L - не-
которое исчисления λ-конверсий. Оболочкой Каруби для L, обозначаемой
через C(L), будем считать категорию, определяемую следующим образом.
Положим a ◦ b = λx.a(bx) для a, b принадлежащих L, где “◦” - знак
композиции функций.
Множество объектов категории : {a ∈ L | a ◦ a = a}.
Множество морфизмов : Hom(a, b) = {f ∈ L | b ◦ f ◦ a = f}.
Тождественный изоморфизм : id a = a.
Композиция морфизмов : f ◦ g.
Задача 13.1 Показать, что C(L) - категория. Предлагается это
проверить самостоятельно, выполнив согласование с какой-либо фор-
мой определения категории.
Уточнение формулировки задачи. Примем следующие определения
необходимых для проведения исследования объектов. Напомним, что
в данном случае необходимость выполнения следующих равенств
предполагается заранее:
A = λx.A(A(x)) = A ◦ A, (A)
F = λx.B(f(A(x))) = B ◦ f ◦ A. (f)
1. Декартово произведение:
A × B = λuλz.z(A(u(λxλy.x)))(B(u(λxy.y))).
2. Проекция на первый и на второй элемент соответственно:
pAB = λu.(A × B)(u)(λxλy.x), pAB : A × B → A;
qAB = λu.(A × B)(u)(λxλy.y), qAB : A × B → B.
3. Спаривание функций:
< f, g >= λtλz.z(f(t))(g(t)) = λt.[f(t), g(t)],
f : C → A, g : C → B, < f, g >: C → (A × B).
4. Множество отображений (функциональное пространство):
(A → B) = λf.B ◦ f ◦ A.
5. Аппликация (приложение функций к аргументу):
εBC = λu.C(u(λxy.x)(B(u(λxy.y)))),
εBC : (B → C) × B → C.
6. Функция каррирования, то есть перевода “обычных” функций
в аппликативный вид, названа в честь Х. Карри (Еще раз на-
поминаем: часто эту функцию обозначают через “Curry”; в
данном случае полагаем, что Curry ≡ Λ, то есть функцию
каррирования обозначаем через “Λ”):
(A × B) → C,ΛABCh : A → (B → C).
Требуется доказать следующее:
• Свойства проекций:
pAB ◦ < f, g >= f, qAB ◦ < f, g >= g,
< pAB ◦ h, qAB ◦ h >= h.
• Пусть h : (A × B) → C, k : A → (B → C). Тогда
ε ◦ < (Λh) ◦ p, q >= h,
Λ(ε ◦ < k ◦ p, q >) = k,
гдеΛ = ΛABC, p = pAB, ε = εBC, q = qAB .
Решение. Доказательство сводится к проверке свойств введенных
объектов.
C(L)--1. Заметим, что отображение h : (A × B) → C имеет перевод
в терм λ-исчисления, причем выполняется равенство:
h = λx.C(h((A × B)(x))),
где x = [x1, x2]. Это непосредственное следствие (f).
C(L)--2. Установим комбинаторную характеристику h:
h[x1, x2] = C(h((A × B)[x1, x2]))
= C(h(λz.z(A([x1, x2]K))(B([x1, x2](KI)))))
= C(h(λz.z(A x1)(B x2))) = C(h[A x1, B x2]).
Таким образом, h[x1, x2] = C(h[A x1, B x2]).
C(L)--3. Еще раз обратим внимание на необходимость учета следующих
равенств:
x = λz.a(x(1 z)) = A ◦ x,
f = λz.B(f(A z)) = B ◦ f ◦ A,
где 1 = λy.y = I.
C(L)--4. Нетрудно видеть (доказать самостоятельно !), что
(A × B) = λu.[A(u K), B(u(K I))],
где K = λxy.x, I = λx.x. Тогда непосредственной проверкой уста-
навливается следующая комбинаторная характеристика декарто-
ва произведения:
(A × B)[u, v] = λz.z(A([u, v]K))(B([u, v](K I)))
= λz.z(A u)(B v)
= [Au, Bv].
C(L)--5. Проверка свойств проекций приводит к следующим характери-
стикам:
pAB([u, v]) = (A × B)[u, v]K = [Au, Bv]K = A u,
qAB([u, v]) = (A × B)[u, v](K I) = [A u, B v](K I) = B v.
C(L)--6. Рассматривая упорядоченную пару [f, x], покажем, как с помо-
щью отображения εBC получить аппликацию f к x:
εBC([C ◦ f ◦ B, B ◦ x]) = εBC([f, x])
= C([C ◦ f ◦ B, B ◦ x]K(B([C ◦ f ◦ B, B ◦ x](K I))))
= C((C ◦ f ◦ B)(B(B ◦ x)))
= C(f(B x))
= (C ◦ f ◦ B)(x)
= f(x).
Отметим необходимость учета свойств композиции.1 По существу,
далее будем обосновывать простое равенство:ΛABC h x y = h([x, y])
(см. раздел 6, где определена функция каррирования).
C(L)--7. Пусть t представимо упорядоченной парой, то есть t = [t1, t2].
Тогда
(ε ◦ < (Λh) ◦ p, q >)t = ε[(Λh)(p t), q t]
= ε[(λxy.h[x, y])(pt), qt]
= ε[(λxy.h[x, y])t1, t2]
= ε[λy.h[t1, y], t2]
= (λy.h[t1, y])t2
= h[t1, t2].
Получено характеристическое равенство:
ε ◦ < (Λh) ◦ p, q >= h.
1
Напомним, что C ◦ f = f, B ◦ x = x.
C(L)--8. Установим теперь второе характеристическое равенство, где
#(t1) = A, #(t2) = B, #(t) = A × B, a t = [t1, t2],
то есть
t представлено в виде упорядоченной пары; через “#” обозначаем
функцию “вычисления типа”:
Λ(ε ◦ < k ◦ p, q >)t1 t2 = (ε ◦ < k ◦ p, q >)([t1, t2])
= ε[k(p t), q t] = ε[kt1, t2]
= (λu.C(uK(B(u(K I)))))[k t1, t2]
= C(k t1(B(t2)))
= C(k t1 t2)
= k t1 t2.
Тем самым2 обосновано характеристическое равенство
Λ(ε ◦ < k ◦ p, q >) = k.
Все введенные равенства действительно имеют место, что завершает
доказательство.
Использование оболочки Каруби привлекает те же самые идеи,
что и рассмотренные в разделе 10 при анализе функции list1. Дей-
ствительно, λ-исчисление дает широкий спектр различных термов.
Среди них отбираются только такие, на синтаксическую форму кото-
рых наложены специальные ограничения. Совокупность этих огра-
ничений, перечисленная в начале настоящего раздела, задает соотне-
сение. В качестве теории-концепта (общая оболочка) выступает бе-
стиповое λ-исчисление, рассматриваемое как теория вычислений. В
результате ее применения к соотнесению получается теория-индивид,
которая в свою очередь обладает свойствами оболочки. В частности,
в ее рамках представим специальный класс вычислений -- катего-
риальные вычисления. В данном случае вопрос о сравнении выра-
зительных возможностей теории-концепта и теории-индивида имеет
математический характер.
2
Следует учесть, что B(t2) = t2.
|
Главная
Каталог файлов
