Система типов данных

Любая переменная характеризуется некоторым типом. Язык CCP является бестиповым в том смысле, что типы переменных не указываются в программе, однако их можно однозначно определить по программе. Система типов описывается далее в виде математической модели.

Тип определяет множество значений. Тип идентифицируется именем типа. Система типов языка CCP включает примитивные типы, подмножество произвольного типа и структурные типы. Для каждого типа набор операций со значениями типа представлен в виде базисных вычислимых предикатов.

Примитивными типами являются: логический, целый, вещественный и литерный. Для них соответственно будем использовать имена: BOOL, INT, REAL и CHAR. Набор базисных предикатов для примитивных типов соответствует распространенным арифметическим и логическим операциям. Например, базисные предикаты +(x, y: z), -(x, y:z), -(x:y), <(x, y:b) соответствуют операциям z = x + y, z = x - y, y = -x , b = x < y.

Для каждого примитивного типа определены два вида предикатов равенства: =(x: y) и =(x, y: b). Для предиката =(x: y) процессор присваивает переменной y значение переменной x. Для предиката =(x, y: b) процессор определяет значение отношения x = y и присваивает его логической переменной b. Предикат =(d: e) определен также для наборов переменных d и e.

Имеется набор базисных предикатов для задания констант. Предикаты
ConsIntZero( :x) и ConsIntOne( :x) определяют целочисленные значения 0 и 1 в качестве значения переменной x.

Далее в определениях типов T, S, X, Y и Z обозначают имена типов.

Новый тип S как подмножество типа T вводится определением

S = SUBSET(T, x, P, d) . (4.3)

Здесь x - переменная типа T, а d - произвольный, возможно пустой, набор переменных, P - имя предиката. Предикат P(x, d: b) является вычислимым, т. е. должен быть определен на языке CCP. Тип S есть множество истинности предиката P(x, d), т. е. S = {xÎT | P(x, d)}. Переменные набора d являются параметрами типа S. Примером подмножества типа является тип натуральных чисел:

NAT = SUBSET(INT, x, GE0) = {xÎINT | x ³ 0} ,

где GE0 есть имя предиката x ³ 0. Другим примером является диапазон целых чисел:

DIAP(n) = SUBSET(INT, x, IN1_n, n) = {xÎINT | x ³ 1 & x £ n} ,

где IN1_n есть имя предиката x ³ 1 & x £ n.

Структурный тип определяется в виде композиции других типов, называемых компонентными по отношению к структурному. Структурными типами являются: произведение типов (кортеж), объединение типов, множество подмножеств типа и предикатный тип. Базисные предикаты для структурного типа подразделяются на конструкторы, деструкторы и другие операции со значениями типа. Конструктор по значениям компонентных типов строит значение структурного типа. Деструктор для значения структурного типа определяет соответствующие значения компонент.

Произведение типов

Z = X ´ Y (4.4)

определяет тип Z в виде множества кортежей (x, y), т. е. Z = {(x, y) | x Î X, y Î Y}. Конструктором является предикат ConsStruct(x, y:z), где x Î X, y Î Y и z Î Z, а деструктором - CompStruct(z:x, y). Для конструктора и деструктора истинно отношение z = (x, y).

Объединение [13] типов

Z = X + Y (4.5)

определяет множество элементов вида (1, x) и (2, y) для типов X и Y, т. е. Z = {(1, x) | x Î X} È {(2, y) | y Î Y}. Первая компонента в этих кортежах (1 или 2) является тегом значения. Конструктор ConsUnion1(x:z) строит структурное значение z по некоторому x Î X, т. е. z = (1, x). Аналогично, для конструктора ConsUnion2(y:z) имеет место z = (2, y). Деструктор CompUnion(z:i, x, y) для z Î Z определяет, что либо z = (1, x) и i = 1, либо z = (2, y) и i = 2. Если i = 1, то значение y не определено. Если i = 2, то значение x не определено.

