Любая переменная характеризуется некоторым типом. Язык 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.
Определим семантику рекурсивно определяемых типов данных. Рассмотрим следующую систему определений типов:
Xk = φk(X1, X2,…, Xn, T1, T2,…, Ts); k = 1,…,n; n > 0; s ³ 0 . (4.8)
Здесь X1, X2,…, Xn - имена определяемых типов; φk - типовый терм вида Y ´ Z или Y + Z, где в качестве Y и Z могут быть типы X1, X2,…, Xn, T1, T2,…, Ts. Определения типов T1, T2,…, Ts не зависят от X1, X2,…, Xn. Например, система определений для типа LIST включает:
LIST = SeqATOM;
SeqATOM = NIL + Seq1;
Seq1 = ATOM ´ SeqATOM;
ATOM = NIL + NUM + SYMBOL + LIST.
Систему определений рекурсивных типов (4.8) перепишем в векторной форме:
X = φ(X) , (4.9)
где X = (X1, X2,…, Xn) - вектор типов и φ = (φ1, φ2,…, φn) - вектор типовых термов. Введем отношение ⊑ на векторах типов:
X ⊑ Y @ "k=1..n (Xk Í Yk).
Отношение Í определяет нижнюю полурешетку на множестве всех типов с пустым типом Æ в качестве минимального элемента. Вектор типов Q = (Æ, Æ,…, Æ) является минимальным элементом полурешетки, определяемой отношением ⊑ на множестве векторов типов.
Рассмотрим последовательность векторов типов {Xm}m³0, определяемую рекуррентно следующим образом:
X0 = Q, Xm+1 = φ(Xm), m ³ 0. (4.10)
Естественно ожидать, что предел последовательности {Xm}m³0 (если он существует) даст нам неподвижную точку - решение системы (4.9). Рассмотрим построение неподвижной точки для рекурсивного типа Seq. Получим следующую последовательность типов:
Seq0 = Æ;
Seq1 = NIL + (T ´ Seq0) = NIL + Æ = {1} ´ NIL È {2} ´ Æ = {(1, nil)};
Seq2 = NIL + {(t, (1, nil))}, где t Î T;
Seq3 = NIL + ({t2} ´ (NIL + {(t1, (1, nil))})) , где t1, t2 Î T, и т. д.
Лемма 4.1. Функция φ системы (4.9) определений рекурсивных типов X = φ(X) является непрерывной относительно произведения и объединения. Понятие непрерывности функций определено в разд. 3.1. Отметим, термы вида SUBSET, SET и PRED могут встречаться в системе (4.9), но они не могут участвовать в рекурсии. Например, недопустима рекурсия вида Z = SET(Z).
Доказательство. Докажем, что произведение Y ´ Z и объединение Y + Z непрерывны относительно вхождений компонентных типов Y и Z. Пусть {Ym}m³0 и {Zm}m³0 - возрастающие цепи типов. Требуется доказать, что
Èm³0(Ym ´ Zm) = (Èm³0Ym) ´ (Èm³0Zm).
Докажем сначала, что тип левой части равенства содержится в типе правой части. Пусть (y, z) Î Èm³0(Ym ´ Zm). Существует такое k, что (y, z) Î Ym ´ Zm для всех m ³ k. Тогда y Î Ym и z Î Zm для m ³ k. Далее, y Î Èm³0Ym и zÎ Èm³0Zm. И, как следствие, (y, z) Î (Èm³0Ym) ´ (Èm³0Zm). Допустим теперь, что (y, z) Î (Èm³0Ym) ´ (Èm³0Zm), и докажем, что (y, z) Î Èm³0(Ym ´ Zm).
Из определения произведения y Î Èm³0Ym и z Î Èm³0Zm. Существуют такие k1 и k2, что y Î Ym для m ³ k1 и z Î Zm для m ³ k2. Пусть k = max(k1, k2). Тогда (y, z) Î Ym ´ Zm для всех m ³ k. Далее, (y, z) Î Èm³0(Ym ´ Zm). Непрерывность произведения доказана. Непрерывность объединения доказывается аналогичным образом.
Непрерывность функции φ доказывается следующей цепочкой равенств:
Èm³0φ(Bm) = Èm³0(φ1(Bm), …, φn(Bm)) = (Èm³0φ1(Bm), …, Èm³0φn(Bm)) = = (φ1(Èm³0Bm), …, φn(Èm³0Bm)) = φ(Èm³0Bm). □
В соответствии с теоремой Клини о неподвижной точке (см. разд. 3.1) решением системы X = φ(X) является наименьшая неподвижная точка функции φ, т. е. Èm³0Xm, где X0 = Q, Xm+1 = φ(Xm).
Для построения последовательностей и деревьев вполне достаточно рекурсии с использованием произведения и объединения. Возможны другие, экзотические, формы рекурсии, однако они бесполезны при разработке реальных алгоритмов. Некоторые из них анализируются в книге [3].