110

4. АЛГЕБРАИЧЕСКИЕ ОСНОВЫ ТИПОВ ДАННЫХ 92

4.1. Сигнатуры 93

Контрольные вопросы 94

4.2. Алгебры 94

Контрольные вопросы 96

4.3. Алгебры слов 96

Контрольные вопросы 97

4.4. Теории 97

Контрольные вопросы 98

4.5. Абстрактные типы данных 98

Контрольные вопросы 99

4.6. Иерархические модели типов данных 99

Контрольные вопросы 101

4.7. Типы и подтипы 101

Контрольные вопросы 102

4.8. Типы типов 102

Контрольные вопросы 103

4.9. Родовые типы данных 103

Контрольные вопросы 104

4.10. Полиморфные операции 104

Контрольные вопросы 105

4.11. Примеры спецификации типов данных 105

Контрольные вопросы 108

Задачи 108

1. Спецификация литерного типа данных 108

2. Спецификация натурального типа данных 108

3. Спецификация целого типа данных 108

4. Спецификация вещественного типа данных 108

5. Спецификация символьного типа данных 108

6. Спецификация строки символов 109

7. Спецификация спецификации имени 109

8. Спецификация константы 109

9. Спецификация типа данных «последовательность» 109

9. Спецификация типа данных «блок спецификаций» 109

10. Спецификация типа данных «запись» 109

11. Спецификация типа данных «оператор» 109

12. Спецификация типа данных «программа» 109

Глоссарий 109

4. Алгебраические основы типов данных

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

Интуитивно ясно, что тип данных характеризует некоторую группу (множество) однородных данных. На начальном этапе развития программирования популярным было определение: тип данных – это множество значений. Более детальное изучение проблемы типов данных навело на мысль: в программе, как и в реальной жизни, при работе с данными с каждым типом связывается некоторый набор операций по созданию и анализу значений данных. Постепенно в трактовке типа данных стал утверждаться принцип конструктивизма: тип данных характеризуется не столько множеством значений, сколько множеством операций. В результате дальнейших исследований появилось операционное определение: тип данных – это множество операций, задающих интерпретацию значений, принадлежащих универсальному пространству значений. Операции, определяющие тип данных, разбиваются на два класса: конструкторы и анализаторы. Конструкторы, их также называют внутренними операциями, вырабатывают в качестве результата значения определяемого типа. Анализаторы, по-другому – внешние операции, вырабатывают значения, не принадлежащие к определяемому типу (т.е. выдают информацию о значениях типа данных). Каждое значение данного типа является результатом работы последовательности конструкторов (не допускается существование в множестве значений некоторого типа таких значений, которые не вычисляются его операциями). В качестве примера рассмотрим тип натуральных чисел Nat с двумя конструирующими операциями nil и succ и одной анализирующей операцией eqv. Операция nil является константой, задающей первое значение типа (первичный конструктор). Операция succ использует в качестве аргумента значение данного типа и вырабатывает следующее значение этого типа (комбинированный конструктор). Анализатор eqv сравнивает два значения этого типа и вырабатывает значение логического типа (false или true). Сопоставляя операции с общепринятым изображением натуральных чисел, можно сказать, что знак 0 – это значение, вырабатываемое операцией nil, 1 – значение, вырабатываемое композицией операций succ(nil), 2 – succ(succ(nil)) и т.д. Все возможные последовательности операций типа образуют множество его значений. При этом, как правило, мало кого интересует, что является строительным материалом для значений типа (мы можем знать, конечно, что в компьютере непосредственным строительным материалом для целых или вещественных чисел являются биты, но в типизированных языках мы очень редко используем такое знание). Рассмотрение значений как результатов тех или иных последовательностей конструкторов позволяет утверждать, что каждое значение принадлежит только некоторому определенному типу, операциями которого оно произведено. Формулировка типа данных в таком случае выглядит следующим образом: тип данных определяет множество значений посредством множества операций.

Поскольку при создании типа необходимо указать для пользователя синтаксис и семантику операций, а для компьютера – способ их реализации, любой тип данных строится как комплекс из двух разделов: спецификации и реализации. Спецификация указывает синтаксис (имена, типы операндов и результатов) и семантику (смысл и условия применимости) операций. Реализация указывает представление типа (т.е. данные каких типов являются строительным материалом для значений данного типа) и алгоритмы операций в терминах типов представления. Пользователю типа данных всегда известен первый раздел, второй раздел обычно скрыт от него.

Для того чтобы операции использовались правильно (т.е. чтобы программист понимал, что делает данная операция и в каких условиях она применима, а компьютер мог проконтролировать правильность применения операции), синтаксис и семантика операций должны быть изложены на некотором формальном языке. К настоящему времени предложено несколько формальных методов спецификации программ вообще и типов данных в частности. Наибольшую популярность получил алгебраический подход. В главе представлена алгебраическая теория абстрактных типов данных, которая является математическим обоснованием процессов конструирования пользовательских данных исходя из существующего множества базовых данных. Любая система программирования строится с учетом теории типов данных. Настоящая глава посвящена рассмотрению алгебраического подхода и использованию его для детального изучения процессов типообразования в языках программирования.