Множество подмножеств

Z = SET(X) (4.6)

для конечного типа X есть Z = {z | z Í X}. Конструктор ConsSetEmpty( :z) определяет пустое множество в качестве значения переменной z. Конструктор ConsSetElem(x :z) определяет z = {x} для x Î X. Предикат CompSet(z, x:b) определяет истинность формулы x Î z.

Предикатный тип

Z = PRED(D: E) (4.7)

есть множество вычислимых предикатов вида j(d: e) для непересекающихся наборов переменных d и e, причем набор d может быть пустым. Типы переменных определяются соответствующими наборами типов D и E. Таким образом, Z = {j(d: e) | d Î D, e Î E, j Î CCP}. Конструктор предиката ConsPred описан в разд. 4.8.

Допустим, набор d не пустой, типы набора D являются конечными, а произвольный предикат j Î Z определен для любого d Î D, т. е. "j Î Z "d Î D $e j(d: e). При этих условиях предикат j(d: e) может трактоваться как массив. Переменные набора d называются индексами массива, а e - элементом массива. Конструктор массива ConsArray описан в разд. 4.9. Деструктор CompArray(j, d: e) определяет элемент e массива j для набора индексов d.

Совокупность типов программы представлена типами переменных, встречающихся в программе. Всякий тип либо является примитивным, либо вводится одним из определений вида (4.3)–(4.7).

Другими типами данных в языке CCP являются последовательности и деревья. Эти типы являются производными, а не базисными. Их определение является рекурсивным и использует произведение и объединение компонентных типов. Следует особо подчеркнуть, что типы указателей (pointers) не принадлежат языку CCP. В этом нет необходимости, поскольку структуры данных, использующие указатели в программе на чистом функциональном языке, могут быть преобразованы в эквивалентные структуры данных с использованием массивов, последовательностей и деревьев. Использование указателей подразумевается в списках для языков семейств ML и Лисп. Формальная семантика типов данных с указателями достаточно сложна.

Дадим примеры рекурсивных типов. Введем специальный тип: NIL = { nil}. Имя nil обозначает пустую последовательность. Тип последовательности, составленной из элементов некоторого типа T, вводится следующими определениями:

Seq = NIL + Seq1;

Seq1 = T ´ Seq.

Здесь тип T является параметром определяемого типа Seq. При использовании типа Seq в правой части определения другого типа в скобках указывается конкретный тип - параметр. Например, строковый тип как последовательность литер имеет определение

STRING = Seq(CHAR).

Тип списка LIST для языка Лисп представляется следующим набором определений:

LIST = Seq(ATOM);

ATOM = NIL + NUM + SYMBOL + LIST;

NUM = INT + REAL;

SYMBOL = STRING.

Определим семантику рекурсивно определяемых типов данных. Рассмотрим следующую систему определений типов:

X_k = φ_k(X₁, X₂,…, X_n, T₁, T₂,…, T_s); k = 1,…,n; n > 0; s ³ 0 . (4.8)

Здесь X₁, X₂,…, X_n - имена определяемых типов; φ_k - типовый терм вида Y ´ Z или Y + Z, где в качестве Y и Z могут быть типы X₁, X₂,…, X_n, T₁, T₂,…, T_s. Определения типов T₁, T₂,…, T_s не зависят от X₁, X₂,…, X_n. Например, система определений для типа LIST включает:

LIST = SeqATOM;

SeqATOM = NIL + Seq1;

Seq1 = ATOM ´ SeqATOM;

ATOM = NIL + NUM + SYMBOL + LIST.

Систему определений рекурсивных типов (4.8) перепишем в векторной форме:

X = φ(X) , (4.9)

где X = (X₁, X₂,…, X_n) - вектор типов и φ = (φ₁, φ₂,…, φ_n) - вектор типовых термов. Введем отношение ⊑ на векторах типов:

X ⊑ Y @ "k=1..n (X_k Í Y_k).

