Абстрактный тип данных

АТД как алгебраические системы

После того, как была осознана важность понятия АТД, была также осознана необходимость в его строгом математическом описании. Этой проблемой занялась группа ADJ.

ПРИМЕЧАНИЕ Идейным вдохновителем деятельности этой группы был Джозеф Гоген (Joseph Goguen). В статье «Воспоминания об ADJ» [10] Гоген пишет, что основной целью работы данной группы было показать связь между теорией категорий и информатикой, а в качестве задачи максимум – построить информатику на новом основании, теории категорий. Название «ADJ» намекает на термин «adjunction», обозначающий в теории категорий сопряжение двух категорий.

Как уже говорилось выше, неформально алгебраическую систему можно определить, как «множество с операциями». Например, множество натуральных чисел с операцией сложения образует алгебру (алгебраическую систему). В большинстве случаем дело обстоит несколько сложнее, операции определяются не на одном множестве, но на нескольких. Например, можно выделить множество строк и множество натуральных чисел, и определить операцию конкатенации (соединения) двух строк, а также операцию конкатенации конечного числа раз строки с собой. Последняя операция будет брать в качестве аргументов (операндов) строку и число, представляющее количество конкатенаций. В теории алгебраических систем отделяют описание операций и их свойств от конкретных реализаций этих операций на конкретных множествах. Далее в разделе будет описано, как это делается.
Для описания операций задается конечное множество имен сортов (типов). Каждое имя сорта представляет соответствующее множество. Множество имен сортов будем обозначать через S. Часто на множестве имен сортов вводят отношение подчинения (моделирующее отношение тип-подтип), которое образует алгебраическую структуру решетки, но здесь мы этого делать не будем.
Задается также множество OP имен или сигнатур операций. Сигнатурой (именем) операции назовем выражение вида

σ : s1 x s2 x .. x sn -> s

где все s_i, 1 ≤ i ≤ n, и s принимают значения в множестве имен сортов S. Элементы s₁, s₂, …, s_n представляют типы аргументов операции, а s – тип значения. Имя операции обозначается здесь греческой буквой σ. Количество аргументов операции называют ее арностью. Множество
Сигнатурой многосортной алгебры назовем пару Σ=(S,OP), где S – множество имен сортов, а OP представляет множество имен операций.
Сигнатура алгебры представляет описание операций этой алгебры (алгебраической системы). Это описание включает в себя описание имен сортов и имен операций, но без указания конкретных множеств и операций на них. Сигнатура многосортной алгебры является математическим представлением абстрактного типа данных, если его трактовать только как кластер операций, без задания аксиом-равенств и предусловий.
Заметим, что арность операции может быть нулевая. Операции с нулевой арностью называют еще константами. Вот, например, как будет выглядеть определение натурального числа в стиле Пеано:

S={Nat}, OP={0,s} 0 : -> Nat s : Nat -> Nat

Задается константа 0 как нульарная операция и унарная операция s увеличения числа на единицу.
Для задания алгебраической системы необходимо определить еще множества для каждого имени сорта и отображение на этих множествах для каждого имени операции. Множества, задаваемые для имен сортов, называются множествами-носителями этих сортов. Мы будем обозначать их через A_s для имени сорта s. Таким образом, приходим к следующему определению.
Многосортной Σ-алгеброй над сигнатурой Σ=(S,OP) будем называть пару A=(A_S,α), где A_S – набор множеств-носителей имен сортов S сигнатуры Σ, а α – семейство отображений вида

ασ : AS1 x AS2 x .. x ASn -> AS

заданных для каждого имени операции

σ : s1 x s2 x .. x sn -> s

Очевидно, что при таком определении каждой нульарной операции соответствует ровно один элемент множества-носителя сорта значения этой операции. Иначе говоря, нульарная операция просто выбирает некоторый элемент во множестве-носителе сорта своего значения. Это и объясняет тот факт, что такие операции называют константами.
Каждому сорту соответствует его множество-носитель, а каждой операции – отображение, определенное на декартовом произведении множеств-носителей аргументов операции, и имеющее значения в множестве-носителе сорта значения данной операции.
Для описанной выше сигнатуры определения множества натуральных чисел в стиле Пеано можно задать сколь угодно много многосортных Σ-алгебр. Основная такая Σ-алгебра – это множество натуральных чисел N, задаваемое как носитель сорта Nat, а также отображения: 0 для константы 0 и увеличения значения числа на единицу – для отображения s. Но можно задать и другие Σ-алгебры. Например, в качестве множества-носителя сорта Nat выбрать множество A = {x} из одного элемента x и задать x как значение отображения 0, а также в качестве значения отображения s. Это задание вполне корректно т.к. никаких требований к свойствам операций мы пока не предъявляем.
Определение многосортной алгебры очень напоминает задание абстрактного типа данных и его реализации. Только при задании АТД обычно имеется ввиду, что абстрактный тип может иметь несколько реализаций. Следовательно, для строгого математического описания АТД необходимо каким-то образом связать сигнатуры типа со всеми его реализациями.
На многосортных Σ-алгебрах можно задать отображения посредством задания отображений их множеств-носителей. В алгебре обычно интересны такие отображения, которые сохраняют свойства операций, т.е. инвариантны относительно отображений, определенных для операций сигнатуры Σ=(S,OP). Эта инвариантность выражается следующим образом. Пусть имеются две Σ-алгебры: A=(A_S,α) и A'=(A’_S,α’). Гомоморфизмом j : A -> A’ будем называть такое отображение j множеств-носителей A_S в множества-носители A’_S, которое сохраняет типы элементов и обладает следующим свойством: для любой операции σ из OP и для любого результата отображения α_σ(a₁, a₂, …, a_n) выполняется условие:

