Теоретические сведения. Задача погружения объектов одной теории в дру-
гую возникает при рассмотрении содержательно заданных отображений,
когда требуется осуществить их трансляцию в аппликативный (функци-
ональный) язык.
При выполнении настоящей работы требуется небольшой запас опреде-
лений: K = λxy.x, I = λx.x, [x, y] = λr.rxy (упорядоченная пара).
Формулировка задачи. Получить терм λ-исчисления, соответствую-
щий декартову произведению n-объектов. Дополнительно устано-
вить n термов, которые ведут себя как проекции. (Указание: для слу-
чая n = 2 получаем
Действительно, непосредственной проверкой можно убедиться, что
((A0 ×A1)×A2)[[x0, x1], x2] = [[A0(x0), A1(x1)], A2(x2)].
Для установления соответствующих проекций сформулируем сле-
дующее утверждение (весьма простое) и выполним его проверку.
Утверждение.
Проверка.
Перейдем теперь к обобщению произведения.
Обобщение. По индукции можно доказать, что:
Выполнить доказательство самостоятельно.
Указание к доказательству обобщения. Частные случаи:
Частные случаи проекций декартова произведения в преобразован-
ном виде:
Неформальное обсуждение решенной задачи сводится к следующим
соображениям. Упорядоченныеn-ки широко распространены, в част-
ности, из них конструируются отношения реляционной базы данных.
Напомним, что язык манипулирования данными реляционных си-
стем управления базами данных рассматривает совокупности n-ок в
виде самостоятельных объектов, называемых отношениями. Часто
использумый запрос к базе данных состоит в усечении имеющихся
отношений и может быть сведен к операциям проекции. Для выпол-
нения этих операций нужен уже реализованный язык запросов.
В данном случае в качестве системы программирования исполь-
зуется АВС. Более точное рассуждение предполагает оговорки, что в
качестве системы-оболочки используется оболочка Каруби (см. раз-
дел 13). В рамках этой оболочки построены объекты-произведения и
объекты-проекции. В свою очередь они состоят из объектов-комби-
наторов. Программирование выполнено полностью в терминах объ-
ектов. |
Главная
Каталог файлов
