Рассмотрим типизированные вычислительные модели объектов дан-
ных. Основной целью системы типизации ОД 2 является ее исполь-
зование для моделирования выполнения либо конструкций ЯМОД3,
либо программы, возможно, использующей конструкции ЯМОД. Рас-
смотрим способ интерпретации конструкций ЯМОД или ЯМОД, ко-
торые, возможно, входят в объемлющую программу, либо, наоборот,
содержат программу (функции) системы программирования. Способ
основан на определении и использовании семейств аппликативных
предструктур вида
< {HB},{evBC} >
для произвольных типов B, C из системы типизации ОД, где H --
домен объектов типа B, evBC -- аппликатор вычисления значения
функции на аргументе из HB.
HT(I)--1. При построении вычислительной модели объектов дан-
ных (ВМОД) предполагаются следующие действия:
• введение в рассмотрение пространства функций как явных
объектов в представляющей категории;
• построение по заданным объектам AиB самостоятельно-
го объекта (A → B);
• установление для его использования отображения-апплика-
тора evBC : (B → C) × B → C, которое обеспечивает по
f : B → C и x : B вычисление f(x) : C, то есть f, x 7→ f(x);
•при вычисленииh(x, y)двухаргументного отображения-оператора
h : A×B → C фиксируется x, а h(x, y) считается функцией
2 ОД -- объекты данных.
3 ЯМОД -- языкманипулирования объектами данных.
от y;
• для связи h со значениями вводится специальная функция
абстракторΛABC, типизируемая посредством
(ΛABCh) : A → (B → C);
• для заданного опертора h и аргумента x абстрактор име-
ет вид (ΛABCh)(x) : B → C, что позволяет при вычислении
значения от второго аргумента использовать аппликатор.
Принципиальной особенностью этой ВМОД является возмож-
ность ее использования для концептов, индивидов и состояний
по отдельности. Вместе с тем допустимо применять ВМОД
и для объекта данных в целом.
HT(I)--2. Абстракция по двум переменным. При абстрагировании
по двум переменным проявляются все особенности разрабо-
танного аппарата, которые обычным образом переносятся
на случай большего числа переменных. Для сокращения записи
дескрипции не указаны сорта переменных:
λ[x, y].t = λzIw∀x∀y(z = [x, y] & t = w).
В свою очередь w трактуется как отношение
w = Id∀z∀τ[d[z, τ] ↔ Ψ]
и τ ∈ w0
(z). Поскольку термt в зависимости от z принимает
значения из w0
(z), то полагаем t ∈ w0
(z). Соответствующие
упорядоченные пары[z, t] кладутся в основу определения объ-
екта
λz.t = λ[x, y].t,
что дает требуемую дескрипцию.
HT(I)--3. Функциональнное пространство. Этот объект предста-
вляет множество функций из типа A в тип B, что записы-
ваем в виде дескрипции
A → B = {z : [A,B] | ∀x ∈ A∃y ∈ B.z[x, y]}
или в более слабой форме для сортов A, B и A → B. В по-
следнем случае определяющая формула изменяется для учета
связи сортов A, B с типами , B.
HT(I)--4. Аппликатор. На основе двух предыдущих дескрипций ука-
жем дескрипцию для оценочного морфизма:
evAB = λ[z, x]Iy.z[x, y],
которая по функции z ∈ A → B и аргументу x ∈ A указыва-
ет значение y ∈ B, то есть
evAB : [z, x] 7→ z(x),
или в более общем случае, evAB : [z, x] 7→ y.
|
Главная
Каталог файлов