j(ασ(a1, a2, …, an))= α’σ(j(a1), j(a2), …, j(an)) (*)

Взаимооднозначный гомоморфизм называют изоморфизмом.
Свойство (*) просто говорит о том, .что применяя отображение α_σ, а затем переводя результат в алгебру A' отображением j, мы получим тоже самое, если переведем все аргументы a₁, a₂, …, a_n отображением j в алгебру A', а потом применим отображение, соответствующее операции σ.
Для выражения аксиом-равенств вводится множество переменных X. Элементы множества X типизированы сортами из S, т.е. каждая переменная принадлежит некоторому сорту. Из переменных и операций можно построить множество типизированных термов следующим образом:

1. 
   Имя нульарной операции есть терм, тип которого совпадает с типом значения операции.
   
2. 
   Имя любой переменной типа s есть терм типа s.
   
3. 
   Для любого имени операции вида σ : s₁ x s₂ x .. x s_n -> s и термов t₁, t₂, …t_n типов s₁ , s₂ , .. , s_n, соответственно, выражение вида σ(t₁, t₂, …t_n) есть терм типа s.
   
4. 
   Ничто другое не является термом типа s.
   

Например, пусть X={x,y} и рассматриваем сигнатуру определения натуральных чисел в стиле Пеано, определенную выше. В это алгебре только один тип – Nat, обе переменные x и y, также являются термами типа Nat. Нульарная операция 0 является термом типа Nat. С помощью операции s можно образовать термы вида: s(0), s(x), s(s(0)), s(s(s(y))) и т.д.
Множество термов, построенных из сигнатуры Σ=(S,OP) и множества переменных X, будем обозначать через T_Σ(X). Множество термов в свою очередь образует Σ-алгебру следующим образом:

• 
  Каждому сорту s сопоставляется множество термов, имеющих сорт s.
  
• 
  Каждой операции вида σ : s₁ x s₂ x .. x s_n -> s сопоставляется отображение, берущее список термов t₁, t₂, …t_n типов s₁ , s₂ , .. , s_n, соответственно, и задающее в качестве значения терм σ(t₁, t₂, …t_n) типа s.
  

Эта алгебра, построенная на множестве термов, играет важную роль в теории алгебраических систем. С помощью этой алгебры можно производить вычисления «синтаксически», на множестве термов, не имея какой-либо конкретной реализации сигнатуры Σ=(S,OP). В логике это построение называется Эрбрановским универсумом [11], используемым, в частности, для вычислений в языке Prolog.
Σ-алгебра, построенная на множестве термов без переменных (т.е. с одними константами в качестве атомарных термов), обладает одним важным свойством: из нее в каждую другую Σ-алгебру имеется единственный гомоморфизм. Таким Σ-алгебры называются инициальными алгебрами. Посредством инициальных Σ-алгебр можно описывать семантику программ, а также производить вычисления.
Для задания аксиом-равенств можно также использовать термы. Внимательный читатель вероятно уже заметил, что аксиомы, приведенные в примере описания АТД стек, на самом деле являются термами, между которыми стоит знак равенства. Более конкретно, равенством в сигнатуре Σ=(S,OP) будем называть тройку e=(X, t’, t’’), где X – некоторое множество переменных, используемых в термах равенства, а t' и t'' – термы, имеющие один и тот же тип.
Таким образом, мы приходим к следующему математически строгому определению абстрактного типа данных:
Абстрактным типом будем называть тройку ADT=(N, Σ, E), где N – имя абстрактного типа данных, Σ=(S,OP) – сигнатура многосортной алгебры, а E = {e₁, e₂, …,e_n} – конечный набор в сигнатуре Σ.
Каждая Σ-алгебра над сигнатурой Σ=(S,OP), в которой выполняются равенства E, называется реализацией абстрактного типа данных ADT=(N, Σ, E).
Таким образом, абстрактные типы данных определяются как сигнатуры многосортных алгебр, включающие в себя задание аксиом в виде равенств. Каждая реализация абстрактного типа данных математически представляет собой Σ-алгебру над сигнатурой данного абстрактного типа данных. Для каждого АТД можно построить алгебру термов, которая является «синтаксическим» представлением данного абстрактного типа данных, а также является инициальной алгеброй в классе всех Σ-алгебр данного АТД.