Теоретические сведения.Идея построения функционального языка, в кото-
ром вовсе отсутствуют переменные, основывается на использовании ком-
бинаторной логики. Отказываясь от переменных, проектировщик языка
программирования начинает оперировать произвольными объектами, ко-
торые при построении программы разрешается применять друг к другу.
Очевидно, что это наиболее рафинированная форма использования объек-
тов.
Как известно, для корректного использования объектов следует оста-
ваться в рамках какого-либо варианта комбинаторной логики, играюще-
го роль теории-оболочки. Комбинаторы из этой оболочки в совокупности
составляют “набор инструкций” некоторой абстрактной вычислитель-
ной системы. Может сложиться впечатление, что этот набор ничем не
ограничен. В этом случае его математические свойства остаются непро-
явленными и потенциально содержащими ту или иную форму противоре-
чия.
Выберем в качестве теории-оболочки теорию категорий. Зафиксиру-
ем в ней набор комбинаторов, который проявляет вполне безопасное ма-
тематическое поведение: составляет декартово замкнутую категорию.
Заметим, что в декартово замкнутой категории (д.з.к.) функции понима-
ются как операторы, действующие на свои операнды, которые записыва-
ются позиционно. С другой стороны, в аппликативной вычислительной си-
стеме (АВС) используется единственная операция - операция аппликации,
трактуемая как приложение одного объекта к другому. Возникает вопрос,
не происходит ли каких-либо потерь при переходе от системы понятий и
определений д.з.к. к системе понятий и определений АВС и наоборот.
Воспользуемся следующими соглашениями об обозначениях:
[x, y] = λr.rxy,
< f, g > = λt.[f(t), g(t)] = λt.λz.z(f(t))(g(t)).
Тот факт, что f является отображением из A в B (в содержательном
смысле) будем обозначать посредством f : A → B. Введем в рассмотре-
ние следующие отображения:
h : A × B → C для x : A, y : B,
ΛABCh : A → (B → C),
ΛABC : (A × B → C) → (A → (B → C)),
k : A → (B → C),
εBC : (B → C) × B → C,
ε◦ < k ◦ p, q >: A × B → C,
p : A × B → A, q : A × B → B
В дальнейшем эти отображения будут часто использоваться без
явного упоминания их типов, если только не возникает двусмыслен-
ности в толковании.
Задача 11.1 Поскольку в оболочке Каруби выводимо:
h = ε◦ < (Λh) ◦ p, q >,
а также выводимо:
k = Λ(ε◦ < k ◦ p, q >),
то прежде всего из предыдущих определений следует самостоя-
тельно получить оба равенства.
Решение.
Λ--1. Во-первых, покажем, как строить перевод выражений из опера-
торной формы в аппликативную, то есть ищем функцию h0 такую,
что h[x, y] = h0xy. Это получается следующим образом:
h = ε◦ < (Λh) ◦ p, q >;
h[x, y] = (εBC◦ < (Λh) ◦ p, q >)[x, y]
= εBC(< (Λh) ◦ p, q > [x, y])
= εBC[((Λh) ◦ p)[x, y], q[x, y]]
= εBC[(Λh)(p[x, y]), q[x, y]]
= εBC[((Λh)x), y]
= (((Λh)x)y) = Λh x y
≡ h0 x y.
Проделанные вычисления нуждаются в правильном приписывании
объектам типов1. Следовательно, h0 x y = (Λh)x y.
Λ--2. Во-вторых, покажем, как строить перевод выражений из аппли-
кативной в операторную форму, то есть ищем функцию k0 такую,
что k x y = k0[x, y]. Это получается следующим образом:
k = Λ(ε◦ < k ◦ p, q >);
kxy = Λ(ε◦ < k ◦ p, q >)xy
= (λu.λv.(ε◦ < k ◦ p, q >)[u, v])xy
= ε◦ < k ◦ p, q > [x, y]
≡ k0
[x, y].
Таким образом, k0 = ε◦ < k ◦ p, q > и Λk0 = k. Остается заме-
тить, что через “=” обозначаем отношение η −ξ-конвертируемости:
оно рефлексивно, симметрично и транзитивно. Следовательно, оно
является отношением эквивалентности. Последнее обстоятельство
позволяет придти к заключению, что
( × → ) ∼= ( → ( → )),
где символ “∼=” читается как “изоморфно”.
1
У выражения ((Λh)x) тип B → C. Выражению y приписан тип B. Выражение
(((Λh)x)y) получает тип C. |
Главная
Каталог файлов