Отношение Í определяет нижнюю полурешетку на множестве всех типов с пустым типом Æ в качестве минимального элемента. Вектор типов Q = (Æ, Æ,…, Æ) является минимальным элементом полурешетки, определяемой отношением ⊑ на множестве векторов типов.

Рассмотрим последовательность векторов типов {X^m}_m³0, определяемую рекуррентно следующим образом:

X⁰ = Q, X^m+1 = φ(X^m), m ³ 0. (4.10)

Естественно ожидать, что предел последовательности {X^m}_m³0 (если он существует) даст нам неподвижную точку - решение системы (4.9). Рассмотрим построение неподвижной точки для рекурсивного типа Seq. Получим следующую последовательность типов:

Seq⁰ = Æ;

Seq¹ = NIL + (T ´ Seq⁰) = NIL + Æ = {1} ´ NIL È {2} ´ Æ = {(1, nil)};

Seq² = NIL + {(t, (1, nil))}, где t Î T;

Seq³ = NIL + ({t₂} ´ (NIL + {(t₁, (1, nil))})) , где t₁, t₂ Î T, и т. д.

Лемма 4.1. Функция φ системы (4.9) определений рекурсивных типов X = φ(X) является непрерывной относительно произведения и объединения. Понятие непрерывности функций определено в разд. 3.1. Отметим, термы вида SUBSET, SET и PRED могут встречаться в системе (4.9), но они не могут участвовать в рекурсии. Например, недопустима рекурсия вида Z = SET(Z).

Доказательство. Докажем, что произведение Y ´ Z и объединение Y + Z непрерывны относительно вхождений компонентных типов Y и Z. Пусть {Y^m}_m³0 и {Z^m}_m³0 - возрастающие цепи типов. Требуется доказать, что

È_m³0(Y^m ´ Z^m) = (È_m³0Y^m) ´ (È_m³0Z^m).

Докажем сначала, что тип левой части равенства содержится в типе правой части. Пусть (y, z) Î È_m³0(Y^m ´ Z^m). Существует такое k, что (y, z) Î Y^m ´ Z^m для всех m ³ k. Тогда y Î Y^m и z Î Z^m для m ³ k. Далее, y Î È_m³0Y^m и zÎ È_m³0Z^m. И, как следствие, (y, z) Î (È_m³0Y^m) ´ (È_m³0Z^m). Допустим теперь, что (y, z) Î (È_m³0Y^m) ´ (È_m³0Z^m), и докажем, что (y, z) Î È_m³0(Y^m ´ Z^m).
Из определения произведения y Î È_m³0Y^m и z Î È_m³0Z^m. Существуют такие k₁ и k₂, что y Î Y^m для m ³ k₁ и z Î Z^m для m ³ k₂. Пусть k = max(k₁, k₂). Тогда (y, z) Î Y^m ´ Z^m для всех m ³ k. Далее, (y, z) Î È_m³0(Y^m ´ Z^m). Непрерывность произведения доказана. Непрерывность объединения доказывается аналогичным образом.

Непрерывность функции φ доказывается следующей цепочкой равенств:

È_m³0φ(B^m) = È_m³0(φ₁(B^m), …, φ_n(B^m)) = (È_m³0φ₁(B^m), …, È_m³0φ_n(B^m)) = = (φ₁(È_m³0B^m), …, φ_n(È_m³0B^m)) = φ(È_m³0B^m). □

В соответствии с теоремой Клини о неподвижной точке (см. разд. 3.1) решением системы X = φ(X) является наименьшая неподвижная точка функции φ, т. е. È_m³0X^m, где X⁰ = Q, X^m+1 = φ(X^m).

Для построения последовательностей и деревьев вполне достаточно рекурсии с использованием произведения и объединения. Возможны другие, экзотические, формы рекурсии, однако они бесполезны при разработке реальных алгоритмов. Некоторые из них анализируются в книге [3].